改进的时空逻辑PPTL^SL及其时空推理方法研究

In many real-world problems of computer science and artificial intelligence, temporal and spatial information are both involved. How to build a powerful spatio-temporal theory which combines two-dimensional (temporal and spatial) information has been an important challenge. In this project, we are motivated to investigate a new spatio-temporal logic system which combines a spatial information based logic -- separation logic, and a temporal information based logic -- PPTL (Propositional Projection Temporal Logic). First, the spatio-temporal logic system supporting complex shape and data features will be studied, and the decidability of the logic will be proved. On this foundation, a dynamic model checking approach based on spatio-temporal logic will be established and implemented. It will be applied to verify memory+data evolution properties of large-scale pointer programs. Meanwhile, a concurrent planning method based on spatio-temporal logic will also be established and implemented. It will be applied to solve planning problems with durative actions and resource constraints. The spatio-temporal logic is used to describe the spatio-temporal resource search control knowledge to guide the planning process.

在计算机科学、人工智能等领域中，许多现实问题的解决都涉及时间和空间信息。如何结合时间和空间两方面的信息而构建一种表达能力更强的时空逻辑理论，成为重要的挑战性课题。本项目拟研究基于空间信息的分离逻辑和基于时间信息的命题投影时序逻辑（Propositional Projection Temporal Logic，简称PPTL）相结合的时空逻辑理论及其应用。首先，研究支持形态及数值复杂特性的时空逻辑系统，并研究该时空逻辑系统的判定性问题。在此基础上，研究基于时空逻辑的动态模型检测方法，并将其应用于大规模指针程序的内存+数据演化性质验证，以及基于时空逻辑的并发智能规划方法，并将其应用于带有持续性动作和资源约束的规划问题求解，利用时空资源搜索控制信息引导规划过程。

现实世界中，许多问题的解决都涉及时间和空间信息，如规划调度、地理信息系统、自治机器人导航、自然语言理解、时空数据库、计算机视觉等。目前针对时间和空间信息的研究工作已经分别有了丰富的积累，而时空结合的研究成果较少，因此时空推理成为当前各领域学者的研究重点。本项目旨在结合时间和空间两方面的信息，从而构建一种表达能力更强的时空逻辑系统，为求解时空问题提供理论和技术支撑。具体来说，本项目研究基于空间信息的分离逻辑和基于时间信息的命题投影时序逻辑相结合的时空逻辑理论及其应用。主要研究内容包括三个方面：首先，研究支持形态及数值复杂特性的时空逻辑系统，并研究该系统的判定性问题；其次，研究基于时空逻辑的动态模型检测方法，并将其应用于大规模指针程序的内存-数据演化性质验证，利用时空逻辑描述指针程序的关键属性；最后，研究基于时空逻辑的并发智能规划方法，并将其应用于带有持续性动作和资源约束的规划问题求解，利用时空资源约束搜索控制信息引导规划过程。在项目的资助下，经过三年的深入探索，取得了一定的学术进展。在智能规划领域：（1）提出了一种新的时空约束编码方法，使得时空约束和原有问题的模型相统一，该方法具有较强的可扩展性，可应用于智能交通控制；（2）提出了时空知识与启发式搜索相结合的方法，在保证规划解质量的同时进一步提高规划效率。在程序合成领域：（1）提出了基于分离逻辑的符号执行框架的指针程序合成方法，可用于简单链表程序的自动合成；（2）提出了一种利用非确定规划的LTL合成方法，通过智能规划技术求解LTL合成问题。在模型检测领域：提出了将模型检测问题转换为智能规划问题的方法，从而提高反例质量。