2. ISN 国家重点实验室(西安电子科技大学), 陕西 西安 710071
2. State Key Laboratory of Integrated Service Networks(Xidian University), Xi'an 710071, China
基于区间的交替时序逻辑在文献[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公式
判断公式的可满足性是程序验证过程中不可或缺的一个环节, 根据文献[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语法语义语法.令
$P:: = p|\neg P|P \vee Q|{\bigcirc _{ \ll A \gg }}P|({P_1}, ..., {P_m})pr{j_{ \ll A \gg }}Q, $ |
其中, p∈
语义. APTL公式的语义是在并发博弈结构(concurrent game structure, 简称CGS)[1, 7]的基础上定义的, CGS是七元组C=〈
根据CGS的定义, 在
● λ(s)
●
λ(s)
●
λ(s)
●
●
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), 其中,
如果生成树中的每一条分支都满足Büchi条件, 那么这个生成树是被接收的.一个字是被交替Büchi自动机接收的当且仅当存在一个可接收的生成树.
2 原型工具 2.1 工具框架我们开发了检查APTL公式的可满足性的原型工具APTL2BCG, 该工具是基于Windows平台采用C++语言开发的, 工具架构如图 3所示.
APTL2BCG主要包括以下几个模块, 分别是词法分析与语法树构造模块、预处理模块、转化范式模块、构造LNFG[1]模块、转化GBCG[1]模块、将GBCG转化为BCG[1]模块、BCG化简模块, 根据得到的BCG是否为空检查公式的可满足性.该工具以APTL公式作为输入, 格式为文本文件.在该文件中, 公式的各操作符的表示方法如下:!表示
检查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), 如果树节点有一个孩子节点那么s2和s3为空, 类似的有两个孩子节点的树节点的s3为空.部分APTL公式的语法树结构如图 4所示.
由图 4可以看出, 语法树的根节点能够表示相应的公式类型.true, false, empty, skip以及原子命题的语法树均不含孩子节点.公式
由于输入的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 P→Q
ptree←
case P↔Q
ptree←
case
ptree←P;
case skip
ptree
case
ptree
case len(n)
ptree
case
ptree
case P
if P==true
ptree←Q;
…
if
ptree←false;
case P
if P==Q
ptree←P;
if P==tru
ptree←true;
…
if Q==false
ptree←P;
…
}
}
构造LNFG模块通过循环调用函数NF来构造公式的LNFG.函数NF(CtreeNode *ptree)将APTL公式转化为范式, 其中输入的是APTL公式的语法树, 得到APTL公式的范式的语法树.构造APTL公式的范式图的函数为LNFG(CtreeNode* ptree, CGraph* pgraph), 其中, ptree为公式的范式的语法树, pgraph为生成的LNFG.
给定一个LNFG G=(Q, q0,
任意一个GBCG GB=(
将一个GBCG GB=(
void BCG(CGraph *GBCG, CGraph *BCG){
Q'←Q×{1, …, n};
F'←{ < qF, 1 > |qF∈F1};
if q∉Fi
δ'(< q, i > , p, A')←{ < q', i > |q'∈δ(q, p, A')};
else if q∈Fi
δ'(< q, i > , p, A')←{ < q', i+1 > |q'∈δ(q, p, A')};
}
例子:通过构造公式
首先, 我们将公式写为
$ \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公式
$\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\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.
公式
节点1表示公式
节点2表示
节点3表示
节点4表示
节点5表示
节点6表示empty.
将图 5中的LNFG转化为GBCG, 如图 6所示.其中, 节点1为初始节点, 节点1、节点4标记有l1, 节点3、节点5标记有l2, 接收集合为F={F1={2, 3, 5, 6}, F2={1, 2, 4, 6}}.
将图 6的GBCG转化为BCG如图 7所示, 其中, 状态(1, 1)为初始状态, 接收集合为F'={(2, 1), (3, 1), (5, 1), (6, 1)}.
2.5 BCG的化简及检查
为了检查APTL公式的可满足性, 必须将得到的BCG进行化简, 因此, 我们给出了化简BCG的算法SIMPLIFY.对于一个BCG, 可能存在没有后继节点的节点或者存在没有出边的非接收状态节点, 这些多余的节点和边应该被删除.由于交替自动机中存在一些全局的迁移关系, 也就是说存在从同一个节点出发的多条边应同时满足相应的性质, 所以做完以上删除操作后, 可能会产生非初始节点入度为0的节点, 这些节点也应该被删除, 具体过程如下.
SIMPLIFY(B).
输入:APTL公式φ的BCG B=(
输出:SIMPLIFY(B)计算出一个φ的最简BCG
B'=B;
while
do (Q'=Q'\q;
for each i
/*
if q∈F' then
F'=F'\q;
)
end while
while
do (Q'=Q'\q;
)
end while
return B';
将图 7中的BCG化简得到最简BCG, 如图 8所示, 其中接收集合为F={(2, 1), (3, 1), (5, 1), (6, 1)}.
图 8中的最简BCG不为空, 所以公式
通过检查化简后的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公式表示为
哲学家在吃面条后需要放下筷子接着再思考, 以免相邻的哲学家拿不到筷子.以哲学家1为例, 哲学家1吃完面条就放下筷子用APTL公式表示为:
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]
● 路径λ满足公式(2)当且仅当智能体A的策略使得公式
● 路径λ满足公式(3)当且仅当智能体集合A的策略使得性质P1, P2, …, Pn依次在路径上成立, 并且使得性质Q成立, 公式
实验环境为2.93GHz, Intel(R) Core(TM) i7 CPU 870, 8G内存PC.实验结果见表 1.在表 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] |