有限域情景演算中时间推理的可判定性研究

针对情景演算中常用的实数时间函数方法，研究表明即使域中仅含有限对象，判定是否存在满足公式的可达情景也是不可判定的。作者提出基于时间自动机理论的替代方法，引入带受限后继状态公理和比较算子的时钟作为实值流，证明有限域基本动作理论的可达性问题可判定，并给出判定 Golog 程序成功执行动作序列的可判定过程。