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

• 作者: 段振华 王海洋 田聪
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 交替投影时序逻辑 范式 标记范式图 基于并发博弈结构的交替Büchi自动机 可满足性
• 年，卷（期）: 2018,（6）
• 所属期刊栏目: 形式化方法的理论基础专题
• 页码范围: 1635-1646
• 页数: 12页
• 分类号: TP311
• 字数: 5475字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005459

摘要

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