软件学报  2019, Vol. 30 Issue (7): 1953-1965   PDF    
基于实时自动机的连续时段演算的验证
安杰, 张苗苗     
同济大学 软件学院, 上海 201804
摘要: 时段演算是描述和推导嵌入式实时系统和混成系统性质的一种区间时态逻辑.扩展线性时段不变式是时段演算的重要子集.针对实时自动机,提出一种连续时间语义下扩展线性时段不变式的有界模型检验方法.该方法将扩展线性时段不变式的有界模型检验问题转化为量词线性算术公式的正确性问题,从而可以采用量词消去技术进行求解.首先,运用符号化的思想,在实时自动机上利用深度优先搜索找到所有满足观测时长约束的符号化路径片段;然后,将每条符号化路径片段转化为一个量词线性算术公式;最后,利用量词消去工具求解.与已有工作相比,基于实时自动机设计了验证算法.另外,降低了验证复杂度,并且加速了验证过程的实际速度.
关键词: 时段演算     扩展线性时段不变式     量词线性算术     量词消去    
Verifying Continuous-time Duration Calculus against Real-time Automaton
AN Jie, ZHANG Miao-Miao     
School of Software Engineering, Tongji University, Shanghai 201804, China
Foundation item: National Natural Science Foundation of China (61472279)
Abstract: Duration calculus is a kind of interval temporal logic, which is designed for specifying and reasoning the properties about the embedded real-time systems and hybrid systems. Extend linear duration invariants (ELDI) is an important subset of duration calculus. In this study, a bounded model checking algorithm of ELDI formulas against real-time automaton is proposed. The bounded model checking problem of ELDI is reduced into the validity problem of Quantified linear real arithmetic (QLRA) formulas, which can be solved by Quantifier elimination (QE) technique. Firstly, by using deep first search algorithm, the real-time automaton is searched to find all the symbolic paths segments which satisfy the constraints of observation time length. Secondly, the paths segments are transformed into QLRA formulas. Finally, the QLRA formulas are solved by QE tools. Thus, compared with the related works, a verification algorithm of ELDIs is proposed against real-time automaton with lower complexity. In addition, the practical speed of verifying process is accelerated.
Key words: duration calculus     extended linear duration invariants     quantified linear real arithmetic     quantifier elimination    

时段演算[1, 2]是周巢尘院士、Hoare和Ravn提出的一种在较高抽象层次上描述和推理嵌入式实时系统及混成系统性质的区间时态逻辑.它对区间时态逻辑[3]进行了扩展, 引入了时段(duration)记号, 将在观察区间内(从a时刻到b时刻)系统在某个状态(s)的累积停留时间记为状态表达式积分$\left( {\int_a^b s } \right).$目前时段演算已在实际系统设计与验证中有了广泛应用[4, 5].时段演算强大的表达能力对系统需求描述有诸多好处, 但其较高的抽象程度为自动化验证带来了不便.时段演算的可满足性(satisfiability)、正确性(validity)和模型检验(model checking)问题都是不可判定的(undecidable)[6].

周巢尘等学者提出并分析了时段演算中一个名为线性时段不变式(linear duration invariants, 简称LDI)[7]的子集, 其形式为$b \leqslant \ell \leqslant e \Rightarrow {\sum _{s \in S}}{c_s}\smallint s \leqslant M;$其中, $\smallint s$表示在观测区间[t, t′]上, 系统在状态s的累积停留时间, ℓ表示观测区间长度, 即t′–t, cs为常量系数, M为实数.因此, 一个LDI公式表示:满足观测区间长度约束时系统状态的时段性质需满足线性约束$\sum\nolimits_{s \in S} {{c_s}\int {s \leqslant M} } .$LDI公式的表达能力较强.例如, 对于文献[5]中煤气燃烧器的例子, 可以将燃烧器的安全需求“任何时候对于系统观察超过1min, 煤气泄漏的累积时间不得超过观察时长的二十分之一”, 表示为一个LDI公式$\ell \geqslant 60 \Rightarrow 20\smallint Leak \leqslant \ell , $该LDI公式可以很容易地改写为上述线性形式$\ell \geqslant 60 \Rightarrow 19\smallint Leak - \smallint Nonleak \leqslant 0.$

文献[7]证明了基于实时自动机的LDI性质的模型检验问题是可判定的.实时自动机可以看作是一类特殊的时间自动机, 即只有一个时钟变量并且每次迁移都会重置该时钟.基于该工作, 学术界研究了在比实时自动机表达能力更强的模型(如时间自动机、混成自动机)下LDI公式的模型检验问题[8-12].其中, 文献[11, 12]提出了一些对于时间自动机下LDI的模型检验的高效算法, 并将这些方法扩展到时间自动机网络中[13].

那么对于时段演算是否可以找到一个比LDI更大的子集, 其模型检验问题仍然是可以判定的.一个比较自然的想法是, 对LDI进行扩展, 例如, 加入布尔连接符和模态词切变(chop), 这样就形成扩展线性时段不变式(extended linear duration invariants, 简称ELDI).根据文献[6]的结论, 在离散时间语义和连续时间语义下, ELDI的可满足性(satisfiability)和正确性(validity)都是不可判定的.Martin等人证明了在离散时间语义和连续时间语义下, 对于有限状态机下ELDI的模型检验问题是不可判定的[14].因此, 他们提出了ELDI的一个近似语义, 并且给出了在该近似语义和离散时间条件下的模型检验算法.由于该算法复杂度过高, 在实际系统中很难运用, 所以Martin等人提出了另外一种近似语义, 并将ELDI的模型检验问题转化为Presburger算术[15].受到该工作的启发, 我们证明了在标准离散时间语义下基于时间自动机的ELDI有界模型检验问题是可以判定的, 并给出了一种高效的模型检验算法[16].更进一步地, 我们讨论了在连续时间语义下基于时间自动机的ELDI的有界模型检验问题, 给出了复杂度为三阶指数的判定算法[17].在此指出, 文献[16, 17]与本文所说的有界模型检验均特指对于ELDI公式中观测区间长度ℓ有上界, 即对于形式b≤ℓ≤e, 其中的上界e有界.

在本文中, 我们研究在标准连续时间语义下基于实时自动机的ELDI的有界模型检验问题.证明了该问题是可以判定的, 并且给出模型检验算法.与文献[7]的区别是, 文献[7]讨论的是基于实时自动机的线性时段不变式(LDI)的模型检验问题, 而本文讨论的是基于实时自动机的扩展线性时段不变式(ELDI)的模型检验问题, 针对的公式更加复杂.与文献[16]比较最主要的一个不同点是, 本文关注于连续时间语义, 而文献[16]关注的是离散时间语义.与文献[17]比较, 本文讨论的模型是实时自动机, 可以得到更加简便的模型检验算法, 在多个方面降低了时间复杂度, 提高了算法实际运行效率.

本文验证方法的基本思路如下.

●第1步, 运用符号化的思想, 在实时自动机上利用深度优先搜索找到所有满足观测时长约束的符号化路径片段;

●第2步, 将每条路径转化为一个量词线性算术表达式(quantified linear real arithmetic, 简称QLRA);

●第3步, 将得到的所有量词线性算术表达式运用量词消去工具(例如REDLOG)求解.

在第1步中, 我们定义了符号化路径片段, 给出了相应的求取方法, 并且有效地缩小了搜索空间.在第2步中, 我们详细定义并构造了组成量词线性算术表达式的不等式约束, 并且采用一些方法减少量词的引入个数.由于量词消去的复杂度与量词个数相关, 因此第2步的处理也加快了第3步量词消去的实际运行速度.

本文第1节对相关基础知识进行回顾, 包括实时自动机和扩展的线性时段不变式, 并给出本文涉及的量词线性算术的定义, 方便后文叙述.第2节对于运用符号化的思想在实时自动机上利用深度优先搜索找到所有满足观测时长约束的符号化路径片段进行描述.第3节介绍如何将一条符号化路径片段转化为一个量词线性算术表达式.第4节根据量词线性算术表达式结果给出ELDI模型检验的判定结果以及相关定理.第5节给出工具实现描述和实验结果.最后对全文进行总结.

1 基础知识及相关定义

本节首先介绍实时自动机, 实时自动机作为本文讨论的模型检验问题中的模型语言.之后介绍扩展线性时段不变式(ELDI), ELDI作为本文模型检验问题中的需求描述逻辑.第3节给出量词线性算术的定义.为了叙述简洁, 本文固定一组命题集合记为$\mathcal{P}$.

1.1 实时自动机

实时自动机(real-time automaton, 简称RTA)[18]可以看作时间自动机(timed automaton)[19]的一个子集, 即只含有一个时钟变量并且每次迁移都重置该时钟变量.实时自动机是对实时系统建模的主流模型.下面给出实时自动机的定义.

定义1(实时自动机).   一个实时自动机RTA是一个6元组$\mathcal{A} = (S, \Sigma , {\rm{\Delta }}, {s_0}, F, \mu ), $其中,

S是一个有穷状态(位置)集合;

S是一个有穷字母表;

● ∆⊆S××S是迁移关系;

s0S是初始状态;

FS是接收状态集合;

$\mu :\Delta \to {2^{{\mathbb{R}_{ \geqslant 0}}}}\backslash \{ \emptyset \} $是一个时间标签函数(μ(∆)通常是一些区间的集合, 这些区间的端点一般落在$\mathbb{N}$∪{∞}或者${\mathbb{Q}_{ \geqslant 0}} \cup \{ + \infty \} $).

一条迁移(s1, σ, s2)∈∆称为σ-迁移, 迁移的源节点状态和目标节点状态分别表示为PreσPostσ.对于实时自动机, 它的一个执行(run)要么只是初始状态s0, 要么为如下形式:其中, n > 0, 对于$1 \leqslant $ $i \leqslant n({s_{i - 1}}, {\sigma _i}, {s_i}) \in {\rm{\Delta }}$并且${\lambda _i} \in \mu ({s_{i - 1}}, {\sigma _i}, {s_i}).$

例1:如图 1所示为一个实时自动机$\mathcal{A}$, 对于其6元组, 状态(位置)集合为S={s0, s1, s2}, 有穷字母表为={a, b, c}, 初始状态为s0, 接收状态集合为F={s2}, 迁移集合为∆={(s0, a, s1), (s1, b, s1), (s1, c, s2)}, 对应的时间标签函数产生的时间标签为μ(∆)={[1,2],[1,3],[2,4]}.

Fig. 1 An example for real-time automaton 图 1 一个实时自动机示例

特别地, 在不影响理解的情况下, 本文之后不对状态和位置做出区分.本文讨论的实时自动机不涉及兹诺行为(non-Zeno)[19], 即每一个可控的循环最少消耗时间为$\epsilon \in {{\mathbb{R}}_{>0}}.$

1.2 扩展线性时段不变式

扩展线性时段不变式是时段演算的一类重要子集, 可以看作是在线性时段不变式(LDI)的基础上引入逻辑连接符$\left( \neg , \wedge , \vee \right)$以及模态词切变(“; ”)得到的.ELDI与LDI相比具有更加复杂的语法结构, 相应地, 表达能力也更强.同时对其进行验证也变得更加困难, 特别是模态词切变的引入, 让ELDI的模型检验问题与LDI的模型检验问题有了根本区别.

扩展线性时段不变式在语法上包括3个组成部分:状态表示式S、线性时段子式$P \in \mathcal{P}$、ELDI子式ϕ.扩展线性时段不变式的定义如下.

定义2(扩展线性时段不变式).  扩展线性时段不变式的结构定义如下.

S::=0|P|$\neg $S|S1$\vee $S2;

$\mathcal{D}:: = \sum\nolimits_{i \in \Omega } {{c_i}} \smallint {S_i} \leqslant c;$

$\phi ~::=\mathcal{D}\ |\neg \phi \ |{{\phi }_{1}}\vee {{\phi }_{2}}\ \text{ }\!\!|\!\!\text{ }{{\phi }_{1}};{{\phi }_{2}}, $

其中, $P \in \mathcal{P}$表示状态变量, cic为实数, Ω为一个有穷的下标集合.每一个扩展线性时段不变式都可以表示为如下形式:b≤ℓ≤eϕ, 其中, $b \in {\mathbb{R}_{ \geqslant 0}}, e \in {\mathbb{R}_{ \geqslant 0}} \cup \{ {\rm{ + }}\infty \} .$

特别地, 本文中我们只关注观测时长上界e有界的情形, 本文所指的有界模型检验指的也是此种情形.

上面给出了ELDI的语法介绍, 其中包含模态词切变, 本文统一记为“; ”.对于模态词切变的解释为

$ {\phi _1};{\phi _2}[{t_1}, {t_2}] \triangleq \exists m.({t_1} \leqslant m \leqslant {t_2}) \wedge {\phi _1}[{t_1}, m] \wedge {\phi _2}[m, {t_2}], $

图 2所示.

Fig. 2 An interpretation for chop 图 2 对于模态词切变的解释

定义3(ELDI的语义解释Iβ).   给定一个实时自动机$\mathcal{A}$和它的一个行为β, 对于给定的命题集合$\mathcal{P}$, 实时自动机$\mathcal{A}$的状态(位置)可能满足或者不满足集合$\mathcal{P}$中的命题.那么在连续时间语义下, 扩展线性时段不变式对于该行为的解释如下.

●对于状态表达式:给定一个时刻$t \in {\mathbb{R}_{ \geqslant 0}}, $

Iβ(0)(t)=0并且Iβ(1)(t)=1;

${{I}_{\beta }}(P)(t)=\left\{ \begin{matrix} 1, \\ 0, \\ \end{matrix} \right.\ $如果t在观察区间内并且系统所处状态满足命题P, 则取1;否则, 取0;

Iβ($\neg $S)(t)=1–Iβ(S)(t);

Iβ(S1$ \vee $S2)(t)=max{Ib(S1)(t), Iβ(S2)(t)}.

●对于时段:给定一个观察区间[t1, t2], 其中, ${t_1}, {t_2} \in {\mathbb{R}_{ \geqslant 0}}$并且t1t2, 那么$\smallint S$的解释为

$ {I_\beta }(\smallint S)([{t_1}, {t_2}]) = \int_{{t_1}}^{{t_2}} {{I_\beta }(S)(t){\rm{d}}t} . $

●对于子式:给定一个观察区间[t1, t2], 一个ELDI子式ϕ的解释为

${I_\beta }, [{t_1}, {t_2}] \vDash \sum\nolimits_{i \in \Omega } {{c_i}\smallint {S_i} \leqslant c} $当且仅当$\sum\nolimits_{i \in \Omega } {{c_i}{I_\beta }(\smallint {S_i})([{t_1}, {t_2}]) \leqslant c} ;$

${I_\beta }, [{t_1}, {t_2}] \vDash \neg \phi $当且仅当Iβ, [t1, t2]不满足ϕ;

${I_\beta }, [{t_1}, {t_2}] \vDash {\phi _1} \vee {\phi _2}$当且仅当${I_\beta }, [{t_1}, {t_2}] \vDash {\phi _1}$${I_\beta }, [{t_1}, {t_2}] \vDash {\phi _2};$

${I_\beta }, [{t_1}, {t_2}] \vDash {\phi _1};{\phi _2}$当且仅当存在$t \in [{t_1}, {t_2}], {I_\beta }, [{t_1}, t] \vDash {\phi _1}$${I_\beta }, [t, {t_2}] \vDash {\phi _2}.$

1.3 量词线性算术

量词线性算术(quantified linear real arithmetic, 简称QLRA)是一种一阶逻辑理论.本文涉及的量词线性算术表达式的语法如下.

定义4(量词线性算术表达式语法)

$ \psi \;:: = {c_0} + {c_1}{x_1} + ... + {c_n}{x_n} \triangleleft 0|\neg \psi {\rm{|}}{\psi _1} \vee {\psi _2}|\forall x.\psi , $

其中, ${c_0}, {c_1}, ..., {c_n} \in \mathbb{R}, \triangleleft \in \{ = , < \} , $其他记号的解释与一阶逻辑和实数算术相同.

2 寻找满足观测时长约束的路径片段.

本节介绍给定一个实时自动机$\mathcal{A}$和观测时长约束[b, e], 求取所有满足时长约束的路径片段.由于本文讨论的时间语义是连续语义, 对于一个时间区间[t, t′], 其包含无穷个时刻点, 那么对于从同一个位置出发具有相同时间长度的执行路径可能有无数条.因此, 本文的基本思路是采用符号化的思想, 求取满足观测时长约束的符号化路径片段.

文献[17]采用基于区域图(zone graph)的方法, 需要先将自动机模型转化为区域图.求取区域图后, 在开始搜索时需要引入一个额外时钟变量t并对区域图中的区域(zone)进行隐式变换, 该时钟变量用来隐式记录路径片段的时间长度.但是求取区域图在最坏情形下会使得搜索空间呈单指数扩大.本文基于实时自动机模型, 所采用的方法不需要像文献[17]那样求取区域图并进行处理, 而是显式地刻画符号化路径片段的时间长度, 这样大大降低了算法时间复杂度.

2.1 符号化路径片段的定义

下面对符号化路径片段及其时间长度给出显性刻画.

定义5(符号化路径片段).  给定一个实时自动机$\mathcal{A}$和它的某个执行$\rho = {s_0}\mathop \to \limits^{{\sigma _1}, {\lambda _1}} {s_1}\mathop \to \limits^{{\sigma _2}, {\lambda _2}} ...\mathop \to \limits^{{\sigma _n}, {\lambda _n}} {s_n}, $那么对于这个执行的某个执行片段${s_i}\mathop \to \limits^{{\sigma _{i + 1}}, {\lambda _{i + 1}}} ...\mathop \to \limits^{{\sigma _j}, {\lambda _j}} {s_j}\mathop \to \limits^{{\sigma _{j + 1}}, {\lambda _{j + 1}}} , $其中, $0 \leqslant i \leqslant j < j + 1 \leqslant n, $其对应的符号化路径片段为$\omega :({s_i}, \mu ({s_i}, $ ${\sigma _{i + 1}}, {s_{i + 1}}))...({s_j}, \mu ({s_j}, {\sigma _{j + 1}}, {s_{j + 1}})).$

可见, 符号化路径片段记录了某个执行片段经过的状态(位置)以及系统在该位置可以停留的时限约束.特别地, 对于执行片段的最后一个位置, 在实时自动机$\mathcal{A}$中没有迁移从该位置发生, 那么可以认为系统可以在该位置停留的时限约束为[0, +$ \propto $].

定义6(符号化路径片段的长度和时间长度).  给定一个符号化执行片段$\omega :({s_i}, \mu ({s_i}, {\sigma _{i + 1}}, {s_{i + 1}}))...({s_j}, \mu ({s_j}, $ ${\sigma _{j + 1}}, {s_{j + 1}})), $它的长度|ω|是指其中离散位置的个数, |ω|=ji+1.它的时间长度||ω||是一个区间, 指的是系统在每个位置停留的时间长度区间加和$\left\| \omega \right\| = \sum\nolimits_i^j {\mu ({s_i}, {\sigma _{i + 1}}, {s_{i + 1}})} .$

2.2 符号化路径片段的搜索算法

根据符号化路径片段的定义, 给定一个实时自动机$\mathcal{A}$和观测时长约束[b, e], 找到所有满足观测时长约束的符号化路径片段即为找到所有$\omega :({s_i}, \mu ({s_i}, {\sigma _{i + 1}}, {s_{i + 1}}))...({s_j}, \mu ({s_j}, {\sigma _{j + 1}}, {s_{j + 1}})), $其中, $\left\| \omega \right\| \cap [b, e] \ne \emptyset .$

寻找的基本思路是从实时自动机的每一个位置出发, 利用深度优先搜索算法寻找.每到一个位置就计算一次当前这条符号化执行片段的时间长度||ω||, 并判断$\left\| \omega \right\| \cap [b, e] \ne \emptyset $是否成立.如果成立, 则说明此条符号化执行路径包含某些满足时长约束的执行片段; 如果不成立, 则说明目前符号化执行片段的长度不满足观测时长约束, 需要更深地搜索或者开始回溯其他分支.深度优先搜索过程依靠一个栈STK实现, 具体过程参考表 1中算法.

Table 1 The algorithm for finding all symbolic path segments whose lengths are in [b, e] 表 1 寻找所有满足观测时长约束[b, e]的符号化路径片段的算法

特别地, 对于一条符号化执行片段的第1个位置, 由于不知道开始观测时系统已在该位置停留了多长时间, 因此需要对于其时间长度进行特殊处理, 即修改在该位置上停留的时间长度的下界为0, 上界不改变.

该算法的输入是实时自动机$\mathcal{A}$和观测时长约束[b, e], 输出为所有满足观测时长约束的符号化路径片段的集合$\Theta $.一开始, $\Theta $为空, 分别从实时自动机$\mathcal{A}$中每一个状态(位置)开始寻找.起初, 当前符号化执行片段w为空($\epsilon $), 将栈STK中栈顶的元素作为ω的下一个位置, 判断当前ω的时间长度与约束[b, e]之间的关系(行9~行10, 行19).第1种情况, 如果当前ω的时间长度区间与约束区间有交集, 说明当前ω是一条满足观测时长约束的符号化路径片段, 那么将当前ω复制到集合$\Theta $(行11).然后继续向前寻找, 查看当前状态是否有后继状态, 如果有, 则将所有后继状态加入到栈中(行12~行14), 如果没有, 则说明需要回溯(行15~行18).第2种情况(第1种情况不满足时进入), 如果当前ω的时间长度区间的最大值小于约束区间的下界b, 则不将ω放入集合$\Theta $中, 直接继续向前寻找(行12~行18), 继续寻找过程与第1种情况处理相同.第3种情况(前两种情况都不满足时进入), 如果当前ω的时间长度区间的最小值第1次超过了时长约束的上界e(行19), 由于是第1次从没有超过上界变为超过上界, 这时同样需要将该符号化执行片段加入集合$\Theta $中; 然后直接开始回溯, 不再向前寻找.直到栈STK为空, 说明以s为开始位置的满足观测时长约束的符号化执行片段已搜索完毕.由于以实时自动机$\mathcal{A}$中所有的状态为起点寻找, 因此, 该算法可以找到所有满足时长约束的符号化执行片段.

2.3 搜索算法的正确性证明

对于算法1的正确性证明, 即需要证明:(1)算法会终止; (2)通过其找到的集合$\Theta $中任意一条符号化路径片段w一定是一条真实的路径片段, 并且时间长度与区间[b, e]相交; (3)任意一条$\mathcal{A}$能够产生的一条符号化路径片段ω, 如果其时间长度与区间[b, e]相交, 那么, 它一定在集合$\Theta $中.因此, 我们证明如下定理.

定理1(算法1正确性).  给定一个实时自动机$\mathcal{A}$和观测时长约束[b, e], 算法1是正确的, 即:

●终止性(termination):算法会终止;

●可靠性(soundness):如果ω是集合$\Theta $中的一条符号化执行路径, 那么, ω一定是$\mathcal{A}$能够产生的一条符号化路径的一个片段, 并且该符号化执行片段的时间长度与区间[b, e]相交;

●完备性(completeness):如果ω$\mathcal{A}$能够产生的一条符号化路径的一个片段, 并且片段的长度与区间[b, e]相交, 那么, ω一定在集合$\Theta $中.

证明:对于终止性来说, 我们只需要证明第6行的while循环会终止, 因为比较明显的是最外层的foreach和最里层的foreach及while循环均能够终止.给定搜索起始位置s, 从s开始的一个满足观测时长约束[b, e]的符号化路径片段ω的长度为$\left| \omega \right|=N\times (1+\left\lceil e/\epsilon \right\rceil ), $其中, N$\mathcal{A}$中状态(位置)个数(|S|), $\epsilon $为假设的一个可控循环消耗的最小时间(不考虑兹诺行为).根据鸽笼原理, 某个状态最多在ω中出现$1+\left\lceil e/\epsilon \right\rceil $也就意味着ω中最多有$\left\lceil e/\epsilon \right\rceil $个可控循环.因此, 从s开始的所有满足观测时长约束[b, e]的符号化路径片段长度最大为$N\times \ \left( 1+\left\lceil e/\epsilon \right\rceil \right)$那么, 找到所有满足观测时长约束的符号化路径片段的循环次数最多为${{N}^{N\times \ \left( 1+\left\lceil e/\epsilon \right\rceil \right)}}$加入到栈中的状态数有上限, 而且每次循环都会去掉栈中一个元素, 因此栈一定会为空, 即循环一定终止.

对于可靠性, 假设ω是集合$\Theta $中的一条符号化执行路径, 显然, 根据算法1找到的执行片段一定是自动机$\mathcal{A}$可以产生的, 并且根据第9行、第10行、第19行的判断条件, 该符号化执行片段的长度与区间[b, e]相交.

对于完备性, 假设$\omega :({s_i}, \mu ({s_i}, {\sigma _{i + 1}}, {s_{i + 1}}))...({s_j}, \mu ({s_j}, {\sigma _{j + 1}}, {s_{j + 1}}))$是自动机$\mathcal{A}$能够产生的一条符号化路径的一个片段, 并且长度区间与约束区间[b, e]相交.那么, 可以构造一个${\omega }'\in \Theta $.首先, 我们让ω'从$({s_i}, \mu ({s_i}, {\sigma _{i + 1}}, {s_{i + 1}}))$开始, 显然, 算法1中第3行可以办到.由于ω是自动机$\mathcal{A}$能够产生的一条符号化路径的一个片段, 那么, ω中的第2个位置$({s_{i + 1}}, \mu ({s_{i + 1}}, {\sigma _{i + 2}}, {s_{i + 2}}))$一定是$({s_i}, \mu ({s_i}, {\sigma _{i + 1}}, {s_{i + 1}}))$的一个后继, 并且$({s_i}, \mu ({s_i}, {\sigma _{i + 1}}, {s_{i + 1}}))({s_{i + 1}}, \mu ({s_{i + 1}}, {\sigma _{i + 2}}, {s_{i + 2}}))$的时间长度的最大值一定小于e, 那么, 根据第9行~第18行, ω'会等于$({s_i}, \mu ({s_i}, {\sigma _{i + 1}}, {s_{i + 1}}))({s_{i + 1}}, \mu ({s_{i + 1}}, {\sigma _{i + 2}}, {s_{i + 2}})).$以此推导, 直到$({s_j}, \mu ({s_j}, {\sigma _{j + 1}}, {s_{j + 1}}))$被加到ω'的最后.那么, ω'会在执行第10行、第11行或者执行第19行、第20行后被加入到$\Theta $中, 即ω′∈$\Theta $.

3 构造量词线性算术表达式

本节我们介绍如何将一条满足观测时长约束的路径片段转化为一个量词线性算术表达式.给定一个观测区间[t, t′], 那么它一定被自动机的状态(位置)所占据, 如图 3所示, 在该段时间区间上, 系统依次处于状态(位置)l1, l2, …, ln(可以有重复状态, 这里为了描述简洁, 重新给出下标号).如果区间长度t′–t在观测区间长度约束[b, e]内, 即bt′–te, 那么, 其对应的路径片段即为一条满足观测时长约束的路径片段.

Fig. 3 Interpretation for introduced variables δ, τ 图 3 对于引入变量δ, τ的解释

对于每一个位置li(1≤in), 我们引入一个变量${\delta _i} \in {\mathbb{R}_{ \geqslant 0}}, $表示系统在该位置停留的时长.对于ELDI子式, 如果含有模态词切变, 例如式子ϕ1; ϕ2; …; ϕr, 那么, 每一个切变点必然位于某个位置lj内.对于某个切变点chopi, 我们引入一个变量${\tau _i} \in {\mathbb{R}_{ \geqslant 0}}.$图 3所示, 如果切变点chopi位于位置lj内, 那么, τi表示从系统进入位置lj到切变点chopi的时间长度.运用引入的这些变量, 我们可以将一条满足观测时长约束的符号化路径片段表达为(l1, δ1)(l2, δ2)…(ln, δn).下面我们给出将其转化为一种量词线性算术表达式的方法.

3.1 构造符号化路径片段的时限约束

首先, 我们需要将这条符号化路径片段的时限约束表示出来, 即刻画实时自动机产生这条符号化路径片段的所有时限约束.这些时限约束包括3种类型:非负约束、加和有界约束和δ约束.

定义7(非负约束).  给定一个满足观测时长约束[b, e]的路径片段(l1, δ1)(l2, δ2)…(ln, δn), 那么, 系统在每个位置的停留时长δi是一个非负实数:

$ \bigcap\limits_{i = 1}^n {({\delta _i} \geqslant 0)} . $

定义8(加和有界约束).  给定一个满足观测时长约束[b, e]的路径片段(l1, δ1)(l2, δ2)...(ln, δn), 那么, 系统在所有位置停留的总时长满足观测时长约束:

$ b \leqslant \mathop \sum \limits_{i = 1}^n {\delta _i} \leqslant e. $

加和有界约束的意义在于, 第2节中求取的每个符号化路径片段的时间长度均是一个区间, 只是与时长约束[b, e]有交集.那么, 加和有界约束则进一步限定, 无论每个δi如何取值, 加和一定需要满足时长约束[b, e], 去除掉路径片段的时间长度在[b, e]约束之外时的δi取值情况.

定义9(δ约束).  给定一个满足观测时长约束[b, e]的路径片段(l1, δ1)(l2, δ2)…(ln, δn), 那么, 系统在每个位置停留的时长δi应满足实时自动机在相应位置停留的时限约束, 即保证该路径片段确实为一条实时自动机能够产生的路径的一个片段.

对于实时自动机, δ约束求取的基本思路如下, 分两种情况加以讨论.

第1种情况, 如果路径片段只含有一个位置(l1, δ1), 那么, 获取实时自动机中所有以位置l1作为源节点的迁移, 可以用迁移上的约束求取系统在该位置停留的时限约束.由于不能够知晓开始观测时系统已经在该位置停留了多长时间, 因此需要对迁移上的约束做出修改, 即将约束下界修改为0即可.例如, 如图 1中, 假设有一个满足时长约束的路径片段为(s1, δ1), 有两条迁移${s_1}\mathop \to \limits^{b, [1, 3]} {s_1}$${s_1}\mathop \to \limits^{c, [2, 4]} {s_2}$s1作为源节点, 那么, 对于某条执行路径, 系统在s1上停留的时限约束为[1,3]或[2,4].由于不知道开始观察时系统已在s1上停留了多长时间, 因此, 观察到系统在s1上停留的时限约束为[0, 3]或[0, 4].那么, 对于这条路径片段来说, δ约束为0≤δ1≤3或0≤δ1≤4.

第2种情况, 如果执行片段长度大于1, 假设路径片段为(l1, δ1)(l2, δ2)…(ln, δn), 那么, 对于路径片段中相邻的两个位置(li, δi)和(li+1, δi+1), 先找到lili+1的所有迁移, 将迁移上的时限约束作为对于(li, di)的δ约束.同样地, 对于(l1, δ1)的δ约束需要处理下界.

由于第2节查找满足观测时限的符号化执行路径时已采用该思想, 因此具体实现时只需将第2节中对于该条符号化执行路径片段所求的每个位置时间长度区间变为相应的δ约束.表 2中算法为生成3种时限约束的算法.该算法输入为某个符号化路径片段ω:(l1, δ1)(l2, δ2)…(ln, δn), 输出为这个符号化路径片段所满足的时限约束$\Gamma $.该算法比较简单, 行2到行3是对每个位置生成其需要满足的δ约束, 运用函数δ_constraint()求取, 具体方法如前所述.第4行将3种类型的约束取交集, 即为时限约束$\Gamma $.

Table 2 The algorithm for generating the timing constraints 表 2 生成时限约束的算法

3.2 构造语义不等式

为了能够用量词线性算术表达式表达每一个线性时段子式$\mathcal{D}$的语义信息, 我们需要构造3种不等式:线性时段子式不等式、t~δ不等式以及τ附加不等式.

定义10(线性时段子式不等式).  给定一个ELDI子式ϕ, 对于其中每一个线性时段子式$\mathcal{D}$, 将$\mathcal{D}$中每一个状态(位置)积分$\smallint {l_i}$用引入的变量δτ表示, 得到的不等式$\mathcal{D}'$即为一个线性时段子式不等式.

定义11(τ~δ不等式).  如果一个切变点chopi落在位置lj内, 那么对应的变量τiδj应满足的不等关系为0≤τiδj, 称为一个τ~δ不等式.

定义12(τ附加不等式).  如果存在两个相邻的切变点chopichopi+1位于同一个位置lj内, 如果chopi+1chopi左边, 那么对应的变量τiτi+1应满足的不等关系为0≤τi+1τi, 称为一个τ附加不等式.

给定一个符号化路径片段ω:(l1, δ1)(l2, δ2)…(ln, δn)和EDLI子式ϕ, 将其翻译为一组不等式的思路是, 根据EDLI子式ϕ的逻辑结构, 分解到每个线性时段子式, 将其翻译为线性时段子式不等式、τ~δ不等式、τ附加不等式; 然后再用相应的逻辑结构组合起来.

●当ϕ是一个线性时段子式, 即假设其含有k个状态积分式子$\smallint {S_1}, \ldots , \smallint {S_k}, $对于ω:(l1, δ1)(l2, δ2)…(ln, δn), $\smallint {S_i} = \sum\nolimits_{{S_i} = {l_j}} {{\delta _j}} , $即将ω中所有与Si相同的位置lj对应的停留时长δj求和, 用该加和表达式代替$\mathcal{D}$$\int {{S}_{i}};$如果没有与Si相同的lj, 则用0代替$\int {{S}_{i}};$.因此得到的线性时段子式不等式为${\mathcal{D}}'=\mathcal{D}\left[ \sum\nolimits_{{{S}_{i}}={{l}_{j}}}{{{{\delta }_{j}}}/{\int {{S}_{i}}}\;} \right],$表示将线性时段子式中的状态积分用相应的变量δ的加和表达式替换.

●当ϕ=$\neg $ϕ, ϕ1$ \vee $ϕ2, ϕ1$\wedge $ϕ2时, 我们将它们递归分解为线性时段子式.

●当ϕ=ϕ1; ϕ2时, 将ω分为两个子片段w1ω2, 分别对应到公式ϕ1ϕ2上, 从而将其转化为与关系($\wedge $)上的两个子问题.

3.3 构造量词线性算术表达式

与文献[17]相比, 本文构造的时限约束和不等式更加明确, 同时, 构造算法中不需要引入额外的δ变量, 即在遇到切变时, 通过已有δ变量和τ变量的算术运算形式来表示片段中被切割的位置分属两个子片段的时间长度(τ, δiτ).由于求解量词线性算术表达式的复杂度与变量个数相关, 因此, 本文采用的方法减少了变量个数, 有效地缩短了求解所需时间.具体算法参考表 3中算法.

Table 3 The algorithm for generating a QLRA formula 表 3 生成一个QLRA公式的算法

表 3中生成一种量词线性算术表达式的算法, 其输入为一个扩展线性时段表达式ϕ和一个符号化路径片段ω:(l1, δ1)(l2, δ2)…(ln, δn); 输出为一个ELDI子式表达式×.整个算法是一种递归算法, 根据扩展线性时段表达式ϕ的逻辑结构进行递归.当递归到某个线性时段子式时, 运用引入的变量的加和形式替换掉式子中的状态积分, 得到线性时段子式不等式(行3).当碰到逻辑连接词时, 根据逻辑连接词的语义, 将问题分解为子问题, 递归地调用本算法.每当碰到一个切变时, 引入一个变量t, 将ω分为两部分(行11), 同时需要添加相应的τ~δ不等式(行11中最后一个不等式).当遇到两个切变点落在同一个状态时, τ~δ不等式会变成一个t附加不等式.例如, 当ϕ1仍然含有切变, 且切变点落在ω1:(l1, δ1)…(li, τ)的最后一个位置时, 新引入的变量t′需要满足的τ~δ不等式为0≤τ'≤τ, 那么, 实际上是一个t附加不等式.当片段有n个位置时, 当前切变点的落位会有n+2种情况, 即在这n个位置之前、在这n个位置中的某个、在这n个位置之后.集合Q记录引入的(多个)τ变量.最后, 我们将引入的δ变量、算法2求出的时限约束表达式$\Gamma $和得到的表达式$\xi $构造一个QLRA表达式$\pi = \forall {\delta _1}, \ldots , {\delta _n}, Q.\Gamma \Rightarrow \xi .$

3.4 构造算法的正确性证明

同样地, 我们需要证明构造算法的正确性, 正确性证明主要依赖递归正确性.

定理2(算法3的正确性).   给定一个满足观测时长约束[b, e]的符号化路径片段ω和ELDI公式ϕ, 算法3是正确的, 即:

●终止性:算法会终止;

●可靠性:如果$\omega \vDash \phi , $那么, QLRA(ϕ, ω)得到的QLRA表达式是满足的(satisfiable);

●完备性:如果QLRA(ϕ, ω)得到的QLRA表达式是满足的, 则$\omega \vDash \phi .$

证明:对于终止性来说, 由于算法是根据ELDI公式ϕ的结构进行递归的, 因此可以看出算法是终止的.对于可靠性和完备性, 下面分析每种递归结构.

●当ϕ是一个线性时段子式, 即$\phi = \mathcal{D} = \sum\nolimits_{i \in \Omega } {{c_i}\smallint {S_i} \leqslant c} $时, ${I_\omega }, [{t_1}, {t_2}] \vDash b \leqslant \ell \leqslant e \Rightarrow \sum\nolimits_{i \in \Omega } {{c_i}\smallint {S_i} \leqslant c} $当且仅当$b \leqslant {t_2} - {t_1} \leqslant e \Rightarrow \sum\nolimits_{i \in \Omega } {{c_i}{I_\omega }(\smallint {S_i})([{t_1}, {t_2}]) \leqslant c} , $其中, t1, t2分别为路径片段的起始时刻和终止时刻.显然, 当按照语义替换后, 仍然有这一关系.因此, 如果$\omega \vDash \phi , $那么, QLRA(ϕ, ω)得到的QLRA表达式是满足的; 如果QLRA(ϕ, ω)得到的QLRA表达式是满足的, 则$\omega \vDash \phi .$

●当ϕ=$\neg $ϕ1时, 对于可靠性, 假设QLRA($\neg $ϕ, ω)不满足, 那么, 根据算法3有$\neg $QLRA(ϕ1, ω)不满足, 也就意味着QLRA(ϕ1, ω)正确.根据归纳假设条件, 我们有$\omega \vDash \phi , $可以得到ω不满足$\neg $ϕ1.对于完备性, 假设QLRA($\neg $ϕ1, ω)正确, 根据算法3有QLRA(ϕ1, ω)不满足.根据归纳假设, 我们有ω不满足$\neg $ϕ1, 因此得到$\omega \vDash \phi .$

●当ϕ=ϕ1$ \vee $ϕ2时, 对于可靠性, 假设QLRA(ϕ1$ \vee $ϕ2, w)不满足, 根据算法3有QLRA(ϕ1, ω)$ \vee $QLRA(ϕ2, w)不满足.根据归纳假设, 我们有ω不满足ϕ1并且ω不满足ϕ2, 因此, ω不满足ϕ1$ \vee $ϕ2.对于完备性, 假设QLRA(ϕ1$ \vee $ϕ2, w)正确, 根据算法3有$\neg $QLRA(ϕ1, ω)或者$\neg $QLRA(ϕ2, ω)不满足.根据归纳假设, 我们有ω不满足ϕ1或者ω不满足ϕ2, 因此得到$\omega \vDash \phi .$

●当ϕ=ϕ1$\wedge $ϕ2时, 证明与ϕ=ϕ1$ \vee $ϕ2类似.

●当ϕ=ϕ1; ϕ2时, 显然$\omega \vDash {\phi _1};{\phi _2}$当且仅当ω被分为两个部分w1ω2${\omega _1} \vDash {\phi _1} \wedge {\omega _2} \vDash {\phi _2}.$根据算法3, 我们选取了所有可能的切变点位置, 并按语义分解为两个子问题${\omega _1} \vDash {\phi _1}$${\omega _2} \vDash {\phi _2}.$因此, 根据归纳假设, 我们得出:如果$\omega \vDash $ ${\phi _1};{\phi _2}, $那么, QLRA(ϕ1; ϕ2, ω)得到的QLRA表达式是满足的; 如果QLRA(ϕ1; ϕ2, ω)得到的QLRA表达式是满足的, 则$\omega \vDash {\phi _1};{\phi _2}.$

3.5 构建量词线性算术表达式举例

下面举例说明如何构建一个量词线性算术表达式.

例2:我们考虑图 1所示的实时自动机以及ELDI公式:$3 \leqslant \ell \leqslant 4 \Rightarrow \smallint {s_0} + \smallint {s_1} \leqslant 1;2\smallint {s_1} - \smallint {s_2} \leqslant 2, $${\mathcal{D}_1} = \smallint {s_0} + $ $\smallint {s_1} \leqslant 1, {\mathcal{D}_2} = 2\smallint {s_1} - \smallint {s_2} \leqslant 2.$现有一条满足观测时长约束的符号化路径片段ω:(s0, δ0)(s1, δ1)(s2, δ2), 可见我们引入了3个δ变量.由于有一个切变, 因此我们引入一个τ变量τ1.

首先, 我们生成符号化路径片段的所有时限约束.对于δ约束, 由于(s0, δ0)是第1个位置, 后继位置为(s1, δ1), 因此, δ0应先取迁移(s0, a, s1)的时限约束, 即1≤δ0≤2.由于(s0, δ0)是第1个位置, 开始观测时并不知道系统在s0已停留多长时间, 因此, 将δ0的下界改为0, 得到δ0的最后约束为0≤δ0≤2.用同样的方法得到(s1, δ1)的时限约束为2≤δ1≤4, (s2, δ2)的时限约束为δ2≥0.非负约束为$({\delta _0} \geqslant 0 \wedge {\delta _1} \geqslant 0 \wedge {\delta _2} \geqslant 0), $加和有界约束为$3 \leqslant {\delta _0} + {\delta _1} + {\delta _2} \leqslant 4.$所有时限约束为$3 \leqslant {\delta _0} + {\delta _1} + {\delta _2} \leqslant 4 \wedge (0 \leqslant {\delta _0} \leqslant 2 \wedge 2 \leqslant {\delta _1} \leqslant 4 \wedge {\delta _2} \geqslant 0) \wedge ({\delta _0} \geqslant 0 \wedge {\delta _1} \geqslant 0 \wedge {\delta _2} \geqslant 0).$

然后, 我们根据算法3来构造不等式和QLRA表达式.由于当前ELDI公式中是一个切变形式, 那么会匹配到第11行, 并有5种可能情况:(1)当切变点落在s0左侧时, ω1为空, ω2为(s0, δ0)(s1, δ1)(s2, δ2), 那么, ${\mathcal{D}_1} = 0 + 0 \leqslant 1, $ ${\mathcal{D}_2} = 2{\delta _1} - {\delta _2} \leqslant 2, $即得到线性时段子式的不等式$0 + 0 \leqslant 1 \wedge 2{\delta _1} - {\delta _2} \leqslant 2.$(2)当切变点落在s0时, ω1为(s0, τ1), ω2为(s0, δ0τ1)(s1, δ1)(s2, δ2), 那么, ${\mathcal{D}_1} = {\tau _1} + 0 \leqslant 1, {\mathcal{D}_2} = 2{\delta _1} - {\delta _2} \leqslant 2, $即得到线性时段子式的不等式${\tau _1} + 0 \leqslant 1 \wedge 2{\delta _1} - $ ${\delta _2} \leqslant 2 \wedge 0 \leqslant {\tau _1} \leqslant {\delta _0}.$(3)当切变点落在s1时, ω1为(s0, δ0)(s1τ1), ω2为(s1, δ1τ1)(s2, δ2), 那么, ${\mathcal{D}_1} = {\delta _0} + {\tau _1} \leqslant 1, {\mathcal{D}_2} = $ $2({\delta _1} - {\tau _1}) - {\delta _2} \leqslant 2, $即得到线性时段子式的不等式${\delta _0} + {\tau _1} \leqslant 1 \wedge 2({\delta _1} - {\tau _1}) - {\delta _2} \leqslant 2 \wedge 0 \leqslant {\tau _1} \leqslant {\delta _1}.$(4)当切变点落在s2时, 用同样的方法得到线性时段子式的不等式为${\delta _0} + {\delta _1} \leqslant 1 \wedge 0 - ({\delta _2} - {\tau _1}) \leqslant 2 \wedge 0 \leqslant {\tau _1} \leqslant {\delta _2}.$(5)当切变点落在s2的右侧时, 用上述方法得到线性时段子式的不等式为${\delta _0} + {\delta _1} \leqslant 1 \wedge 0 - 0 \leqslant 2.$因此, 根据算法3构造的QLRA表达式为

$ \pi = \forall {\delta _0}, \forall {\delta _1}, \forall {\delta _2}, \exists {\tau _1}.3 \leqslant {\delta _0} + {\delta _1} + {\delta _2} \leqslant 4 \wedge (0 \leqslant {\delta _0} \leqslant 2 \wedge 2 \leqslant {\delta _1} \leqslant 4 \wedge {\delta _2} \geqslant 0) \wedge ({\delta _0} \geqslant 0 \wedge {\delta _1} \geqslant 0 \wedge {\delta _2} \geqslant 0) \\ \Rightarrow (0 + 0 \leqslant 1 \wedge 2{\delta _1} - {\delta _2} \leqslant 2) \vee ({\tau _1} + 0 \leqslant 1 \wedge 2{\delta _1} - {\delta _2} \leqslant 2 \wedge 0 \leqslant {\tau _1} \leqslant {\delta _0}) \vee ({\delta _0} + {\tau _1} \leqslant 1 \wedge 2({\delta _1} - {\tau _1}) - {\delta _2} \leqslant 2 \wedge 0 \leqslant {\tau _1} \leqslant {\delta _1}) \\ \vee ({\delta _0} + {\delta _1} \leqslant 1 \wedge 0 - ({\delta _2} - {\tau _1}) \leqslant 2 \wedge 0 \leqslant {\tau _1} \leqslant {\delta _2}) \vee ({\delta _0} + {\delta _1} \leqslant 1 \wedge 0 - 0 \leqslant 2). $
4 求解QLRA表达式及判定定理

根据定理1和定理2, 给定一个实时自动机$\mathcal{A}$和一个观测时长约束有上界的ELDI公式Φ, 我们可以将模型检验问题$\mathcal{A} \vDash {\rm{\Phi }}$转化为QLRA表达式的正确性(validity)问题.

定理3.  给定一个实时自动机$\mathcal{A}$和一个观测时长约束有上界的ELDI公式Φ, $\mathcal{A} \vDash {\rm{\Phi }}$当且仅当$\bigcap\nolimits_{\omega \in Search\left( {\mathcal{A}, \left[ {b, e} \right]} \right)} {QLRA({\rm{\Phi }}, \omega )} $是正确的(valid).

定理3可以从定理1和定理2得出, 这里不再证明.根据Tarski理论, 量词线性算术表达式的可满足性和正确性问题是可以判定的[20], 因此有下面的结论.

定理4.  给定一个实时自动机$\mathcal{A}$和一个观测时长约束有上界的ELDI公式Φ, $\mathcal{A}, [b, e] \vDash {\rm{\Phi }}$是可判定的.

QLRA表示式可以运用量词消去技术求解, 量词消去技术基于柱形代数分解理论(cylindrical algebraic decomposition, 简称CAD)[21], 该方法的最坏复杂度与变量规模呈二阶指数关系, 但是, 由于QLRA表达式中均为线性不等式, 因此, 求解比较迅速.目前, 量词消去技术在许多求解器中都有实现, 例如, REDLOG、QEPCAD[22]、Z3等.

5 工具实现与实验

目前, 我们在Linux平台上实现了一个原型工具, 如图 4所示为工具的架构图.工具接收两个输入:一是, 实时自动机($\mathcal{A}$)模型文件, 格式参考UPPAAL模型文件格式; 二是, 扩展线性时段不变式(ϕ), 存放在一个文本文件中.工具会接收这两个输入, 首先寻找所有满足观测时长约束ℓ的符号化路径片段, 并得到其集合$\Theta $, 然后构造QLRA表达式, 生成所有QLRA表达式的集合Π, 并保存在符合REDLOG输入格式的文本文件中; 然后将该文件传递给量词消去工具REDLOG, REDLOG会依次求解QLRA表达式πi, 并将每个表达式的结果(true or false)记录在一个文本文件中.

Fig. 4 The tool structure 图 4 工具架构图

在实验部分, 我们讨论文献[14, 16]中给出的一个实验.一个实时自动机$\mathcal{A}$N个简单的实时自动机M迭代组成.Mi图 5所示, 由4个状态组成Ai, Bi, Ci, Di, 系统在每个状态上停留一个时间单位.特别地, 对于1≤iN, Di有一条迁移前往Ai+1; 对于1≤jiN, Di有一条迁移前往Aj.文献[14, 16]在离散时间语义下进行了实验, 本文则在标准连续时间语义下进行了实验, 迭代次数N从3到6.表 4是我们的实验结果, tqlra表示生成所有QLRA表达式所用时间, tqe表示运用量词消去工具求解所有QLRA表达式所用时间, ttotal表示验证的总时间, 而ttotal表示采用文献[17]中算法的总时间, 时间单位均为s.我们同样对含有不同逻辑运算符和切变的ELDI式子进行了实验, 工具和实验可以参考https://github.com/Leslieaj/VCELDI.

Fig. 5 The model and property of the experiment 图 5 实验的模型与性质

Table 4 The results of the experiment 表 4 实验结果

由于本文采用标准连续时间语义, 而文献[16]采用离散时间语义, 所以模型检验的总时间比文献[16]中相同问题所用时间要长.这是由于采用方法、基于的模型以及讨论的时间语义不同所致, 我们的优势是可以解决连续时间语义下的模型检验问题.与文献[17]中算法的实验结果相比, 我们的验证方法所用时间明显低于文献[17]验证所需时间, 可见本文方法有效地降低了验证算法的复杂度, 提高了实际验证速度.

6 总结

本文讨论了在连续时间语义下, 对于一个观测时长约束有上界的扩展线性时段不变式(ELDI)在实时自动机上的模型检验问题.本文证明了该问题是可以判定的, 并且给出了判定方法.首先, 我们采用符号化的思想, 运用深度优先搜索得到所有满足观测时长约束的符号化路径片段; 然后, 将每一个符号化路径片段转化为一个量词线性算术表达式; 最后, 运用量词消去工具REDLOG求解这些量词线性算术表达式.

时间复杂度方面, 对于第1步, 我们可以看到算法1与自动机中状态(位置)数目呈一阶指数关系.第2步中, 生成QLRA表达式的算法复杂度是多项式复杂度.最后一步运用量词消去工具求解, 量词消去工具的最坏时间复杂度与变量个数呈二阶指数关系.但是, 根据前文分析, QLRA表示式中均为线性不等式, 所以求解比较快, 近似为多项式和一阶指数, 这一点可以从实验tqlartqe的比较中看出.所以, 对于时间复杂度来说, 与实时自动机的规模和扩展线性时段不变式的切变个数呈一阶指数关系, 最坏是二阶指数关系.而文献[17]中的验证算法复杂度一般为二阶指数, 最坏情况为三阶指数.与文献[17]相比, 复杂度和运行速度方面的优化有以下两点:第一, 缩短了搜索空间, 降低了搜索算法的复杂度, 并减少了所产生的QLRA公式数量; 第二, 对于单个QLRA表达式, 减少了量词的引入个数.从而, 整体上降低了验证算法的复杂度, 并加快了量词消去工具求解时的实际运行速度.

参考文献
[1]
Zhou CC, Hoare CAR, Ravn AP. A calculus of durations. Information Processing Letters, 1991, 40(5): 269-276. [doi:10.1016/0020-0190(91)90122-X]
[2]
Li XS, Zhou CC. Duration calculi:An overview. Chinese Journal of Computers, 1994(11): 842-851(in Chinese with English abstract). http://www.cnki.com.cn/Article/CJFDTOTAL-JSJX411.005.htm
[3]
Halpern JY, Manna Z, Moszkowski BC. A hardware semantics based on temporal intervals. In: Proc. of the 10th Int'l Colloquium on Automata, Languages, and Programming (ICALP). Berlin: Springer-Verlag, 1983. 278-291.[doi: 10.1007/BFb0036915]
[4]
Meyer R, Faber J, Hoenicke J, Rybalchenko A. Model checking duration calculus:A practical approach. Formal Aspects of Computing, 2008, 20(4): 481-505. [doi:10.1007/s00165-008-0082-7]
[5]
Zhou CC, Hansen MR. Duration Calculus:A Formal Approach to Real-Time Systems. Berlin, Heidelberg: Springer-Verlag, 2004. [doi:10.1007/978-3-662-06784-0]
[6]
Zhou CC, Hansen MR, Sestoft P. Decidability and undecidability results for duration calculus. In: Proc. of the 10th Annual Symp. on Theoretical Aspects of Computer Science (STACS). Berlin, Heidelberg: Springer-Verlag, 1993. 58-68.[doi: 10.1007/3-540-56503-5_8]
[7]
Zhou CC, Zhang J, Yang L, Li XS. Linear duration invariants. In: Proc. of the 3rd Int'l Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT). Berlin, Heidelberg: Springer-Verlag, 1994. 86-109.[doi: 10.1007/3-540-58468-4_161]
[8]
Braberman VA, Huang DV. On checking timed automata for linear duration invariants. In: Proc. of the 19th IEEE Real-Time Systems Symp. (RTSS). Washington: IEEE Computer Society, 1998. 264-273.[doi: 10.1109/REAL.1998.739752]
[9]
Li XD, Huang DV. Checking linear duration invariants by linear programming. In: Proc. of the Concurrency and Parallelism, Programming, Networking, and Security: The 2nd Asian Computing Science Conf. (ASIAN). Berlin, Heidelberg: Springer-Verlag, 1996. 321-332.[doi: 10.1007/BFb0027804]
[10]
Li XD, Huang DV, Zheng T. Checking hybrid automata for linear duration invariants. In: Proc. of the Advances in Computing Science: The 3rd Asian Computing Science Conf. (ASIAN). Berlin, Heidelberg: Springer-Verlag, 1997. 166-180.[doi: 10.1007/3-540-63875-X_51]
[11]
Thai P, Huang DV. Verifying linear duration constraints of timed automata. In: Proc. of the 1st Int'l Colloquium on Theoretical Aspects of Computing (ICTAC). Berlin, Heidelberg: Springer-Verlag, 2004. 295-309.[doi: 10.1007/978-3-540-31862-0_22]
[12]
Zhang MM, Huang DV, Liu ZM. Verification of linear duration invariants by model checking CTL properties. In: Proc. of the 5th Int'l Colloquium on Theoretical Aspects of Computing (ICTAC). Berlin, Heidelberg: Springer-Verlag, 2008. 395-409.[doi: 10.1007/978-3-540-85762-4_27]
[13]
Zhang MM, Liu ZM, Zhan NJ. Model checking linear duration invariants of networks of automata. In: Proc. of the 3rd Int'l IPM Conf. on Fundamentals of Software Engineering (FSEN). Berlin, Heidelberg: Springer-Verlag, 2009. 244-259.[doi: 10.1007/978-3-642-11623-0_14]
[14]
Fränzle M, Hansen MR. Efficient model checking for duration calculus based on branching-time approximations. In: Proc. of the 6th IEEE Int'l Conf. on Software Engineering and Formal Methods (SEFM). Washington: IEEE Computer Society, 2008. 63-72.[doi: 10.1109/SEFM.2008.26]
[15]
Fränzle M, Hansen MR. Efficient model checking for duration calculus. Int'l Journal of Software and Informatics, 2009, 3(2-3): 171-196. http://www.wanfangdata.com.cn/details/detail.do?_type=perio&id=CC025016141
[16]
Zu Q, Zhang MM, Zhu JQ, Zhan NJ. Bounded model-checking of discrete duration calculus. In: Proc. of the 16th Int'l Conf. on Hybrid Systems: Computation and Control (HSCC). New York: ACM, 2013. 213-222.[doi: 10.1145/2461328.2461362]
[17]
An J, Zhan NJ, Li XS, Zhang MM, Wang Y. Model checking bounded continuous-time extended linear duration invariants. In: Proc. of the 21st Int'l Conf. on Hybrid Systems: Computation and Control (HSCC). New York: ACM, 2018. 81-90.[doi: 10.1145/3178126.3178147]
[18]
Dima C. Real-time automata. Journal of Automata, Languages and Combinatorics, 2001, 6(1): 3-24. [doi:10.25596/jalc-2001-003]
[19]
Alur R, Dill DL. A theory of timed automata. Theoretical Computer Science, 1994, 126(2): 183-235. http://d.old.wanfangdata.com.cn/OAPaper/oai_arXiv.org_1307.7443
[20]
Tarski A. A Decision Method for Elementary Algebra and Geometry. Berkeley: University of California Press, 1951.
[21]
Collins G. Hauptvortrag: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Proc. of the 2nd GI Conf. on Automata Theory and Formal Languages. Berlin, Heidelberg: Springer-Verlag, 1975. 134-183.[doi: 10.1007/3-540-07407-4_17]
[22]
Brown CW. QEPCAD B:A program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bulletin, 2003, 37(4): 97-108. [doi:10.1145/968708.968710]
[2]
李晓山, 周巢尘. 时段演算综述. 计算机学报, 1994(11): 842-851. http://www.cnki.com.cn/Article/CJFDTOTAL-JSJX411.005.htm