基于实时自动机的连续时段演算的验证*

安 杰, 张苗苗

(同济大学 软件学院,上海 201804)

文献[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节给出量词线性算术的定义.为了叙述简洁,本文固定一组命题集合记为P.

1.1 实时自动机

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

定义1(实时自动机).一个实时自动机RTA是一个6元组A=(S,Σ,Δ,s0,F,μ),其中,

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

·∑是一个有穷字母表;

· Δ⊆S×∑×S是迁移关系;

·s0∈S是初始状态;

·F⊆S是接收状态集合;

·μ:Δ→2ℝ≥0{Ø}是一个时间标签函数(μ(Δ)通常是一些区间的集合,这些区间的端点一般落在ℕ∪{∞}或者ℚ≥0∪{+∞}).

例1:如图1所示为一个实时自动机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]}.

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

1.2 扩展线性时段不变式

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

扩展线性时段不变式在语法上包括 3个组成部分:状态表示式S、线性时段子式D、ELDI子式φ.扩展线性时段不变式的定义如下.

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

其中,P∈P表示状态变量,ci和c为实数,Ω为一个有穷的下标集合.每一个扩展线性时段不变式都可以表示为如下形式:b≤ℓ≤e⇒φ,其中,b∈ℝ≥0,e∈ℝ≥0∪{+∞}.

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

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

如图2所示.

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

· 对于状态表达式:给定一个时刻t∈ℝ≥0,

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

Iβ(¬S)(t)=1-Iβ(S)(t);

Iβ(S1˅S2)(t)=max{Iβ(S1)(t),Iβ(S2)(t)}.

· 对于时段:给定一个观察区间[t1,t2],其中,t1,t2∈ℝ≥0并且t1≤t2,那么∫S的解释为

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

1.3 量词线性算术

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

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

其中,c0,c1,...,cn∈ℝ,◁∈ {=,＜},其他记号的解释与一阶逻辑和实数算术相同.

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

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

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

2.1 符号化路径片段的定义

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

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

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

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

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

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

2.3 搜索算法的正确性证明

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

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

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

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

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

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

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

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

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

对于每一个位置li(1≤i≤n),我们引入一个变量δi∈ℝ≥0,表示系统在该位置停留的时长.对于ELDI子式,如果含有模态词切变,例如式子φ1;φ2;…;φr,那么,每一个切变点必然位于某个位置lj内.对于某个切变点chopi,我们引入一个变量τi∈ℝ≥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是一个非负实数:

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

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

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

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

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

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

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

3.2 构造语义不等式

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

定义10(线性时段子式不等式).给定一个ELDI子式φ,对于其中每一个线性时段子式D,将D中每一个状态(位置)积分∫li用引入的变量δ和τ表示,得到的不等式D′即为一个线性时段子式不等式.

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

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

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

· 当φ=¬φ,φ1˅φ2,φ1˄φ2时,我们将它们递归分解为线性时段子式.

· 当φ=φ1;φ2时,将ω分为两个子片段ω1和ω2,分别对应到公式φ1和φ2上,从而将其转化为与关系(˄)上的两个子问题.

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).当碰到逻辑连接词时,根据逻辑连接词的语义,将问题分解为子问题,递归地调用本算法.每当碰到一个切变时,引入一个变量τ,将ω分为两部分(行11),同时需要添加相应的τ～δ不等式(行11中最后一个不等式).当遇到两个切变点落在同一个状态时,τ～δ不等式会变成一个τ附加不等式.例如,当φ1仍然含有切变,且切变点落在ω1:(l1,δ1)…(li,τ)的最后一个位置时,新引入的变量τ′需要满足的τ～δ不等式为 0≤τ′≤τ,那么,实际上是一个τ附加不等式.当片段有n个位置时,当前切变点的落位会有n+2种情况,即在这n个位置之前、在这n个位置中的某个、在这n个位置之后.集合Q记录引入的(多个)τ变量.最后,我们将引入的δ变量、算法2求出的时限约束表达式Γ和得到的表达式ξ构造一个QLRA表达式π=∀δ1,…,δn,Q.Γ⇒ξ.

3.4 构造算法的正确性证明

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

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

· 终止性:算法会终止;

· 可靠性:如果ω⊧,φ那么,QLRA(φ,ω)得到的QLRA表达式是满足的(satisfiable);

· 完备性:如果QLRA(φ,ω)得到的QLRA表达式是满足的,则ω⊧.φ

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

· 当φ是一个线性时段子式,即φ=D =∑i∈Ωci∫Si≤c时,Iω,[t1,t2]⊧b≤ℓ≤e⇒∑i∈Ωci∫Si≤c当且仅当b≤t2-t1≤e⇒∑i∈Ωci Iω(∫Si)([t1,t2])≤c,其中,t1,t2分别为路径片段的起始时刻和终止时刻.显然,当按照语义替换后,仍然有这一关系.因此,如果ω⊧φ,那么,QLRA(φ,ω)得到的QLRA表达式是满足的;如果QLRA(φ,ω)得到的QLRA表达式是满足的,则ω⊧φ.

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

· 当φ=φ1˅φ2时,对于可靠性,假设QLRA(φ1˅φ2,ω)不满足,根据算法 3 有QLRA(φ1,ω)˅QLRA(φ2,ω)不满足.根据归纳假设,我们有ω不满足φ1并且ω不满足φ2,因此,ω不满足φ1˅φ2.对于完备性,假设QLRA(φ1˅φ2,ω)正确,根据算法3有¬QLRA(φ1,ω)或者¬QLRA(φ2,ω)不满足.根据归纳假设,我们有ω不满足φ1或者ω不满足φ2,因此得到ω⊧φ1˅φ2.

· 当φ=φ1˄φ2时,证明与φ=φ1˅φ2类似.

· 当φ=φ1;φ2时,显然ω⊧φ1;φ2当且仅当ω被分为两个部分ω1和ω2且ω1⊧φ1˄ω2⊧φ2.根据算法3,我们选取了所有可能的切变点位置,并按语义分解为两个子问题ω1⊧φ1和ω2⊧φ2.因此,根据归纳假设,我们得出:如果ω⊧φ1;φ2,那么,QLRA(φ1;φ2,ω)得到的 QLRA 表达式是满足的;如果QLRA(φ1;φ2,ω)得到的 QLRA 表达式是满足的,则ω⊧φ1;φ2.

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

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

例2:我们考虑图1所示的实时自动机以及ELDI公式:3≤ℓ≤4⇒∫s0+∫s1≤1;2∫s1-∫s2≤2,令D1=∫s0+∫s1≤1,D2=2∫s1-∫s2≤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.非负约束为(δ0≥0˄δ1≥0˄δ2≥0),加和有界约束为3≤δ0+δ1+δ2≤4.所有时限约束为3≤δ0+δ1+δ2≤4˄(0≤δ0≤2˄2≤δ1≤4˄δ2≥0)˄(δ0≥0˄δ1≥0˄δ2≥0).

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

π=∀δ0,∀δ1,∀δ2,∃τ1.3≤δ0+δ1+δ2≤4˄(0≤δ0≤2˄2≤δ1≤4˄δ2≥0)˄(δ0≥0˄δ1≥0˄δ2≥0)⇒(0+0≤1˄2δ1-δ2≤2)˅(τ1+0≤1˄2δ1-δ2≤2˄0≤τ1≤δ0)˅(δ0+τ1≤1˄2(δ1-τ1)-δ2≤2˄0≤τ1≤δ1)˅(δ0+δ1≤1˄0-(δ2-τ1)≤2˄0≤τ1≤δ2)˅(δ0+δ1≤1˄0-0≤2).

4 求解QLRA表达式及判定定理

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

定理 3.给定一个实时自动机A和一个观测时长约束有上界的 ELDI公式Φ,A⊧Φ当且仅当∩ω∈Search（A,［b,e］）QLRA(Φ,ω)是正确的(valid).

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

定理4.给定一个实时自动机A和一个观测时长约束有上界的ELDI公式Φ,A,[b,e]⊧Φ是可判定的.

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

5 工具实现与实验

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

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

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

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

6 总 结

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

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