DOI: 10.3969/j.issn.1673-4785.201303034
,
,
,
,
,
,
模型检测[1]是一种被广泛应用的验证有限状态系统性质的自动化验证技术。该技术其一方面基于状态转换系统对所考察的系统进行建模，另一方面应用线性时态逻辑LTL或分支时态逻辑CTL等对所需验证的性质进行刻画。在此基础上，通过对状态空间的穷举搜索来判断系统是否满足由时态逻辑公式所刻画的性质，若不满足则返回一条违反规范的路径(即反例)，以便开发者对系统进行改进。在以E.M.Clarke和E.A.Emerson等为代表的研究者的努力下，时态逻辑CTL和LTL的模型检测问题已经得到了很好的解决，其不仅具有高效的搜索算法，而且具有SPIN、SMV等相应的验证工具予以支撑，能够自动化地进行验证。因此，以CTL和LTL为代表的时态逻辑模型检测技术在通讯协议验证、计算机系统验证等方面得到了广泛的应用。
为了将模型检测技术应用于更广泛的领域，在提出时态逻辑的各种扩展形式之后，研究者相应地对这些扩展形式的模型检测问题进行了研究。例如，知识逻辑与时态逻辑相结合的时态认知逻辑在分布式系统中具有广泛应用。对于基于LTL的时态认知逻辑CKLn，2002年Hoek等[2]提出了借助LTL模型检测算法实现CKLn模型检测的方法，2004年，Meyden等基于OBDD技术开发出时态知识逻辑模型检测工具MCK[3]。对于基于CTL的时态认知逻辑CKCn，吴立军等提出了基于OBDD的模型检测算法[4]，并在CTL模型检测工具NuSMV的基础上开发了支持CKCn的模型检测工具MCTK。
无论是在传统时态逻辑CTL、LTL的模型检测中，还是在将它们扩展后得到的时态认知逻辑CKLn等的模型检测中，一个共同的特点是都基于命题逻辑对模型的状态以及时态规范中的原子性质进行描述。由于命题逻辑的描述能力有限，使得对相关知识尤其是领域知识的刻画受到了很大的限制。相对于命题逻辑来说，描述逻辑[5]具有更强的表达能力，同时又保持了可判定性，并且具有有效的判定算法和推理机制作为支撑。特别是近年来，描述逻辑成为了Web本体语言OWL的逻辑基础，是语义Web环境下进行知识表示和知识推理的关键所在。
对描述逻辑进行时态扩展是近年来描述逻辑领域的一个研究热点。通过采用不同的方式在描述逻辑中引入时态维，研究者提出和构造了各种不同类型的时态描述逻辑[6-7]，并证明了这些时态描述逻辑中的公式可满足性问题仍然是可判定的。从描述逻辑的角度看，时态描述逻辑将描述逻辑针对静态领域的知识表示和推理能力扩展到了动态领域。
目前研究者将描述逻辑与时态逻辑相结合的工作绝大部分都是从描述逻辑的角度来进行的，动机是增强描述逻辑的刻画能力，关注的问题主要是公式的可满足性问题。但实际上，从时态逻辑的角度来看，时态描述逻辑将LTL、CTL等时态逻辑中使用的命题逻辑提升到了描述逻辑的层面，在很大程度上扩展了时态逻辑的应用范围。尤其是，鉴于描述逻辑在Web本体语言和语义Web中所扮演的核心角色，时态描述逻辑尤其适用于在语义Web环境下对相关系统的时态性质进行刻画。而为了对这些时态规则进行验证和推理，首先有必要研究时态描述逻辑的模型检测问题。
本文对线性时态描述逻辑ALC-LTL的模型检测问题进行研究。线性时态描述逻辑ALC-LTL最早由Baader等[8]提出。与之前文献中的时态描述逻辑相比，ALC-LTL仅仅将时态算子用于对公式的构造而没有用于对概念的构造，从而在很大程度上降低了公式可满足性问题的计算复杂度。Baader等借助Büchi自动机证明了ALC-LTL中公式可满足性问题的可判定性，然后研究了基于ALC-LTL的运行时验证问题[9]。之后，文献[10]给出了时态描述逻辑ALC-LTL的Tableau判定算法并开发了推理工具。 本文在ALC-LTL的基础上，一方面在公式中引入合取查询，允许变元出现在个体断言中，使得对时态规格的刻画更为方便；另一方面参照ALC-LTL解释结构引入状态迁移系统，作为待检测的模型。针对模型检测问题，本文将描述逻辑ALC的推理机制与时态逻辑LTL的模型检测结合起来，得到时态描述逻辑的模型检测算法。
1 时态描述逻辑ALC-LTL本节对Baader等提出的时态描述逻辑ALC-LTL[8]进行简单介绍。从时态逻辑的角度看，ALC-LTL是在命题线性时态逻辑LTL中引入描述逻辑ALC的刻画成分之后得到的逻辑系统。
ALC-LTL的基本符号包括由概念名组成的集合NC、由角色名组成的集合NR、以及由个体名组成的集合NI。从这些符号出发，通过描述逻辑ALC中的概念构造符和线性时态逻辑LTL中的公式构造符，可以递归地生成ALC-LTL的概念和公式。
定义 1 ALC-LTL中的概念由如下产生式生成： $C,C::={{C}_{i~}}~|\neg C|C\tilde{U}D|\forall \text{R}.C$ 式中：${{C}_{i~}}~\in {{N}_{c}},R\in {{N}_{R}}~\circ \neg C、 C\tilde{U}D、 \forall R.C$的概念分别称为否定、析取以及值限定。
此外，可以引入形如$C\tilde{\cap }D、 \exists R.C、 T$以及⊥的概念，分别作为 $\neg \left( \neg C\tilde{U}~\neg D \right)、\neg \left( \forall R.\neg C \right)、C\tilde{U}\neg C$ 以及的缩写。分别称为合取、存在性限定、全概念以及空概念。
令C、D为任意2个概念，$R \in {N_R},p,q \in N$则将$C \subseteq D$称之为一般概念包含公理，将C(p)称为概念断言，将R(p,q)称为角色断言。C(p)和R(p,q)也可分别记为p:C和pRq。
将一般包含公理、概念断言与角色断言都称为ALC-公理。ALC-公理是构成ALC-LTL公式的最基本的原子公式。
定义 2 ALC-LTL公式通过下式递归生成：$C \subseteq D\|lpha C\left( p \right)\|lpha R\left( {p,q} \right)\|lpha \neg \phi \|lpha \phi \wedge \psi X\phi |\phi U\psi $ 式中：$p,q \in {N_1},R \in {N_R},C、D$为概念。
此外，也可以依次引入形如$\phi \vee \psi 、\phi \to \psi AF\phi $以及的公式，分别作为的缩写。
在语义方面，ALC-LTL公式的解释结构与LTL公式解释结构类似。随着时间的推进将各个状态线性的连接起来。不同的是ALC-LTL公式的解释结构将每个状态映射为一个ALC的一个解释而不单纯的是一个原子命题集合。
定义 3 ALC-LTL解释结构是一个二元组s=(N,I)，其中：
1) N为自然数集合；
2) 函数I对每个自然数n∈N赋予描述逻辑ALC的一个解释I(n)=(Δ,·I(n)，其中的解释函数·I(n)满足以下条件：
① 每个概念名Ci∈Nc解释为Δ的某个子集； CiI(n)
② 每个角色名解释为Δ上的某个二元关系；
③ 每个个体名解释为Δ中的某个元素，并且对于任一自然数m都有piI(n) = piI(m)。
定义 4 给定任一ALC-LTL解释结构，对ALC-LTL中概念和公式的语义递归定义如下：
首先，相对于任一自然数i，将每个概念C解释为Δ的某个子集CI(i)；递归定义为：
1) ${\left( {\neg C} \right)^{I\left( i \right)}}: = \Delta \backslash {C^{I\left( i \right)}}$，其中的“\”为集合差运算；
2) ${{\left( C\tilde{U}D \right)}^{I\left( i \right)}}:={{C}^{I\left( i \right)}}\cup {{D}^{I\left( i \right)}}$，其中的“∪”为集合并运算；
3) ${{\left( \forall R.C \right)}^{I\left( i \right)}}:=\left\{ x| \right.$对于任一$y \in \Delta $如果$\left( {x,Y} \right) \in {R^{I\left( i \right)}}$，则必然有$y \in {C^{I\left( i \right)}}$} $。
其次，相对于任一自然数n∈N，用$\left( {s,i} \right)| = \phi $表示公式φ在结构中的时间点i下成立，递归定义如下：
4) $\left( {s,i} \right)| = C \subseteq D,iff{C^I}^{\left( i \right)} \subseteq {D^I}^{\left( i \right)};$
5) $\left( {s,i} \right)| = C\left( p \right),iff{p^I}^{\left( i \right)} \in {C^I}^{\left( i \right)};$
6) $\left( {s,i} \right)| = R\left( {p,q} \right),iff{p^I}^{\left( i \right)},{q^I}^{\left( i \right)}A \in {R^I}^{\left( i \right)};$
7) $\left( {s,i} \right)| = \neg \phi ,iff\left( {s,i} \right)| = \phi ;$(即公式φ在解释结构中的时间点中不成立)；
8) $\left( {s,i} \right)| = \neg \phi \wedge \psi ,iff\left( {s,i} \right)| = \phi ;$并且$\left( {s,i} \right)| = \psi $
9) $\left( {s,i} \right)| = X\phi ,iff\left( {s,i + 1} \right)| = \phi ;$(；
10) $\left( {s,i} \right)| = \phi U\psi ,iff$存在某整数，使$\left( {s,i + k} \right)| = \psi $并且对于任意0≤j〈k都有$\left( {s,i} \right)| = \phi $
时态描述逻辑ALC-LTL中的知识库与描述逻辑ALC中的知识库相同，由TBox和ABox组成。其中的TBox是由一般概念包含公理组成的有限集合；ABox是由概念断言、角色断言及其否定形式组成的有限集合。
令T是一个TBox，A是一个ABox，那么称知识库〈T,A〉是一致的当且仅当存在描述逻辑ALC的一个语义解释I=(Δ,·I)使得并且I|=T，并且I|=A,也记为I|=〈T,A〉。
令〈T,A〉是一个知识库，p是一个ALC-公理。如果对于描述逻辑ALC的任一语义解释I=(Δ,·I)来说，当I|=〈T,A〉时必然有I|=p，则称知识库〈T,A〉能推导出p，记为〈T,A〉|=p。
2 含有合取查询的时态规范在时态描述逻辑ALC-LTL的基础上，为了进一步增强对时态规范的描述能力，本文在ALC-LTL公式中引入变元，允许变元出现在概念断言和角色断言中个体名的位置上。由于公式中出现的变元代表了一类具有相同性质的个体，从而使得对系统时态性质的刻画更为方便。
为了对含有个体变元的ALC-LTL公式的语义进行严格定义，下面先引入合取查询[11] (Conjunctive query)的概念。
定义 5 基于一个知识库 〈T,A〉定义的合取查询Q是一个原子集合$\left\{ {{q_1}\left( {{{\mathop x\limits^ - }_1}} \right),{q_2}\left( {{{\mathop x\limits^ - }_2}} \right),...,{q_n}\left( {{{\mathop x\limits^ - }_n}} \right)} \right\}$。其中，$qi\left( {{{\mathop x\limits^ - }_i}} \right)$表示概念断言或者角色断言。相应的，$\left( {{{\mathop x\limits^ - }_i}} \right)$表示一个符号${x_i}({q_i}\left( {{{\mathop x\limits^ - }_i}} \right)$表示概念断言)，或者一对符号$\left( {{x_{i1}},{x_{i2}}} \right)\left( {{q_i}\left( {{{\mathop x\limits^ - }_i}} \right)} \right)$表示角色断言)。符号xixi1和xi2表示变元或者个体。也即是qi(xi)≡Ci(xi)或qi(xi1,xi2)≡ R(xi1,xi2)，其中Ci为概念名，Ri为角色名。
为了方便起见，文中用VC(Q)表示合取查询Q中的个体与变元的集合，用V(Q)表示合取查询Q中的变元的集合。当V(Q)=ø时，显然每个符号xi、xi1与xi2都为个体名，此时的Q退化为由概念断言和角色断言合取而构成的公式。
对于一个给定的知识库，合取查询直观上表示一个典型的描述逻辑问题：检索推理问题。
举例来说，设C(x)是一个概念断言，对于一个知识库〈T,A〉，检索推理问题就是根据TBox T在ABox A中找出所有概念C的实例(属于概念C的个体)。角色断言与之类似，假设R(x,y)是一个角色断言,检索推理问题就是根据TBox T在ABox A中找出所有角色R的实例。由此给出如下定义：
定义 6 设〈T,A〉是一个知识库，I=(Δ,·I)是该知识库上的一个解释，$Q = \left\{ {{q_1}\left( {\mathop {{x_1}}\limits^ - } \right),{q_2}\left( {\mathop {{x_2}}\limits^ - } \right),...,{q_n}\left( {\mathop {{x_n}}\limits^ - } \right)} \right\}$是定义在该知识库上的合取查询。则定义${Q^I} = \left\{ {\left\langle {{{\mathop a\limits^ - }_1},{{\mathop a\limits^ - }_2},...,{{\mathop a\limits^ - }_n}} \right\rangle 1,...,{{\left\langle {{{\mathop a\limits^ - }_1},{{\mathop a\limits^ - }_2},...,{{\mathop a\limits^ - }_n}} \right\rangle }_k}} \right\}$，其中，对每一个元组${\left\langle {{{\mathop a\limits^ - }_1},{{\mathop a\limits^ - }_2},...,{{\mathop a\limits^ - }_n}} \right\rangle _t} \in {Q^I}$和每一个原子$qi\left( {\mathop {{x_i}}\limits^ - } \right)$都有〈T,A〉$| = {q_i}\left( {\mathop {{a_{it}}}\limits^ - } \right)$。
定义 7 引入合取查询的时态规范是一个ALC-LTL公式ø(q1,q2,...qn)，其中{q1,q2,…,qn}是ø中所有概念断言和角色断言构成的集合，也是一个合取查询。
显然，这里定义的时态规范也即是用合取查询替代了概念断言和角色断言的ALC-LTL公式。
这里也将符号VC(Q)和V(Q)扩展到时态规范ø上。即VC(ø)=VC(q1,q2,…,qn)，V(ø)=V(q1,q2,…,qn)。显然，当V(ø)=∅时，时态规范是一个不含变元的ALC-LTL公式。
根据ALC-LTL公式的语义，可以给出含有合取查询的时态规范的语义，如下定义：
定义 8 令s=I(i)是一个ALC-LTL解释结构，ø(q1,q2,…,qn)是一个时态规范，{q1,q2,…,qn}是一组合取查询，令VC(q1,q2,…,qn)=$\mathop X\limits^ - $。那么，在一个状态点i∈0,1,2,…下，φ(q1,q2,…,qn)的解释为ø(q1,q2,…,qn) I(i)=$\left\{ {\mathop a\limits^ - |\left( {s,i} \right)| = \phi \left( {{q_1},{q_2}...,{q_n}} \right)\left[{\mathop X\limits^ - /\mathop a\limits^ - } \right]} \right\}$其中的$\mathop a\limits^ - | = \left\langle {{a_1},{a_2}...{a_n}} \right\rangle $是对应于X_的实例元组。
3 模型检测问题 3.1 系统模型在本文中，将待考察的系统建模为一个基于描述逻辑ALC的状态迁移系统。定义如下：
定义 9 基于描述逻辑ALC的状态迁移系统是一个四元组M=(s,S,s0,R,Label)，其中：
1) s是描述逻辑ALC中的一个TBox，对系统中涉及的领域知识进行描述，这些知识不随着时间的变化而变化；
2) S是一个有限的非空状态集；
3) s0是初始状态；
4) R:S→S是一个状态转移函数，使得任一状态s∈S都存在一个惟一的直接后继状态R(s)；
5) Label是标记函数，将每个状态s∈S映射为描述逻辑ALC中的一个ABox。
由于任一状态s∈S都存在惟一后继R(s)，所以可以将上述状态迁移系统看作一个无限的状态序列：s、R(s)、R(R(s))、R(R(R(s)))…。为了表述方便，在后面的内容中将初始状态记为s0，将s0的各个后继状态依次记为s1、s2、s3…。
定义 10 令M=(T,S,s0,R,Label)是基于描述逻辑ALC的一个状态迁移系统。如果存在一个ALC-LTL解释结构s=(N,I)，使得对于任一自然数i∈N都有I(i)|=〈T,Label(si)〉，则将s=(N,I)称为状态迁移系统的一个解释。
3.2 模型检测在本文中提出的模型检测方案是将应用领域的语义抽象的建模为一个本体；将系统模型建模为一个基于描述逻辑描述的状态迁移系统模型M，在每个状态中用描述逻辑来描述系统的性质和行为；用带有合取查询的ALC-LTL公式φ来描述待验证的规范。这样，ALC-LTL模型检测问题即为验证M|=ø是否成立：
定义 11 给定状态迁移系统M=(T,S,s0,R,Label)和时态规范ø(q1,q2,…,qn)，如果对于M的任一解释s=(N,I)都有 ø(q1,q2,…,qn)I(0)≠∅
则称时态规范φ(q1,q2,…,qn)在模型中成立，记为Mø。
为了便于对算法进行介绍，在这里选取一段中国历史作为案例进行研究说明，验证在这段历史中是否具有某种规律——我国历史上的唐王朝历经22位皇帝，23次政权交替，24次执政。这22位皇帝上台执政或是因为接受禅让或是因为发动政变夺取皇位，在这里抽出几位皇帝按照他们在位顺序将他们列举如下图 1所示。
|
| 图 1 唐朝部分皇帝执政顺序 Fig. 1 Some of the Tang Dynasty emperors in chronological order |
由于这几位皇帝具有如下的血缘关系：
父子关系：李治→李显；李治→李旦；李显→李重茂；李旦→李隆基。
母子关系：武则天→李显；武则天→李旦。
为了便于对算法进行介绍，在这个实例中将傀儡政权的操纵者也视为是政变者，并且不考虑被废的皇太子。在此基础上来判断是否能从这段历史中得到如下结论：
1) 如果接任皇位的新君不是前任皇帝的皇子，则新君一定是发动政变获取的皇位；
2) 如果接任皇位的新君不是前任皇帝的儿子，则要么新君是发动政变获取的皇位，要么前任皇帝是傀儡。
4 ALC-LTL的模型检测 4.1 预处理对于前述案例来说，在调用模型检测算法之前首先需要将案例中所需要用到的领域知识建模为一个术语集Tbox。如表 1所示。
对于这段历史事实，根据表 1中定义的术语，进一步的将其建模为一个基于描述逻辑的状态迁移系统M。为方便起见，文中用s0,…,s7,…来表示从李治开始的各皇帝执政时期的状态。那么有: R(si)=si+1(i≥1) Label(s0)={Emperor(lizhi),haschild(lizhi,lixian),haschild(lizhi,lidan)}；
Label(s1)={Emperor(lixian),puppet(lixian),haschild(lixian,lichongmao)}；
Label(s2)={Emperor(lidan),puppet(lidan),haschild(lidan,lilongji)}；
Label(s3)={Emperor(wuzetian),manipulator(wuzetian),haschild(wuzetian,lixian),haschild(wuzetian,lidan)}；
Label(s4)={Emperor(lixian),bekilled(lixian),haschild(lixian,lichongmao)}；
Label(s5)={Emperor(lichongmao),bekilled(lichongmao)}；
Label(s6)={Emperor(lidan),coupmakers(lidan),haschild(lidan,lilongji)}；
Label(s7)={Emperor(lilongji)}.
对于所考察的结论(1)，可将其形式化描述为 G(Emperor(x)∧haschild(x,y)∧X(¬Emperor(y))→
X(Emperor(z)∧coupmakers(z))) (1) 对于所考察的结(2)，可以将其形式化描述为 G(Emperor(x)∧haschild(x,y)∧X(Emperor(y))→X((Emperor(z)∧coupmakers(z))∨puppet(x))) (2)
为了方便算法处理，在把时态规范带入算法执行之前通常要进行预处理，将时态规范转换为标准否定范式(negation normal form)。具体来说，首先将蕴涵连接词消去，然后借助德摩根法则(¬(p∨q) ≡ ¬p∧¬q，¬(p∧q) ≡¬p∨q)和对偶规则(¬Gp≡F¬p)将否定符号尽可能的向内移，使得否定符号仅与断言相邻。
例如对时态规范① 化后得到如下形式： G{Emperor(x)∨¬haschild(x,y)∨ XEmperor(y)
X[Emperor(z)∧coupmakers(z)]}(3) 在这里，预处理后的规范中含有的合取查询为：{Emperor(x),haschild(x,y),Emperor(y),Emperor(z),coupmakers(z)}。
类似地可以将时态规范② 化为如下形式： G{¬Emperor(x)∨¬ haschild(x,y)∨XEmperor(y)∨Xpuppet(x)∨X[Emperor(z)∧coupmakers(z)]}(4)
在本文所构造的ALC-LTL公式中，一般概念包含公理并不随着时间的变化而变化，全局保持一致。因此时态规范中出现的一般概念包含公理可视为恒成立，在预处理阶段用true代替一般概念包含公理。
另外，在介绍算法之前，有必要引入一些算法中用到的概念和术语。
定义 13 假设表A、B的表头分别是：{x1,…,xm,y1,…,yn}和{y1,…,yn,z1,…,zt}，属性y1,…,yn是表A与表B共有的属性，x1,…,xm为表A所特有的属性，z1,…,zt为表B所特有的属性。那么，表A与表B的自然连接(在算法中记为A⊗B)是一个表，它的表头为{x1,…,xm,y1,…,yn,z1,…,zt}。其中属性x1,…,xm,y1,…,yn对应的值为表A中的值，属性y1,…,yn,z1,…,zt对应的值为表B中出现的值。也即是属性y1,…,yn的值是表A和表B中所共有的值。
举例来说：表A的表头为{x,y,z}，表B的表头为{z,t}。它们分别对应的数值如下： $$A=\left[ \begin{array}{*{35}{l}} x & y & z \\ 1 & 2 & 3 \\ 2 & 3 & 3 \\ 1 & 1 & 1 \\ \end{array} \right] B=\left[ \begin{array}{*{35}{l}} z & t \\ 3 & 5 \\ 1 & 6 \\ 3 & 4 \\ \end{array} \right]$$
那么表A与表B的自然连接为 $$A\otimes B=\left[ \begin{array}{*{35}{l}} x & y & z & t \\ 1 & 2 & 3 & 5 \\ 1 & 2 & 3 & 4 \\ 2 & 3 & 3 & 5 \\ 2 & 3 & 3 & 4 \\ 1 & 1 & 1 & 6 \\ \end{array} \right]$$
一个实现自然连接最简单(非最优化)的算法是首先求得表A与B的笛卡尔积，然后去除表A
在下面的算法中处理合取查询时要调用到一个关键的服务——合取查询应答服务[11-12]。在后文的算法中，用标记CQ_answer(q,K)来指代对该算法的调用。该算法的输入是一个可能包含变元的断言q和一个描述逻辑知识库K=(T,A)。具体来说该算法就是根据知识库K中的TBox T对断言q在ABox A中进行推理、查询，在A中找出该断言的所有实例。最终以表的形式给出返回值。该表的表头对应着该断言q中的个体和变量(即表头对应着VC(q)中所有的元素)，表的每一行是一组对个体和变量VC(q)的可能的赋值，表的每一列是对相应个体或变量的所有可能赋值。
合取查询应答服务算法已得到了广泛的研究[11-12]，况且本文用到的合取查询算法每次仅对一个断言进行查询，比较简单，在这里不再详细介绍该算法的具体步骤。
4.2 模型检测算法令M=(s,S,s0,R,Label)和ø(q1,q2,…,qn)分别是经过预处理的状态迁移系统和时态规范，下面判断M|=ø是否成立。
整个模型检测算法分为3个步骤，分别完成不同功能。首先是对状态迁移系统的处理，查找出时态规范中包含的合取查询，对合取查询中每一个断言，在系统模型的所有状态中进行推理、检索，查找出所有断言在所有状态中的所有实例，并将这些实例在系统模型中分别映射为所在状态的命题条件。这样，基于描述逻辑的状态迁移系统就被映射为了基于“命题”的状态迁移系统。其次是对时态规范的处理，将前面查找到的各个断言的实例根据时态规范的结构通过自然连接组合在一起，生成所有可能的组合形式，将这些实例组合依次代入时态规范的相应断言中并映射为相应的命题，便可得到若干组不含变元的“命题”时态规范。这里所谓的“命题”也就是将模型和规范中相同的ALC-公理视为是相同的命题符号。最后将得到的所有“命题”时态规范分别在这个基于“命题”的状态迁移系统中进行LTL模型检测，看是否存在不成立的“命题”时态规范。
4.2.1 对状态迁移系统的处理给定状态迁移系统M=(s,S,s0,R,Label)和时态规范ø(q1,q2,…,qn) (qi表示ø中的断言)，经过本步骤的处理后将得到一个基于命题的状态迁移系统M=(TrueP,S,s0,R,X)和一个二维集合ASS[n][m]。其中集合ASS[q][s]是断言q在状态s中所有可能的赋值组成的集合。
被步骤中处理过程的基本思路为：在系统模型的每一个状态si中，对时态规范中所有断言qj调用合取查询应答服务算法，得到所有断言在所有状态中的所有实例赋值。然后将这些实例分别代入与之对应的断言中并映射为状态的命题条件，这样最终便得到一个基于命题的迁移系统。
下面引入处理过程中用到的几个集合和函数：用函数PRO将每个状态中通过合取查询得到的断言实例映射为一个命题；用集合TrueP记录处理过程中得到的真命题；用函数将每个状态映射到其对应的真命题。本文采用闭世界假设，因此可以得到状态s对应的假命题集合：TrueP/X(s)。
在此基础上，对详细的处理过程描述如下：
1) 查找出时态规范中所包含的的合取查询Q={q1,…,qn}，对Q中每个断言q，令ASS[qj][si]=∅；
2) 在Q中选取一个尚未处理过的断言qj，如果Q中所有的断言都已处理过，则转向5)；
3) 在模型M中选取一个尚未查询过的状态si，如果所有状态都已处理过，则转向2)；
4) 对断言qj在状态si中调用合取查询应答服务CQ_answer(qj,〈s,Label(si)〉)，将返回值存入集合ASS[qj][si]，并用返回值替代qj中变量(qj[X/CQ_answer(qj,〈T,Label(si)〉)])，将其标记为真命题分别存入真命题集合TrueP以及X(si)，标记为状态si中成立的命题，转回3)；
5) 返回Kripke模型M=(TrueP,S,s0,R,X)以及二维集合ASS[n][m]。
4.2.2 时态规范处理在该步骤中输入标准化规范ø(q1,…,qn)和集合ASS[n][m]，经过本步处理得到一个不含变元的时态规范集合Φ。
根据ø的结构对ASS[n][m]中各集合进行组合并通过自然连接相结合，得到的每一组数据都是一组对ø中VC (ø)的个体赋值。对于ASS[qj][si]为空的集合可用false代替。
首先引入处理过程中用到的几个概念：集合N,M存储的子公式；函数Sc将φ的每一个子公式映射到一个数据；集合A[n]用来存储VC (ø)的赋值。详细的处理过程描述如下：
1) 令N:={ø},Sc(ø)=0,Φ:=∅；
2) 从集合N中取出一个公式ψ，并将ψ从N中删除，若N空则转8)；
3) 若ψ为断言或断言的否定，则令A[ψ]=ASS[ψ][Sc(ψ)]，转2)；
4) 若ψ:=Xψ1，则将ψ1存入N，令Sc(ψ1)=Sc(ψ)+1，转2)；
5) 若ψ:=ψ1∧ψ2或ψ1∨ψ2，则将ψ1,ψ2存入N，令Sc(ψ1)=Sc(ψ2)=Sc(ψ)，转2)；
6) 若ψ:=Gψ1，则将ψ1与ψ2存入N，令Sc(ψ1)=k，(k=0,…,m)，转2)；
7) 若ψ:=ψ1Uψ2，则将ψ1与ψ2存入N，令Sc(ψ1)=0，Sc(ψ2)=min，转2)；
8) 令ASSER:=A[q1]⊗...⊗A[qn]，
9) 在集合ASSER中选取一组尚未经过处理的元组tupe，如果所有的元组都已处理过，则转11)；
10) 令X_=VC (ø)，Φ:=Φ∪{ø[X_/]};转9)；
11) 返回集合Φ。
(注：若Sc(ψ)=min+t，则令A[ψ]=ASS[ψ][s]，其中s为ASS[ψ][m]中状态下标最小的非空集合)。
注意到，某公式ψ:=ψ1Uψ2，则ψ1一定在s0状态中成立，且ψ2在状态下标最小的状态中成立。而ψ:=Gψ1意味着ψ1在每一个状态中成立。
4.2.3 命题LTL模型检测在该步骤中输入步骤一中得到的状态迁移系统M=(TrueP,S,s0,R,X)和2) 中得到的时态规范集合Φ。调用常规LTL模型检测算法对Φ中的每一个时态规范在状态迁移系统M中进行验证，如果否条时态规范返回反例，则算法返回该时态规范及其反例，算法结束。否则所有时态规范均成立，则返回true值，算法结束。
在案例中对规范③ 行检测，调用上述算法。调用步骤一，对状态迁移系统模型进行处理，首先查得到规范③ 所包含的的合取查询{Emperor(x),haschild(x,y),Emperor(y),Emperor(z),coupmakers(z)}；选取Emperor(x)在状态s0中调用合取查询应答服务算法，得到返回值{lizhi},用{lizhi}替代Emper or(x)中变量得到Emperor(lizhi)作为X(s0)标记；并将{lizhi}存入ASS[Emperor(x)][s0]。其余查询与此类似不再赘述，最终得到：
1) ASS[Emperor(x)]=ASS[Emperor( y)]=ASS[Emperor(z)]={{lizhi},{lixian},{lidan},{wuzetian},{lixian},{lichongmao},{lidan},{lilongji}}；
ASS[haschild(x,y)]={{{lizhi,lixian},{lizhi,lidan}},{lixian,lichongmao},{lidan,lilongji},{{wuzetian,lixian},{wuzetian,lidan}},{lixian,lichongmao},∅,{lidan,lilongji},∅}；
ASS[coupmakers(z)]={∅,∅,∅,{wuzetian},∅,∅,{lidan},∅}。
2) 令N:={ø},Sc(ø)=0，取ψ= ø，因为ø =G{¬Emperor(x)∨¬haschild(x,y)∨XEmperor(y)∨X[Emperor(z)∧coupmakers(z)]}，故将ψ1={¬Emperor(x)∨ ¬haschild(x,y)∨XEmperor(y)∨X[Emperor(z)∧coupmakers(z)]}存入N，Sc(ψ1)=k。
从N中取出ψ1，令ψ=ø，因为ψ为ψ1∨ψ2的形式，故将{¬Emperor(x)},{¬haschild(x,y)},{XEmperor(y)},{X[Emperor(z)∧coupmakers(z)]} 存入N，且Sc(ψ1)= Sc(ψ2)=Sc(ψ3)=k，…。最终求得Sc(Emperor(x))= Sc(haschild(x,y))=k，Sc(Emperor(y))= Sc(Emperor(z))= Sc(coupmakers(z))=k+1。
k=1时得到ASSER={A[Emperor(x)]=ASS[Emperor (x)][1];A[haschild(x,y)]=ASS[haschild(x,y)][1];A[Emperor(y)]=ASS[Emperor(y)][2];A[Emperor(z)]=ASS[Emperor(z)][2];A[coupmakers(z)]=ASS[coupmakers(z)][2]}，
k=2时得到ASSER={A[Emperor(x)]=ASS[Emperor (x)][2];A[haschild(x,y)]=ASS[haschild(x,y)][2];A[Emperor(y)]=ASS[Emperor(y)][3];A[Emperor(z)]=ASS[Emperor(z)][3];A[coupmakers(z)]=ASS[coupmakers(z)][3]}，…
将ASSER中每一组数据自然连接后带入φ，可得若干组时态规范： G{¬Emperor(lizhi)∨¬haschild(lizhi,lixian)∨XEmperor(lixian)∨X[Emperor(lixian)∧coupmakers(lixian)]}; G(¬(Emperor(lizhi)∧haschild(lizhi,lidan))∨XEmperor(lidan)∨X[Emperor(lidan)∧coupmakers(lidan)]}; G(¬(Emperor(lizhi)∧haschild(lixian,lichong-mao))∨XEmperor(lidan)∨X[Emperor(lidan)∧coupmakers(lidan)]}; …
3) 将得到的所有命题时态规范依次带入M=(TrueP,S,s0,R,X)中进行验证。在验证第2) 条时态规范G(¬(Emperor(lizhi)∧haschild(lizhi,lidan))∨X Emperor(lidan)∨X[Emperor(lidan)∧coupmakers(lidan)]}时，返回反例，算法结束。 与上面的过程类似，可以对时态规范④进行模型检测；模型检测结果将表明案例中考察的结论(2) 成立，算法返回true。
4.3 复杂度分析算法主要的时间花销在于对合取查询调用应答服务算法在各个状态中寻找实例。最坏情况下在公式φ中含有|φ|个合取查询，需要在|S|个状态中调用合取查询应答服务算法，设合取查询应答服务算法的时间复杂度[11]为|CQA|，那么这个环节的最坏时间复杂度为O(|ø|*|S|*|CQA|)。根据ø的结构对实例进行组合，时间复杂度与|ø|成线性关系。最坏情况下需要对每一组时态规范调用一次LTL模型检测算法。|ø|个合取查询的所有赋值与|Ssys|成线性关系，产生|Ssys|个命题时态规范。假设LTL模型检测算法的时间复杂度为O(2|ø|*|S|2)[1]，那么本章算法的最坏时间复杂度为O(|φ|*|S|*|CQA|+|Ssys||ø|*2|ø|*|S|2)，也即是max{O(|ø|*|S|*|CQA|),O(|Ssys|*2|φ|*|S|2}。
5 工作比较到目前为止，国内外与时态描述逻辑的模型检测相关的工作主要有3项：文献[13]将含有过去算子的线性时态逻辑LTL与描述逻辑ALC结合起来，基于模型检测问题对本体演化过程进行推理和验证。但是他们并没有提出模型检测算法，只是将所研究的问题转化成了LTL的模型检测问题。文献[14]基于标记büchi自动机研究了时态描述逻辑ALC-LTL的模型检测问题，但是该文献没有考虑含有变元的时态规范。文献[15]将分支时态逻辑CTL与描述逻辑ALC结合起来，得到带有描述逻辑ALC标注的时态逻辑AnCTL，研究了AnCTL的模型检测问题，最终将AnCTL及其模型检测算法应用于语义Web服务的时态规格和验证。但是文献[15]提出的算法不能返回反例，只能验证能否存在可满足的时态规范。如下例：在图 2模型中验证时态规范x
|
| 图 2 案例模型 Fig. 2 Model of case |
依据文献[15]的算法，将得到2个命题时态规范：A:C∧Xb:D与A:C∧Xc:D，显然A:C∧Xc:D并不是所需要验证的时态规范，其验证结果恒为false。对这些恒为false的规范调用模型检测算法进行验证造成了时间上的浪费，本文算法避免了这些问题。
6 结束语本文提出的时态描述逻辑ALC-LTL的模型检测算法使用具有变量的时态描述逻辑ALC-LTL公式作为时态规范，这样扩大了待验证规范的描述范围。在描述系统的状态迁移系统中引入描述逻辑知识库，增加了对系统领域知识的表示能力。最终使得时态逻辑的模型检测能够应用到更广阔的空间，尤其适用于在语义Web环境下对复杂系统的时态性质进行规格和验证。虽然本文仅讨论了ALC-LTL模型检测的算法，但可以类似地将ALC-LTL中的描述逻辑ALC替换为其它任何一个描述逻辑XDL，或者将时态逻辑LTL替换为其它时态逻辑YTL后(如CTL)；对于这样替换后得到的模型检测问题，只需要在算法中相应地将ALC的推理机制替换为描述逻辑XDL的推理机制，或者将调用的LTL的模型检测算法替换为时态逻辑YTL的模型检测算法，就可以得到时态描述逻辑XDL-YTL的模型检测算法。
本文只是将ALC-LTL模型检测转换成了LTL的模型检测，并没有给出直接的ALC-LTL模型检测算法，这可能会造成时态规范规模的爆炸问题，这也是我们下一步要进行的工作。另外，本文算法中采用了闭世界假设，在一定程度上限制了算法的应用范围；下一步将研究如何在采用开世界假期的情况下进行ALC-LTL模型检测。
| [1] | Jr CLARKE E M, GRUMBERG O, PELED D A. Model checking[M]. Cambridge: The MIT Press, 1999 : 23 -28. |
| [2] | Van der HOEK W, WOOLDRIDGE M. Model checking knowledge and time[C]//Model Checking Software. Van der HOEK W, WOOLDRIDGE M. Model checking knowledge and time[C]//Model Checking Software.Model checking knowledge and time |
| [3] | GAMMIE P, Van Der MEYDEN R. Mck: Model checking the logic of knowledge[C]//Computer Aided Verification (CAV'04). Heidelberg: Springer, 2004: 479-483. |
| [4] | 吴立军, 苏开乐. 多智体系统时态认知规范的模型检测算法[J]. 软件学报,2004, 15 (7) : 1012 –1020. WU Lijun, SU Kaile.. A model checking algorithm for temporal logics of knowledge in multi-agent systems[J]. Journal of Software,2004, 15 (7) : 1012 –1020. |
| [5] | BAADER F, CALVANESE D, MCGUINNESS D, et al. The description logic handbook: theory, implementation and applications[M]. Cambridge: Cambridge University Press, 2003 : 14 -18. |
| [6] | ARTALE A, FRANCONI E. A survey of temporal extensions of description logics[J]. Annals of Mathematics and Artificial Intelligence,2000, 30 . |
| [7] | LUTZ C, WOLTER F, ZAKHARYASCHEV M. Temporal description logics: a survey[C]//Temporal Representation and Reasoning. Los Alamitos: IEEE Computer Society Press, 2008: 3-14. |
| [8] | BAADER F, GHILARDI F, LUTZ C. LTL over description logic axioms[C]//Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning. Cambridge: AAAI Press, 2008: 684-694. |
| [9] | BAADER F, BAUER A, LIPPMANN M. Runtime verification using a temporal description logic[C]//Frontiers of Combining System. Heidelberg: Springer, 2009: 149-164. |
| [10] | 常亮, 王娟, 古天龙, 等. 时态描述逻辑ALC-LTL的Tableau判定算法[J]. 计算机科学,2011, 38 (8) : 150 –154. CHANG Liang, WANG Juan, GU Tianlong, et al. Tableau decision algorithm for the temporal description logic ALC-LTL[J]. Computer Science,2011, 38 (8) : 150 –154. |
| [11] | ORTIZ M, CALVANESE D, EITER T. Characterizing data complexity for conjunctive query answering in expressive description logics[C]//Proceedings of the 21th AAAI Conference on Artificial Intelligence. London: AAAI Press, 2006: 275-280. |
| [12] | CALVANESE D, De GIACOMO G, LEMBO D, et al. Data complexity of query answering in description logics[J]. Knowledge Representation and Reasoning,2006 (6) : 260 –270. |
| [13] | HUANG Zhisheng, STUCKENSCHMIDT H. Reasoning with multi-version ontologies: a temporal logic approach[M]//The Semantic Web-ISWC 2005(ISWC2005). Heidelberg: Springer, 2005: 398-412. |
| [14] | 朱创营, 常亮, 徐周波, 等. 基于标记büchi自动机时态描述逻辑ALC-LTL模型检测[J]. 计算机科学,2013, 40 (10) : 166 –171. ZHU Chuangying, CHANG Liang, XU Zhoubo, et al. Model checking of temporal description logic ALC-LTL based on label büchi automata[J]. Computer Science,2013, 40 (10) : 166 –171. |
| [15] | Di PIETRO I, PAGLIARECCI F, SPALAZZI L. Model checking semantically annotated services[J]//IEEE Transactions on Software Engineering, 2012, 38(3): 592-608. |