软件学报  2018, Vol. 29 Issue (6): 1635-1646   PDF    
APTL公式的可满足性检查工具
王海洋1,2, 段振华1,2, 田聪1,2     
1. 西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071;
2. ISN 国家重点实验室(西安电子科技大学), 陕西 西安 710071
摘要: 交替投影时序逻辑(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自动机     可满足性    
Tool for Checking Satisfiability of APTL Formulas
WANG Hai-Yang1,2, DUAN Zhen-Hua1,2, TIAN Cong1,2     
1. Institute of Computing Theory and Technology, Xidian University, Xi'an 710071, China;
2. State Key Laboratory of Integrated Service Networks(Xidian University), Xi'an 710071, China
Foundation item: National Natural Science Foundation of China (61732013, 61420106004)
Abstract: Alternating projection temporal logic (APTL) has a concise syntax with strong expressive power. It is able to express not only properties specified in classical temporal logic LTL, but also interval related sequential and periodical properties, as well as game related properties of open systems and multi-agent systems. To verify whether a system satisfies an APTL formula, the satisfiability of the APTL formula should be checked. In this paper, based on the method for checking satisfiability of an arbitrary APTL formula provided, a supporting tool APTL2BCG has been developed. The details of implementation are given as follows. Firstly, LNFG of P is constructed according to the normal form of the formula P. Then, the LNFG is transformed to a generalized alternating Büchi automaton over concurrent game structure (GBCG). Finally, the alternating Büchi automaton is developed over concurrent game structure (BCG) from the obtained GBCG, and the BCG is simplified for checking the satisfiability of the formula P.
Key words: alternating projection temporal logic     normal form     LNFG (labeled normal form graph)     BCG (alternating Büchi automaton over concurrent game structure)     satisfiability    

基于区间的交替时序逻辑在文献[1]中提出, 其中包括交替区间时序逻辑(alternating interval temporal logic, 简称AITL)和交替投影时序逻辑(alternating projection temporal logic, 简称APTL)[2, 3].APTL是由命题投影时序逻辑(propositional projection temporal logic, 简称PPTL)[4]扩展得到的, 并且是在AITL中引入投影操作符prj得到的, 因此, APTL也是AITL的扩展逻辑.时序逻辑是形式化验证的关键元素之一, Pnueli于1977年提出了线性时序逻辑(linear temporal logic, 简称LTL)[5]用于规约系统的线性时序性质.LTL公式描述的是系统的任意一次运行中的状态以及它们之间的关系.

Clarke和Emerson于1980年提出了分支时序逻辑, 即计算树逻辑(computation tree logic, 简称CTL)[5], CTL公式不仅可描述系统中状态的先后关系, 而且可描述系统存在一条路径和任意一条路径满足的性质.经典逻辑LTL, CTL存在局限性, 如无法描述某些循环和并发的性质.区间时序逻辑(interval temporal logic, 简称ITL)[4]和投影时序逻辑(projection temporal logic, 简称PTL)[2, 6]可方便地描述系统的顺序、循环性质, 另外, PTL公式还可方便地描述系统的并发性质.为了描述开放系统和多智能体系统中合作及博弈相关的性质, 文献[1]中提出了APTL.APTL公式不仅可以描述经典时序逻辑LTL可以描述的性质, 而且可以描述与区间相关的顺序和循环性质以及开放系统和多智能体系统中与博弈相关的性质.多智能体系统是现阶段各领域的研究热点, 并得到了广泛应用.比如人工智能、竞拍.验证多智能体是否满足人们所期望的性质, 是人工智能中面临的关键问题之一, APTL可用于描述多智能体系统的各种性质.

APTL中包括chop和projection时序操作符, 使得APTL公式可方便地描述系统的顺序和并发性质.例如, 智能体集合A使得p在第10和第16个状态之间成立, 可用APTL公式表示为

$ len\left( {10} \right){;_{ \ll \emptyset \gg }}len\left( 6 \right) \wedge {\diamondsuit _{ \ll A \gg }}p{;_{ \ll \emptyset \gg }}{\rm{true}}. $

对于APTL公式$({P_1}, ..., {P_m})pr{j_{ \ll A \gg }}Q$, 公式${P_1}{; _{ \ll A \gg }}...{; _{ \ll A \gg }}{P_m}$Q是相对独立的, 每一个公式对应一个区间模型; 公式Q与公式${P_1}{; _{ \ll A \gg }}...{; _{ \ll A \gg }}{P_m}$的模型是并行的, 他们只是在特定的汇合点上通信, 而且两个公式可能在不同的时间点结束.

判断公式的可满足性是程序验证过程中不可或缺的一个环节, 根据文献[1]中给出的APTL公式的可满足性检查方法, 开发实现了检查工具APTL2BCG.具体细节如下:首先, 将给定的APTL公式转化为范式, 构造标记范式图(labeled normal form graph, 简称LNFG); 然后, 将LNFG转化为对应的GBCG, 并将GBCG转化为BCG; 最后, 根据本文给出的BCG的化简方法将BCG化为最简形式, 检查BCG是否为空, 得出公式是否可满足.

本文第1节介绍APTL的语法语义.第2节详细描述工具APTL2BCG的框架和实现过程.第3节展示工具效果.第4节总结全文并展望将来的工作.

1 基础概念 1.1 APTL语法语义

语法.令$\mathcal{P}$为原子命题的可数集合, $\mathcal{A}$为代理的可数集合.APTL的语法定义如下:

$P:: = p|\neg P|P \vee Q|{\bigcirc _{ \ll A \gg }}P|({P_1}, ..., {P_m})pr{j_{ \ll A \gg }}Q, $

其中, p$\mathcal{P}$, A$\mathcal{A}$, Pi(i=1, …, m), PQ为APTL公式, ${\bigcirc _{ \ll A \gg }}$(next)及${prj _{ \ll A \gg }}$(projection)是基本的时序操作符.

语义. APTL公式的语义是在并发博弈结构(concurrent game structure, 简称CGS)[1, 7]的基础上定义的, CGS是七元组C=〈$\mathcal{P}$, $\mathcal{A}$, S, S0, l, Δ, τ〉, 详细的解释见文献[1].

根据CGS的定义, 在$\mathcal{P}$上定义了一个状态s, 是$\mathcal{P}$B={true, false}的投影, s:$\mathcal{P}$B.在CGS中, 以状态s为起始节点的一条执行路径λ(s)满足APTL公式P, 标记为λ(s)$ \models $P.CGS C满足APTL公式P当且仅当所有以CGS的初始节点为起为接收状态集始节点的执行序列满足公式P, 标记为C$ \models $P.

$ \models $关系定义如下:

λ(s)$ \models $p当且仅当命题p$\mathcal{P}$pl(s);

λ(s)$ \models \neg $P当且仅当λ(s)$\nvDash $P;

λ(s)$ \models $P$\vee $Q当且仅当λ(s)$ \models $Pλ(s)$ \models $Q;

$\lambda (s)\vDash {{\bigcirc }_{\ll A\gg }}P$当且仅当|λ(s)|≥2, 并且A存在一个策略fA, 使得λ(s)∈out(s, fA)并且λ(s)[1, |λ|]$ \models $P;

$\lambda (s)\vDash ({{P}_{1}}, \ldots, {{P}_{m}})pr{{j}_{\ll A\gg }}Q$当且仅当A存在一个策略fA, λ(s)∈out(s, fA), 0=r0r1≤…≤rm≤|λ(s)|, 使得λ(s)[ri-1, ri]$ \models $Pi, 0 < im并且λ$ \models $Q.λ有以下两种情况得到.

a) rm < |λ(s)|, 那么λ=λ(s)↓(r0, …, rmλ(s)[rm+1, …, |λ(s)|];

b) rm=|λ(s)|, 那么λ=λ(s)↓(r0, …, rm).

1.2 交替Büchi自动机

基于并发博弈结构的自动机在文献[1, 8]中已经介绍, 本节简单介绍了交替Büchi自动机[9]的定义.在计算中, 传统的自动机只包含存在性迁移关系, 交替自动机[10]包含了存在性迁移关系和全局性迁移关系.

定义(交替Büchi自动机).交替Büchi自动机(alternating Büchi automaton)是一个五元组A=(P, Q, q0, δ, F), 其中, $\mathcal{P}$为有穷字母表, Q为有穷状态集合, q0为初始状态, F∈2Q为接收状态集合, δ:Q×$\mathcal{P}$$\mathit{\mathbb{B}}$+(Q)为迁移函数.由于交替自动机中有全局性迁移关系, 所以交替Büchi自动机读入一个字生成无穷树而不是无穷序列.如图 1所示为一个交替自动机({a, b}, {s, p, q}, s, δ, {p}), 其中, 从状态s出发的两个标记有b的迁移为全局性迁移关系, 即:图中加粗的两条边为全局性迁移, 其他都是选择性迁移关系.给定一个字abbab…, 自动机读入该字的一个生成树如图 2所示.

Fig. 1 An alternating automaton 图 1 交替自动机

Fig. 2 A spanning tree of the automaton in Fig. 1 on the word abbab 图 2 图 1中的自动机读入字abbab…的一个生成树

如果生成树中的每一条分支都满足Büchi条件, 那么这个生成树是被接收的.一个字是被交替Büchi自动机接收的当且仅当存在一个可接收的生成树.

2 原型工具 2.1 工具框架

我们开发了检查APTL公式的可满足性的原型工具APTL2BCG, 该工具是基于Windows平台采用C++语言开发的, 工具架构如图 3所示.

Fig. 3 Architecture of APTL2BCG 图 3 APTL2BCG的架构

APTL2BCG主要包括以下几个模块, 分别是词法分析与语法树构造模块、预处理模块、转化范式模块、构造LNFG[1]模块、转化GBCG[1]模块、将GBCG转化为BCG[1]模块、BCG化简模块, 根据得到的BCG是否为空检查公式的可满足性.该工具以APTL公式作为输入, 格式为文本文件.在该文件中, 公式的各操作符的表示方法如下:!表示$\neg $, |和 & 分别表示$\vee $$\wedge $, ()表示○, < > 表示$\diamond $, []表示□, < < > > 表示$\ll \gg $.例如, 公式${{\bigcirc }_{\ll A\gg }}P\wedge {{\diamond }_{\ll B\gg }}\neg Q$表示为$() < < A>>P\And < > < < B>>!Q$.

检查APTL公式ϕ的可满足性的具体过程是:

●  首先, 对输入的公式ϕ进行词法分析, 词法无误则构造语法树, 对公式进行预处理;

●  然后, 构造公式的LNFG, 构造过程需要不断的调用范式转化模块将产生的新节点转化为范式, 并据此生成新的节点和边, 直到所有的节点表示的子公式均已被处理;

●  接着, 将LNFG转化为GBCG;

●  最后, 将GBCG转化为BCG并化简, 接着检查最简BCG是否为空:如果BCG为空, 则公式ϕ不可满足; 反之亦然.

在检查公式的可满足性时, 将公式以文本形式输入, 在检查过程中输出描述LNFG, GBCG和BCG的文本文档, 文本格式是工具Graphviz的输入文本的格式, 调用Graphviz工具可将LNFG, GBCG和BCG的图输出, 最后输出公式的可满足性.

2.2 语法树构造

在构造BCG的过程中, 针对节点和边的操作都是在语法树的概念上进行的, CTreeNode(NODETYPE ptype, int typeofAgentset, string agentstr, string pstr, int istr, CTreeNode *s1, CTreeNode *s2, CTreeNode *s3)表示树节点.其中, ptype为节点类型, 如节点类型为CHOP, 则以该节点为根的子树表示的是chop类型的公式; 节点类型为PROJECTION, 则以该节点为根的子树表示的是prj类型的公式, 等等.typeofAgentset表示代理集合的类型, 其中: 1代表 <<>>, <<A>>?表示无论其他代理采取什么策略, 集合A中的代理总能使得公式成立; 2代表[[]], [[A]]表示集合A中的代理无论采取什么策略都不能使公式不成立.agentstr表示代理的字符串, pstr是该节点的字符串, istr为该节点的整数值, s1, s2, s3分别为该节点的3个孩子节点.没有孩子节点的节点表示为CTreeNode(NODETYPE ptype, int typeofAgentset, string agentstr, string pstr, int istr), 如果树节点有一个孩子节点那么s2s3为空, 类似的有两个孩子节点的树节点的s3为空.部分APTL公式的语法树结构如图 4所示.

Fig. 4 Syntax trees of APTL formulas 图 4 APTL公式的语法树

图 4可以看出, 语法树的根节点能够表示相应的公式类型.true, false, empty, skip以及原子命题的语法树均不含孩子节点.公式$\neg $p, fin(n), len(n)的语法树均含有一个孩子节点, 分别为p, n, n.在公式p$\vee $q(或p$\wedge $q)的语法树中, 左右孩子节点分别对应公式的左右析取项(或合取项).${{\bigcirc }_{\ll A\gg }}p, {{\diamond }_{\ll A\gg }}p$${{\square }_{\ll A\gg }}p$的语法树的根节点均表示节点的类型和代理集合, 而且均只有一个孩子节点p.公式$p{{; }_{\ll A\gg }}q$的语法树的左右孩子分别为pq.公式(p1, p2, p3, …)$pr{{j}_{\ll A\gg }}q$的语法树有3个孩子节点, 分别对应p1, p2, p3, …和q.

2.3 公式的预处理

由于输入的APTL公式本身可能存在冗余的情况, 因此要先经过预处理过程对输入的合法的APTL公式进行等价化简.预处理函数的伪代码如函数PRE(CtreeNode *ptree)所示, 对公式的预处理过程是在语法树上进行的.其中, 输入的是待处理公式的语法树, 输出化简后的公式的语法树.

2.4 BCG构造

任意一个合法的APTL公式都可以构造相应的BCG.首先, 根据文献[1]中的算法, 实现了将APTL公式转化为LNFG的过程, 并将LNFG转化为相应的GBCG; 然后, 将GBCG转化为对应的BCG.

void PRE(CtreeNode *ptree){

if (ptree==NULL) return;

switch(ptree){

case PQ

   ptree$\neg $P$\vee $Q;

case PQ

   ptree$\neg $P$\wedge $$\neg $Q$\vee $P$\wedge $Q;

case $\neg $$\neg $P

   ptreeP;

case skip

   ptree $\leftarrow {{\bigcirc }_{\ll \varnothing \gg }}{\varepsilon}$;

case $\neg $ ε

   ptree $\leftarrow \bigcirc _{\ll \varnothing \gg }^{n}\text{true} $;

case len(n)

   ptree $\leftarrow \bigcirc _{\ll \varnothing \gg }^{n}\varepsilon $;

case ${{\diamond }_{\ll A\gg }}P$

   ptree $\leftarrow \text{true}{{; }_{\ll A\gg }}P$;

case P$\wedge $Q

 if P==true

   ptreeQ;

    if $P==\varepsilon \wedge Q=={{\bigcirc }_{\ll A\gg }}{Q}'$

 ptree←false;

case P$\vee $Q

  if P==Q

   ptreeP;

  if P==tru$\vee $Q==true

   ptree←true;

if Q==false

   ptreeP;

   }

       }

构造LNFG模块通过循环调用函数NF来构造公式的LNFG.函数NF(CtreeNode *ptree)将APTL公式转化为范式, 其中输入的是APTL公式的语法树, 得到APTL公式的范式的语法树.构造APTL公式的范式图的函数为LNFG(CtreeNode* ptree, CGraph* pgraph), 其中, ptree为公式的范式的语法树, pgraph为生成的LNFG.

给定一个LNFG G=(Q, q0, $\mathcal{A}$, δ, ε, $ \mathit{\mathbb{L}}$={$\mathit{\mathbb{L}}$1, …, $\mathbb{L}$m})存在一个GBCG $GB=({Q}', {{{q}'}_{0}}, {\mathcal{A}}', {\delta }', F=\{{{F}_{1}}, ..., {{F}_{n}}\})$与之相对应.其中, ${Q}'=Q, {{{q}'}_{0}}={{q}_{0}}, {\mathcal{A}}'=\mathcal{A}, {\delta }'=\delta \cup \delta (d, \varepsilon)=(\ll \varnothing \gg, d), F=\{\mathbb{L}_{1}^{\sim }, ..., \mathbb{L}_{m}^{\sim }\}.$

任意一个GBCG GB=($\mathcal{P}$, $\mathcal{A}$, Q, q0, δ, F={F1, …, Fn})都可以转化为一个BCG $B=(\mathcal{P}, \mathcal{A}, {Q}', {{{q}'}_{0}}, {\delta }', {F}')$, 根据文献[11]中的方法, 实现了将GBCG转化为BCG的过程.如果GB的接收集合F中只有一个接收状态子集, 也就是说, F={F1}, 则无需转换, 该GBCG即为BCG, 那么对应的BCG的接收集合为F'=F1.如果n≥2, 将GB的状态复制n遍, 第iGB中的非接收状态与第iGB中的相应状态相连接, 第iGBFi的状态与第i+1个GB中相应的状态相连接.得到的B的接收集合F中的状态是第1个GB中的接收集合的F1中的状态.B的接收条件是F中的一个状态无穷次的出现, 根据该BCG B的构造过程, 能推出所有的接收状态集Fi都能够被无穷次地访问到.

将一个GBCG GB=($\mathcal{P} $, $\mathcal{A} $, Q, q0, δ, F={F1, …, Fn})转化为BCG $B=(\mathcal{P}, \mathcal{A}, {Q}', {{{q}'}_{0}}, {\delta }', {F}')$的伪代码如下所示.

void BCG(CGraph *GBCG, CGraph *BCG){

Q'←Q×{1, …, n};

${{{q}'}_{0}}\leftarrow < {{q}_{0}}, 1>$;

F'←{ < qF, 1 > |qFF1};

 if qFi

δ'(< q, i > , p, A')←{ < q', i > |q'∈δ(q, p, A')};

  else if qFi

δ'(< q, i > , p, A')←{ < q', i+1 > |q'∈δ(q, p, A')};

}

例子:通过构造公式$p{{; }_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{; }_{\ll b\gg }}{{\square }_{\ll b\gg }}r$的BCG过程, 讲解给定一个APTL公式构造BCG的具体细节.以下是构造公式$p{{; }_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{; }_{\ll b\gg }}{{\square }_{\ll b\gg }}r$的LNFG的过程.

首先, 我们将公式写为$p\wedge fin({{l}_{1}}){{; }_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{; }_{\ll b\gg }}{{\square }_{\ll b\gg }}r$并转化为范式;

$ \begin{align} &p\wedge fin({{l}_{1}}){{;}_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{;}_{\ll b\gg }}{{\square }_{\ll b\gg }}r\equiv p\wedge q\wedge r\wedge {{l}_{1}}\wedge \varepsilon \vee p\wedge q\wedge r\wedge {{l}_{1}}\wedge {{\bigcirc }_{\ll b\gg }}{{\square }_{\ll b\gg }}r\vee p\wedge {{l}_{1}}\wedge q\wedge \\ &\text{ }{{\bigcirc }_{\ll a\gg }}({{\square }_{\ll a\gg }}q{{;}_{\ll b\gg }}{{\square }_{\ll b\gg }}r)\vee p\wedge {{\bigcirc }_{\ll \varnothing \gg }}(fin({{l}_{1}}){{;}_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{;}_{\ll b\gg }}{{\square }_{\ll b\gg }}r); \\ \end{align} $

接着, 将新生成的APTL公式${{\square }_{\ll b\gg }}r, {{\square }_{\ll a\gg }}q{{; }_{\ll b\gg }}{{\square }_{\ll b\gg }}r$$fin({{l}_{1}}){{; }_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{; }_{\ll b\gg }}{{\square }_{\ll b\gg }}r$转化为范式;

$\begin{align} &{{\square }_{\ll b\gg }}r\equiv r\wedge \varepsilon \vee r\wedge {{\bigcirc }_{\ll b\gg }}{{\square }_{\ll b\gg }}r \\ &{{\square }_{\ll a\gg }}q\wedge fin({{l}_{2}}){{;}_{\ll b\gg }}{{\square }_{\ll b\gg }}r\equiv q\wedge r\wedge {{l}_{2}}\wedge \varepsilon \vee q\wedge r\wedge {{l}_{2}}\wedge {{\bigcirc }_{\ll b\gg }}{{\square }_{\ll b\gg }}r\vee q\wedge \\ &\text{ }{{\bigcirc }_{\ll a\gg }}({{\square }_{\ll a\gg }}q{{;}_{\ll b\gg }}{{\square }_{\ll b\gg }}r)\wedge q\wedge {{\bigcirc }_{\ll \varnothing \gg }}(fin({{l}_{2}}){{;}_{\ll b\gg }}{{\square }_{\ll b\gg }}r) \\ &fin({{l}_{1}}){{;}_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{;}_{\ll b\gg }}{{\square }_{\ll b\gg }}r\equiv q\wedge r\wedge {{l}_{1}}\wedge \varepsilon \vee q\wedge r\wedge {{l}_{1}}\wedge {{\bigcirc }_{\ll b\gg }}{{\square }_{\ll b\gg }}r\vee q\wedge {{l}_{1}}\wedge \\ &\text{ }{{\bigcirc }_{\ll a\gg }}({{\square }_{\ll a\gg }}q{{;}_{\ll b\gg }}{{\square }_{\ll b\gg }}r)\vee {{\bigcirc }_{\ll \varnothing \gg }}(fin({{l}_{1}}){{;}_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{;}_{\ll b\gg }}{{\square }_{\ll b\gg }}r); \\ \end{align}$

然后, 将生成的新的APTL公式$fin({{l}_{2}}){{; }_{\ll b\gg }}{{\square }_{\ll b\gg }}r$转化为范式;

$ fin({{l}_{2}}){{;}_{\ll b\gg }}{{\square }_{\ll b\gg }}r\equiv {{l}_{2}}\wedge r\wedge \varepsilon \vee {{l}_{2}}\wedge r\wedge {{\bigcirc }_{\ll b\gg }}{{\square }_{\ll b\gg }}r\vee {{\bigcirc }_{\ll \varnothing \gg }}(fin({{l}_{2}}){{;}_{\ll b\gg }}{{\square }_{\ll b\gg }}r); $

最后, 根据公式的NF构造LNFG.

公式$p{{; }_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{; }_{\ll b\gg }}{{\square }_{\ll a\gg }}r$的LNFG如图 5所示.

Fig. 5 LNFG of formula $p{{; }_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{; }_{\ll b\gg }}{{\square }_{\ll b\gg }}r$ 图 5 公式$p{{; }_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{; }_{\ll b\gg }}{{\square }_{\ll b\gg }}r$的LNFG

节点1表示公式$p\wedge fin({{l}_{1}}){{; }_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{; }_{\ll b\gg }}{{\square }_{\ll a\gg }}r; $

节点2表示${{\square }_{\ll b\gg }}r; $

节点3表示${{\square }_{\ll a\gg }}q\wedge fin({{l}_{2}}){{; }_{\ll b\gg }}{{\square }_{\ll b\gg }}r; $

节点4表示$fin({{l}_{1}}){{; }_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{; }_{\ll b\gg }}{{\square }_{\ll b\gg }}r; $

节点5表示$fin({{l}_{2}}){{; }_{\ll b\gg }}{{\square }_{\ll b\gg }}r; $

节点6表示empty.

图 5中的LNFG转化为GBCG, 如图 6所示.其中, 节点1为初始节点, 节点1、节点4标记有l1, 节点3、节点5标记有l2, 接收集合为F={F1={2, 3, 5, 6}, F2={1, 2, 4, 6}}.

Fig. 6 GBCG of formula $p{{; }_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{; }_{\ll b\gg }}{{\square }_{\ll b\gg }}r$ 图 6 公式$p{{; }_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{; }_{\ll b\gg }}{{\square }_{\ll b\gg }}r$的GBCG

图 6的GBCG转化为BCG如图 7所示, 其中, 状态(1, 1)为初始状态, 接收集合为F'={(2, 1), (3, 1), (5, 1), (6, 1)}.

Fig. 7 BCG of formula $p{{; }_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{; }_{\ll b\gg }}{{\square }_{\ll b\gg }}r$ 图 7 公式$p{{; }_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{; }_{\ll b\gg }}{{\square }_{\ll b\gg }}r$的BCG

2.5 BCG的化简及检查

为了检查APTL公式的可满足性, 必须将得到的BCG进行化简, 因此, 我们给出了化简BCG的算法SIMPLIFY.对于一个BCG, 可能存在没有后继节点的节点或者存在没有出边的非接收状态节点, 这些多余的节点和边应该被删除.由于交替自动机中存在一些全局的迁移关系, 也就是说存在从同一个节点出发的多条边应同时满足相应的性质, 所以做完以上删除操作后, 可能会产生非初始节点入度为0的节点, 这些节点也应该被删除, 具体过程如下.

SIMPLIFY(B).

输入:APTL公式φ的BCG B=($\mathcal{P}$, $\mathcal{A}$, Q, q0, δ, F);

输出:SIMPLIFY(B)计算出一个φ的最简BCG ${B}'=({\mathcal{P}}', {\mathcal{A}}', {Q}', {{{q}'}_{0}}, {\delta }', {F}')$.

B'=B;

while $\exists $qQ'且节点q没有出边或者q为非接收节点且没有出边从q节点到其他节点

do (Q'=Q'\q;

${\delta }'={\delta }'\backslash \bigcup\nolimits_{i}{({{q}_{i}}, {{p}_{i}}, {{A}_{i}}, q)}$;           /*$\bigcup\nolimits_{i}{({{q}_{i}}, {{p}_{i}}, {{A}_{i}}, q)}$表示节点qi到节点q的连边集合*/

  for each i

${\delta }'={\delta }'\backslash \bigcup\nolimits_{j}{({{q}_{i}}, {{p}_{i}}, {{A}_{j}}, {{r}_{j}})}$;

/*$\bigcup\nolimits_{j}{({{q}_{i}}, {{p}_{i}}, {{A}_{j}}, {{r}_{j}})}$表示边的集合, 在APTL公式的范式中, 存在${{p}_{i}}\wedge {{\bigcirc }_{\ll {{A}_{i}}\gg }}{{R}_{{{q}_{i}}}}\wedge {{\bigcirc }_{\ll {{A}_{j}}\gg }}{{R}_{{{r}_{j}}}}$, 其中, 节点qirj分别由公式${{R}_{{{q}_{i}}}}$${{R}_{{{r}_{j}}}}$标记*/

  if qF' then

F'=F'\q;

)

end while

while $\exists $qQ'并且q不是初始节点, 入度为0

do (Q'=Q'\q;

${\delta }'={\delta }'\backslash \bigcup\nolimits_{j}{\bigcup\nolimits_{i}{(q, {{p}_{i}}, {{A}_{i}}, {{r}_{j}})}}$;        /*$\bigcup\nolimits_{j}{\bigcup\nolimits_{i}{(q, {{p}_{i}}, {{A}_{i}}, {{r}_{j}})}}$为连接节点q的边*/

)

end while

return B';

图 7中的BCG化简得到最简BCG, 如图 8所示, 其中接收集合为F={(2, 1), (3, 1), (5, 1), (6, 1)}.

Fig. 8 BCG of formula $p{{; }_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{; }_{\ll b\gg }}{{\square }_{\ll b\gg }}r$ 图 8 公式$p{{; }_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{; }_{\ll b\gg }}{{\square }_{\ll b\gg }}r$的BCG

图 8中的最简BCG不为空, 所以公式$p{{; }_{\ll a\gg }}{{\square }_{\ll a\gg }}q{{; }_{\ll b\gg }}{{\square }_{\ll b\gg }}r$是可满足的.

通过检查化简后的BCG是否为空, 来判断对应的APTL公式的可满足性.检查任意一个APTL公式的可满足性过程如算法CHECK所示, 其中, 函数LNFG构造APTL公式P的LNFG, 函数TR将公式的LNFG转化为GBCG, 函数BCG将公式的GBCG转化为BCG, 函数SIMPLIFY对生成的BCG进行化简.

CHECK(P).

输入:APTL公式P;

输出:公式P是否可满足.

G=LNFG(P);       /*构造公式P的LNFG G*/

GB=TR(G);       /*将LNFG G转化为GBCG GB */

BCG(GB, B);       /*将GBCG GB转化为BCG B*/

G'=SIMPLIFY(B);

if G'为空

return  不可满足;

else return  可满足;

3 工具展示 3.1 实例展示

本节通过检查哲学家就餐问题需要满足性质的可满足性, 展示工具APTL2BCG的工作效果.哲学家围坐在一张圆桌旁, 每人面前各摆放一碗面条, 每两位哲学家之间只摆放一支筷子, 哲学家的行为是反复地吃饭和思考.当哲学家饥饿时, 他必须能够同时拿起左、右两支筷子才能吃到面条, 餐后放下两支筷子继续考虑.i是哲学家的编号(比如有5位哲学家, 那么1≤i≤5), 每个哲学家存在以下5种状态:哲学家i思考表示为i_Thk, 哲学家i处于饥饿状态表示为i_Hug, 哲学家i拿筷子表示为i_Tch, 哲学家i吃饭表示为i_Eat, 哲学家i放下筷子表示为i_Pch.哲学家的行为构成循环, 依次是思考、感觉到饥饿后准备拿筷子、当两边的筷子都闲置的时候拿起筷子、接着吃饭、吃完后放下筷子, 继续思考, 依次循环下去.

哲学家i总能吃到面条, 不会出现一直饥饿的情况用APTL公式表示为${{\square }_{\ll i\gg }}{{\diamond }_{\ll i\gg }}i\_Eat$.以哲学家1为例, 用工具APTL2BCG检查公式${{\square }_{\ll 1\gg }}{{\diamond }_{\ll 1\gg }}1\_Eat$的可满足性, 为了使输出的BCG简单明了, 令p=i_Eat, 将公式[]$\ll 1\gg<>\ll 1\gg $p输入, 得出的最简BCG如图 9所示, BCG不为空, 表示公式${{\square }_{\ll 1\gg }}{{\diamond }_{\ll 1\gg }}1\_Eat$是可满足的.

Fig. 9 BCG of formula ${{\square }_{\ll 1\gg }}{{\diamond }_{\ll 1\gg }}p$ 图 9 公式${{\square }_{\ll 1\gg }}{{\diamond }_{\ll 1\gg }}p$的BCG

哲学家在吃面条后需要放下筷子接着再思考, 以免相邻的哲学家拿不到筷子.以哲学家1为例, 哲学家1吃完面条就放下筷子用APTL公式表示为:${{\square }_{\ll \varnothing \gg }}(fin(1\_Eat){{; }_{\ll 1\gg }}{{\bigcirc }_{\ll 1\gg }}1\_Pch)$.令p代表 1_Eat, q代表 1_Pch, 检查公式${{\square }_{\ll \varnothing \gg }}(fin(p){{; }_{\ll 1\gg }}{{\bigcirc }_{\ll 1\gg }}q)$的可满足性.将公式[]$\ll \gg $(fin(p);$\ll 1\gg \left( {} \right)\ll 1\gg $q)输入到工具APTL2BCG中, 得到如图 10所示的BCG, 表明公式${{\square }_{\ll \varnothing \gg }}(fin(1\_Eat){{; }_{\ll 1\gg }}{{\bigcirc }_{\ll 1\gg }}1\_Pch)$是可满足的.

Fig. 10 BCG of formula ${{\square }_{\ll \varnothing \gg }}(fin(p){{; }_{\ll 1\gg }}{{\bigcirc }_{\ll 1\gg }}q)$ 图 10 公式${{\square }_{\ll \varnothing \gg }}(fin(p){{; }_{\ll 1\gg }}{{\bigcirc }_{\ll 1\gg }}q)$的BCG

3.2 实验与分析

本节通过检查3类APTL公式的可满足性, 展示工具APTL2BCG的实用性和工作效率.对以下3类公式进行可满足性检查:

$len(n)\wedge {{\diamond }_{\ll A\gg }}p$ (1)
$ {{\diamond }_{\ll A\gg }}{{P}_{1}}{{;}_{\ll A\gg }}{{\diamond }_{\ll A2\gg }}{{P}_{2}}{{;}_{\ll A\gg }}\cdots {{;}_{\ll A\gg }}{{\diamond }_{\ll An\gg }}{{P}_{n}} $ (2)
$ \left( {{P}_{1}}, \ldots {{P}_{n}} \right)pr{{j}_{\ll A\gg }}Q $ (3)

我们用工具APTL2BCG检查以上3类公式的可满足性, 其中,

●  路径λ满足公式(1)当且仅当智能体集合A的策略使得λ[i]$\vDash $p(0≤in)成立;

●  路径λ满足公式(2)当且仅当智能体A的策略使得公式${{\diamond }_{\ll A1\gg }}{{P}_{1}}, {{\diamond }_{\ll A2\gg }}{{P}_{2}}, ..., {{\diamond }_{\ll An\gg }}{{P}_{n}}$在路径上顺序成立, 其中, ${{\diamond }_{\ll A1\gg }}{{P}_{1}}$表示智能体A1的策略使得P1在区间内可满足;

●  路径λ满足公式(3)当且仅当智能体集合A的策略使得性质P1, P2, …, Pn依次在路径上成立, 并且使得性质Q成立, 公式${{P}_{1}}{{; }_{\ll A\gg }}{{P}_{2}}{{; }_{\ll A\gg }}...{{; }_{\ll A\gg }}{{P}_{n}}$与公式Q是相对独立的, 他们的模型是并行的只是在特定的汇合点通信.

实验环境为2.93GHz, Intel(R) Core(TM) i7 CPU 870, 8G内存PC.实验结果见表 1.在表 1中,

Table 1 Experimental results 表 1 实验结果

●  第1列表示公式中n的大小;

●  节点数和边数所在列分别表示生成的相应公式的BCG的节点数和边数, 单位为个;

●  内存所在列表示程序运行时占用的内存, 单位为kb;

●  时间所在列表示判断公式的可满足性所需时间, 单位为s.

表 1的实验结果显示:n的取值在一定范围时, 此3类公式随着n的增大, 生成的BCG的节点数、边数和所用内存空间都是线性增长.对于公式(2)和公式(3), 随着公式中n的增大增长迅速.

但是实验结果看, 工具APTL2BCG的实际应用效果比较好, 有较好的实用性.

4 结论

APTL作为一种语法简洁、表达能力强的逻辑, 其可用于规约多智能体系统的性质.APTL公式的可满足性检查是系统验证的前提, 本文开发了APTL公式的可满足性检查工具APTL2BCG.检查过程是:首先, 利用APTL公式的范式、LNFG以及GBCG构造公式的BCG; 然后, 化简BCG并检查其是否为空, 得出公式是否可满足.

此外, 本文通过实验展示了APTL2BCG在实践中的可用性和实用性.未来将进一步优化检查工具APTL2BCG, 并在此基础上开发基于BCG的APTL模型检测工具.

参考文献
[1]
Tian C, Duan ZH. Alternating interval based temporal logics. In: Proc. of the ICFEM. 2010. 694-709. [doi:10.1007/978-3-642-16901-4_45]
[2]
Duan ZH. Temporal Logic and Temporal Logic Programming. Beijing: Science Press, 2005.
[3]
Wang HY, Duan ZH, Tian C. Symbolic model checking for alternating projection temporal logic. In: Proc. of the COCOA. 2015. 481-495. [doi:10.1007/978-3-319-26626-8_35]
[4]
Duan ZH, Tian C, Zhang L. A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica, 2008, 45(1): 43–78. [doi:10.1007/s00236-007-0062-z]
[5]
Baier C, Katoen JP. Principles of Model Checking. Cambridge: MIT Press, 2008.
[6]
Duan ZH, Tian C. A practical decision procedure for propositional projection temporal logic with infinite models. Theoretical Computer Science, 2014, 554: 169–190. [doi:10.1016/j.tcs.2014.02.011]
[7]
Alur R, Henzinger TA, Kupferman O. Alternating-Time temporal logic. JACM, 2002, 49: 672–713. [doi:10.1145/585265.585270]
[8]
Schewe S, Finkbeiner B. Satisfiability and finite model property for the alternating-time Mu-calculus. In: Proc. of the CSL. 2006. 591-605. [doi:10.1007/11874683_39]
[9]
[10]
Manna Z, Sipma H. Alternating the Temporal Picture for Safety. In: Proc. of the ICALP. 2000. 429-450. [doi:10.1007/3-540-45022-X_37]
[11]
Gastin P, Oddoux D. Fast LTL to Buchi Automata Translation. In: Proc. of the CAV. 2001. 53-65. [doi:10.1007/3-540-44585-4_6]