APTL公式的可满足性检查工具

交替投影时序逻辑(alternating projection temporal logic,简称APTL)公式简单易懂,表达能力强;不仅可以描述经典时序逻辑LTL可以描述的性质,而且可以描述与区间相关的顺序和循环性质以及开放系统和多智能体系统中与博弈相关的性质.在验证系统是否满足所给的APTL公式所描述的性质之前需要检查公式的可满足性.根据检查APTL公式的可满足性的方法,开发实现了工具APTL2BCG.具体细节如下:首先,利用公式P的范式构造P的标记范式图(labeled normal form graph,简称LNFG);然后,将LNFG转化为广义的基于并发博弈结构的交替Büchi自动机(generalized alternating Büchi automaton over concurrent game structure,简称GBCG);最后,将GBCG转化为基于并发博弈结构的交替Büchi自动机(alternating Büchi automaton over concurrent game structure,简称BCG)并且化为最简形式并检查公式P的可满足性.

一种命题投影时序逻辑的分布式模型检测方法

为缓解模型检测的状态空间爆炸问题,提出一种基于命题投影时序逻辑的分布式模型检测方法。通过标记范式图技术将命题投影时序逻辑公式描述的待验证性质转换为自动机;根据强连通分量将其状态空间划分为多个子自动机,将各个子自动机与层次语法图描述的待验证系统模型分发至验证服务器集群中,使用动态验证技术进行多机协同完成系统模型检测验证。实验结果表明,该方法和单机模型检测相比验证时间明显降低,且能够验证更复杂的系统。