本人所在的西安电子科技大学计算理论与技术研究所（Institute of Computing Theory & Technology）长期从事投影时序逻辑、可信软件、人工智能等基础理论方面的研究，取得了丰硕的研究成果，在CCF A类期刊IEEE Transactions on Software Engineering（TSE），IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems（TCAD），IEEE Transactions on Knowledge and Data Engineering (TKDE)，CCF A类会议International Joint Conference on Artificial Intelligence（IJCAI），International Conference on Software Engineering（ICSE），International Conference on Automated Software Engineering（ASE），CCF B类期刊Theoretical Computer Science（TCS），Journal of Parallel and Distributed Computing（JPDC）发表学术论文数十篇，其中与本人相关的研究成果包括：

（1）建立了时空逻辑系统PPTL^SL

将分离逻辑与命题投影时序逻辑PPTL相结合，得到了时空逻辑PPTL^SL，并定义了相应的语法和语义，给出了重要的逻辑规则。如图1所示，在空间维度，PPTL^SL利用分离逻辑描述每个时间点的空间形态；在时间维度，PPTL^SL利用PPTL刻画时间演化的特征。因此，PPTL^SL能够描述空间形态随着时间的演化性质，这是一类在实际应用中较为常见的、典型的时空性质。提出了从PPTL_SL到其严格子集RPPTL^SL的等价可满足转换，进一步证明了RPPTL^SL能够重用PPTL的判定过程。在此基础上完成了PPTL^SL的可判定性证明，并给出了相应的判定过程。研究了PPTL^SL的判定复杂度，得出了它与PPTL的判定复杂度相同的重要结论。（以第一作者发表国际会议SOFL+MSVL 2013论文一篇：Integrating Separation Logic with PPTL）

图1：分离逻辑与PPTL结合示意图

（2）建立了基于时空逻辑PPTL^SL的程序验证方法

在时空逻辑PPTL^SL判定过程的基础上，结合范式图（Normal Form Graph，简称NFG）理论，给出了相应的模型检测方法，用于验证指针程序的内存演化性质，如图2所示。采用投影时序逻辑的可执行子集——建模、仿真和验证语言MSVL对指针程序进行建模，PPTL^SL描述程序应满足的内存演化性质，通过分别构造程序和性质的NFG，从而根据经典自动机理论检查二者的乘积NFG中是否存在反例，以说明程序是否满足性质。该方法已被成功应用于经典的并发程序以及小型Windows设备驱动例程的验证。（发表CCF B类国际期刊TCS一篇：Verify Heaps Via Unified Model Checking，国内期刊软件学报一篇：二维逻辑PPTL^SL的可满足性检查，国际会议COCOA 2016一篇：Using Unified Model Checking to Verify Heaps，均为第一作者）

图2：基于PPTL^SL和MSVL的模型检测方法

（3）建立了基于时空逻辑PPTL^SL的智能规划方法

首次将时空逻辑PPTL^SL应用于智能规划领域，提出了高效的规划算法。该算法利用PPTL^SL判定过程中的范式（Normal Form）转换技术，给出了进展算法（progression algorithm），并结合基本的前向搜索框架以及SMT（Satisfiability Modulo Theories）求解器Z3进行规划搜索，如图3所示。对于同时涉及时间和空间信息的一类规划问题来说，PPTL^SL适用于描述搜索过程应遵循的时空搜索控制信息，以引导整个规划过程，降低搜索空间。开发了相应的规划器，并选取学术界公认的国际规划竞赛中具有代表性的标准规划问题进行实验。实验结果表明，与国内外其它优秀的规划器相比，基于PPTL^SL的规划方法的效率较高，并且能够获得更优的规划解。（发表CCF A类国际会议IJCAI 2017论文一篇：Temporalising Separation Logic for Planning with Search Control Knowledge，CCF A类国际期刊TKDE论文一篇：Planning with Spatio-Temporal Search Control Knowledge，均为第一作者）

图3：基于PPTL^SL的规划搜索框架