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

来源：软件学报杂志2018年第6期北京时间：

作者：王海洋,段振华,田聪

单位：王海洋，西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071;ISN 国家重点实验室(西安电子科技大学), 陕西 西安 71007111,段振华，西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071;ISN 国家重点实验室(西安电子科技大学), 陕西 西安 71007102,田聪，西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071;ISN 国家重点实验室(西安电子科技大学), 陕西 西安 71007103

摘要：交替投影时序逻辑（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的可满足性.

关键词：交替投影时序逻辑;范式;标记范式图;基于并发博弈结构的交替Büchi自动机;可满足性

基金资助：国家自然科学基金（61732013，61420106004）