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的可满足性.

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

所属期刊栏目：29

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金61732013,61420106004National Natural Science Foundation of China 61732013,61420106004

在线出版日期：2018-07-12（万方平台首次上网日期，不代表论文的发表时间）

页数：共12页

页码：1635-1646