关于时间逻辑方程的可解性

在由所建立起来的、数字式自动机的逻辑设计的、词混合运算方法(运算子法中,时间逻辑方程组乃是描述自动机的操作的《动力学》与表述自动机的结构的逻辑函数之间的关系的方便工具。本文的任务在于:从给定的时间逻辑方程 F(d,)～co 的、函数 F(d,)的特异析取范式,直接地从F(d,)～co 的等效式 R~v(B,x)～co 的形成词 B来求方程的可解性的必要条件,而绕过求函数 F(d,)的最简化析取范式的手绩。并且,基于文中的结果,可制定求时间逻辑方程的可解性的必要条件的算法,从而为解更加繁复的具有多个变目的时间逻辑方程或方程组的可解性问题提供机器化的基础。