实时并发系统的PTSL模型检测

王晓燕，韩啸,2，彭君，刘淑芬

(1.吉林大学 计算机科学与技术学院，吉林 长春 130012； 2. 吉林大学 学报编辑部，吉林 长春 130012)

实时并发系统的PTSL模型检测

王晓燕1，韩啸1,2，彭君1，刘淑芬1

(1.吉林大学 计算机科学与技术学院，吉林 长春 130012； 2. 吉林大学 学报编辑部，吉林 长春 130012)

随着实时并发系统的软件规模越来越大、复杂性日趋增加，如何保证并发实时系统正确性和可靠性成为日益紧迫的问题。模型检测技术采用自动化的验证算法判断系统是否具有某一性质，它不仅包括对系统模型的遍历以及基于图形的分析方法，而且还需要大量的数值计算。本文把实时并发模型看成对并发博弈模型(CGS)的扩展，在此基础上添加了概率与时间性质，提出了概率时间并发博弈结构(PTCGS)。同时本文还提出了新的逻辑语言-概率时间策略逻辑(PTSL)，它显式地把策略作为一阶逻辑中的对象，从而使我们能够以简单而自然的方式指定PTCGS系统中的非零和属性。PTSL模型检测方法能够让设计者准确知道模型是否满足用户的需求，从而提高系统的可靠性。最后，本文以ZeroConf协议为例来说明PTSL模型检测方法的正确性。

模型检测；概率时间并发博弈结构；概率时间策略逻辑；概率时间自动机；区域图；实时并发系统；博弈模型

实时并发系统被广泛应用在各领域中,例如并发和分布式实时软件、离散事件模拟、通信网络的建模等。这些系统中通常包含若干个并发构件，这些构件之间使用实时信号通信，并具有随机性与不确定性。随着计算机技术的发展，实时并发系统的软件规模越来越大、复杂性日趋增加，如何保证其正确性和可靠性成为日益紧迫的问题，而且由于其内在的非确定性，这个问题难度更大。

在为此提出的诸多理论和方法中，模型检测(model checking)以其简洁明了和自动化程度高而引人注目[1]。模型检测作为形式化验证的一种主流技术，它可以克服传统软件测试用例生成不完备的不足，同时具有验证自动化的优点，并且当验证的性质不满足时，能给出违背性质的反例。模型检测采用了严格的形式化方法对系统进行验证，因此比测试和仿真更能保证系统的正确性。模型检测中常使用数学抽象模型对系统进行建模，概率时间自动机(probabilistic timed automata， PTA)就是其中的一种[2-3]，由于它能同时表示概率性、不确定性和实时性，因此是模型检测实时并发系统的有效工具。

模型检测通过对状态空间的穷举搜索来判定系统是否具有所关心的性质φ，但是随着实时并发系统越来越多地应用在一些对安全性、可靠性要求非常高的领域，如航空系统、电力系统、智能交通系统等，系统一旦发生故障所带来的后果不堪设想，因此设计者需要确切知道在什么情况下系统会出现最坏或者最好的结果，这时候就需要通过模型检测技术找到满足特定性质φ的某个策略或者最佳策略。

目前模型检测主要用时序逻辑来刻画所关心模型的性质，常用的逻辑包括线性时态逻辑LTL(linear temporal logic)、概率计算树逻辑PCTL(probabilistic computation tree logic)、概率时间计算树逻辑PTCTL (probabilistic timed computation tree logic)、交替时间时态逻辑ATL(alternating-time temporal logic)等，当系统中存在多个agent时，LTL、PCTL、PTCTL等不能够明确描述每个agent对象所使用的策略[4-6]，而ATL又不能够描述并发系统中的非零和逻辑[7-8]，于是Henzinger等提出了策略逻辑(strategy logic，SL)[9]，但是SL中缺少对不确定性以及时间的逻辑，因此本文提出概率时间策略逻辑(probabilistic timed strategy logic，PTSL)，把策略作为第一实体对象，能够针对每个模型所使用的策略进行描述，从而使我们能够以简单而自然的方式指定博弈系统中的非零和逻辑属性。

本文的目的是在概率时间并发博弈结构模型基础上，为PTSL逻辑语言提供验证方法。本文的主要贡献如下:

1)在并发博弈结构基础上提出了概率时间并发博弈结构模型；

2)提出的PTSL逻辑语言，它将策略和时态与概率度量相结合；

3)提出基于区域图的PTSL模型检测算法，并证明了区域图中的路径与PTA中的路径的等价性。

1 相关工作

对实时并发系统的模型检测可以分为2类：对并发模型的研究；对并发模型中使用的逻辑语言的研究。在实时并发系统中，通常使用一些控制策略，该策略模型与系统并发模型交互作用，因此完全可以把实时并发模型看成对博弈模型的扩展。而目前博弈模型通常分为两种类型：一种是轮流(turn-based)博弈模型[10]，在整个系统中，可以存在多个玩家，但是在每个状态只能有一个玩家做出选择，从而系统转换到下一个状态；还有一种是并发(concurrent)博弈模型[11]，同样在整个系统中，可以存在多个玩家，但是在每个状态多个玩家可以同时且独立地做出选择。Alfaro等[12]提出了时间博弈自动机，每个游戏者不仅可以选择可能的转换，同时还可以选择转换发生前的等待时间。Thomas Brihaye等[13]提出了时间并发博弈结构TCGS，并使用新的逻辑语言TALTL进行验证。目前在并发模型中使用的逻辑语言的研究更丰富多彩。ATL是博弈模型中的一种典型，用来描述零和逻辑的语言[14]。Taolue Chen等[15]在ATL基础上添加了概率算子，提出了PATL逻辑语言，Henzinger等提出了以策略为第一对象的非零和逻辑语言SL并给出了模型检测算法，Christel Baier等[16]也在ATL基础上提出了一种新的逻辑语言Stochastic Game Logic。

2 概率时间自动机与概率时间并发博弈结构

2.1 时钟与概率时间自动机

定义1 概率时间自动机(probabilistic timed automata, PTA)。PTA是一个八元组P=(L,l0,Act,χ,prob,inv,enab,L), 其中L表示自动机的位置集合;初始位置l0∈S；Act表示有限的动作集合;χ表示P中使用的时钟集合；inv:L→C(χ)是环境函数，它为每个位置指定一个不变式；prob:L×Act→Dist(2χ×L)表示概率转移函数，Dist(L)表示状态L上的条件转移的概率，且L上的所有条件转移的概率和为1，即∑l∈Lθ(l)=1,θ:L→[0,1];enab:L×Act→C(χ)表示动作使能条件;标签函数L:L→2AP表示每个位置上的原子命题。

PTA中的符号状态定义为二元组(l,v)，其中l是符号状态的位置信息，η是时钟赋值且ηinv(l)。因此在符号状态(l,η)上，要么有一定的时间流逝，要么某个动作m∈Act被执行，即

μ(l′,η′)=∑{|prob(l,η)(X,l′)|X∈2χ∧

η′=η[X∶=0]|}

(X,l′)∈2χ×L表示支持动作m转换的一条边，在位置(l,η)上，所有的转换边记为〈e1,e2，…,em〉。从位置迁移的定义可以看出，一旦一个动作m被选择，则时钟会重置并随机选择后继位置。

inv(l1,l2)=inv1(l1)∧inv2(l2)

enab((l1,l2),m)=

prob((l1,l2),m)=

L(l1,l2)=L1∪L2

2.2 概率时间并发博弈结构

由于可以把实时并发模型看成对博弈模型的扩展，本文首先给出由Henzinger等提出的并发博弈CGS模型的定义，如下所示。

定义3 并发博弈结构(concurrent game structure，CGS)。CGS是一个8元组G=(Q,Q0,Σ,τ,Agt,Μ,Γ,Edg)，其中Q是CGS的有限状态集合，Q0是初始状态，Σ表示输入与输出动作集合，τ:Q×M→μ(M)是概率转换函数，其中μ(M)是概率分布函数，Agt={a1,a2,…,ak}是系统中k个agent的集合，M是系统中所有agent可能的动作集合，而Γ定义了每个agent的动作，Edg:Q×Mk→τ表示状态转换表，它包含所有agent的每个状态的状态转移函数。本文使用Edg(q,ma1,ma2,…,mak)表示状态q上的所有agent的动作。

从上面的定义可以看出，在CGS中，由状态qi转换成状态qi+1是由所有的agent共同作用的结果，这也就是说，每个agentaj∈Agt都会根据当前的状态qi选择一个动作mj∈Mv(qi,aj)，因此状态qi转换成状态qi+1需使用Edg(qi,a1,a2,…，ak)表示。

在CGS模型中缺少时钟概念，因此本文对CGS模型进行扩展，在模型中添加时钟，其定义如下所示。

定义4 概率时间并发博弈结构(probabilistic timed concurrent game structure，PTCGS)。PTCGS是一个十元组T=(Q,Q0,Σ,χ,Inv,τ,Agt,Μ,Γ,Edg)，其中(Q,Q0,Σ,χ,Inv,τ)就是PTA，而Agt、Μ、Γ、Edg的含义与CGS中一样。

因此在PTCGS系统中，每个agent都可以使用一个PTA来表示，整个PTCGS系统就是多个PTA的集合。

定义7 策略与联合策略(strategy and coalition strategy)。策略通常表示系统中的agent在不确定性环境下如何在每个状态选择动作，从而找到满足某个性质的解决方案。agentai的策略σi是一个偏序函数，它将有限的路径映射到概率分布函数，即σi:ρ→D(M)，且满足当m∈M(last(ρ))时，σ(ρ)(m)gt;0。联合策略σA是指包含多个agent的策略集合。如果σA中包含所有的agent的策略，即A=Agt,则称其为完全联合策略，否则为不完全联合策略。

3 概率时间策略逻辑语言

为了描述博弈系统的非零和逻辑，Chatterjee和Henzinger提出了策略逻辑(stragegy logic， SL)，该语言把策略作为第一实体对象，但缺少概率与时间特性。本文在SL基础上提出概率时间策略逻辑(probabilistic timed strategy logic，PTSL)，其语法如下所示：

φ∷=p|ζ|φ|φ1∧φ2|

Φ∷=φ1∪≤kφ2|z.Φ

Λ∷=∀x(a,x)Φ|∃x(a,x)Φ|Λ1∧Λ2|Λ

ψ∷=P～λΛ

为了更好地描述时间性质，在PTSL中引入了一个新的时钟符号，称之为公式时钟，且χ∩=∅，χ是PTA模型中的时钟，称为系统时钟。ζ∈(χ∪)是一个时间区域Zone。z.φ表示从时钟z=0的状态开始搜索满足φ的路径，且z∈。∀x·φ含义是任意策略x都满足φ，而∃x.φ表示存在一个策略x满足φ，(a,x)φ是策略赋值公式，表示模型a使用策略x且满足φ，～∈{lt;，≪，gt;，≫}，λ∈[0，1]，k∈R+，概率算子P表示满足公式φ和界限符～λ的路径的概率。在本文中，我们只考虑有两个agent的并发实时系统，因此使用x1，x2，…，表示一个模型使用的策略，用y1，y2，…表示另外一个模型使用的不同策略。

因此使用PTSL语言可以表达如下的属性，例如在ZeroConf协议中，发送者在发送信息后要求接收者要在1s内接收到消息的概率大于等于99%，

P≥0.99[∀x1∀y1(s,x1)(r,y1)z.[s.l.=12∪

(r.l=4∧z≤1)]

定义8 扩展的时间区域。由于在PTSL中存在公式时钟变量z，因此本文将[η,I]称为扩展的时间区域，其中η是系统时钟，I是公式时钟。从而本文使用(l,[η,I])表示PTA中的状态，称为扩展的符号状态。

4 基于region graph的模型检测算法

4.1 基本知识

对于时钟变量x，用kx表示时钟x的上界值。对于实数t，用frac(t)表示t的小数部分，用⎣t」表示t的整数部分。

定义9 时钟等价(clock equivalence)。两个时钟赋值v和v′是等价的，记为v≈v′，当且仅当满足下列所有条件：

1)对于每一个时钟变量x，要么⎣v(x)」=⎣v′(x)」,要么v(x)gt;kx并且v′(x)gt;kx;

2)对于所有的时钟变量x和x′，如果v(x)≤kx并且v′(x)≤kx，那么

①frac(v(x))=0当且仅当frac(v′(x))=0；

②frac(v(x))≤frac(v(x′))当且仅当frac(v′(x))≤frac(v′(x′))。

本文使用[v]表示时钟v所属的等价类，同样可以将≈扩展到符号状态，使用〈l,[v]〉表示状态相同，时间等价的等价类，称其为区域(region)。由于在PTSL有公式时钟，因此在TCGS系统中使用扩展的符号状态(l,[η,I])，而使用〈l,[η,I]〉表示扩展区域。在扩展区域α中，使用zone(α)表示α中的等价时间类。

在PTA模型G中存在多个状态，有的状态存在后继状态，与之对应的区域也会有后继区域，而由多个区域组成的模型称为区域图。

定义10 后继区域(successor region)。扩展区域β=〈l,[η′,I′]〉是α=〈l,[η,I]〉的后继区域，当且仅当存在正数t∈,t′∈，当〈l,[η′+t′,I′+t′]〉∈β,则对任意t≤t′,都有〈l,[η+t,I+t]〉∈α∪β，记为succ(α)=β。

定义11 区域图(region graph)。与PTAP对应的区域图R是一个三元组R(P,Λ)=(R*,Steps*,L*)，其中R*表示扩展区域的集合，对于任意扩展区域α=〈l,[η,I]〉∈R*转换函数Steps*包含以下3种类型的转换。

1)时间迁移：当succ([η,I])inv(l),则

2)位置迁移：如果存在概率p′∈prob(l)而且[η,I]满足PTA中的位置转换条件τl(p′)，则

3)自身循环

标签函数L*的定义如下所示：

L*〈l,[η,I]〉=L(l)∪

{pζ|[η,I]满足ζ，ζ∈Z(χ∪)(Λ)}

由于在验证过程中需要使用区域图上的策略，其定义如下。

定义13 区域图上的策略(adversary)。在区域图中的策略σR将有限路径ω*映射到概率p且p∈Steps*(last(ω*))。

下面介绍在区域图上的PTSL满足关系。

定义14 PTSL的满足关系。给定区域图(P,Λ)以及PTSL公式φ，则PTSL在上的满足关系定义如下：

(l,[η,I])true，对于所有l,η,I均成立

(l,[η,I])p⟺p∈L*(l,[η,I])

(l,[η,I])φ1∧φ2⟺

(l,[η,I])φ1and(l,[η,I])φ2

(l,[η,I])φ⟺(l,[η,I])φ

(l,[η,I])Λ1∧Λ2⟺

(l,[η,I])Λ1and(l,[η,I])Λ2

(l,[η,I])Λ⟺(l,[η,I])Λ

(l,[η,I])φ1∪≤kφ2⟺存在整数i,j及路径ω*，且ω*(i)φ1，且对于任意i≤j≤i+k，都有ω*(j)φ2。

以上定义的满足关系与PCTL的满足关系的定义基本相同，而PTSL中独有的3个操作符——时钟重置z、任意算子∀以及存在算子∃满足关系定义如下。

(l,[η,I])z.φ⟺

(l,[η,I[z:=0]])σAφ

(l,[η,I])∀x(a,x)Φ⟺∀x∈σanda∈

A,(l,[η,I])Φ

(l,[η,I])∃x(a,x)Φ⟺∃x∈σanda∈

A,(l,[η,I])Φ

将带有概率算子公式P～λΛ展开，可以得到公式(1)、(2)、(3)：

(l,[η,I])P≥λ∀x∀y(a,x)(b,y)Φ(1)

(l,[η,I])P≥λ∀x∃y(a,x)(b,y)Φ(2)

(l,[η,I])P≥λ∃x∃y(a,x)(b,y)Φ(3)

公式(1)～(3)的概率值以及σA的求解过程是本文验证算法的核心。

4.2 验证算法

本节将介绍基于区域图的PTSL验证算法。本文将该算法分为3步：1)构建TCGS系统的区域图；2)在区域图上解析PTSL公式；3)在TCGS系统中找到满足公式的路径。

从PTA构造区域图的方法按照区域图的定义就可以得到，本文不再给出转换算法。本文重点介绍在区域图上解析PTSL公式的过程,首先仍旧是构建PTSL的语法树。在语法树上，叶节点代表原子命题，而内部节点标识PTSL中的操作符标识包括∧,,∪≤k,P等，PTSL的验证算法如下所示。

算法1 PTSL验证算法

foreachφ′ in sub(φ)do

caseφ′=p: [φ′]:={(l,[η,I])|l∈Lamp;l∈L(p)}

caseφ′=θ: [φ′]:={(l,[η,I])|(l,[η,I])/θ}

caseφ′=θ1∧θ2:[φ′]:={(l,[η,I])|(l,[η,I])θ1∩(l,[η,I])θ2}

caseφ′=ζ: [φ′]:={(l,[η,I])|l∈L∧I∈pζ}

caseφ′=z.θ:

[φ′]:={(l,[η,ζ[z:=0]])|(l,[η,ζ])θ}

caseφ′=θ1∪≤kθ2:Until(θ1,θ2,≤k)

caseφ′=P～λ∀x∀y(a,x)(b,y)θ: [φ′]:=P1θ

caseφ′=P～λ∀x∃y(a,x)(b,y)θ:[φ′]:=P2θ

caseφ′=P～λ∃x∃y(a,x)(b,y)θ:[φ′]:=P3θ

…

PTSL与PCTL的不同之处在于存在以下几个操作：时钟重置z.φ、任意∀x(a,x)·Φ以及存在∃x(a,x)·Φ，因此对于PTSL中其他的操作符，例如,∧,∨,∪≤k等，都可以采用PCTL中原有的算法，这里不作详细介绍。ζ是公式时钟，pζ的定义在区域图中已经给出，表示满足时间赋值的命题。依据PCTL语义，P～λΛ的计算方法如下所示：

从定义可以看出，求解P～λΛ的值的问题其实是求解极值的问题。依据这个思路，我们来叙述式(1)～(3)的计算过程。

为了叙述的方便，下面将～λ直接定义为≥λ。

从PTSL的满足关系可知，式(1)的含义是，无论agenta和agentb使用任何策略，所找到的路径的目标状态都满足Φ且概率大于等于λ，因此λ是agenta和agentb使用联合策略σA=(x,y)下所得的最小值。从而我们可以将式(1)转换为求解最小值问题。式(2)中P≥λ∃x∃y(a,x)(b,y)Φ的含义是，agenta和agentb存在某个策略，所找到的路径的目标状态满足Φ且概率≥λ，这也就是说，找到一条满足条件的路径即可，因此可以将式(2)转换为求解最大概率问题。式(3)的含义是无论agenta使用任何策略，agentb都会找到某个策略y使所找到的路径的目标状态满足Φ且概率≥λ。因为a可以使用任意策略，所以式(3)其实是求解最小概率问题。以上将式(1)～(3)求解概率≥λ的情形进行了分析，而≤λ恰好是相反的情形，在这里不再赘述。有关在区域图中寻找概率最优解的方法与在MDP中的方法一样，可以使用value iteration的方法查找整个模型中的概率最大最小值[17]。而公式时钟z值的计算则是将找到的满足θ的路径中的各个区域的时间最大值相加起来即可。

当在区域图中找到了满足条件的路径ω*后，这并不是最终解，还需要在TCGS系统中构建与ω*相对应的路径ω，另外还需要证明ω*与ω的概率是一样的，这样才能保证最终找到的路径ω是正确的。

构建ω过程采用递归方法，算法如下所示。

算法2 构建w过程

BuildPathFromRG(R,ω*)

length∶=(|ω*|;i∶=0;ω∶=∅;Trans:=∅;

Whileilt;length

if(i=0) amp;(η0,I)∈[η0,I0]

ω:ω∪(l0,η0);

else

if (ηi,I+Dω(i))∈[ηi,Ii]

ω:=ω∪(li,ηi);

Trans:=Trans∪{(li-1,ηi-1),(mi,pi),(li,ηi)}

return (ω,Trans)

5 实验与结果

本文以ZeroConf协议为例说明PTSL的模型检测方法。ZeroConf协议是一种用于局域网内自动生成可用IP地址的网络技术。设备S连接网络后，首先随机地选择一个IP地址，然后设备S会向网络中的其他设备连续K次发送“这个IP地址是否已经被占用”的询问信息， 如果设备S没有收到任何应答，则它会使用该IP地址，否则只要收到过1个“IP地址被占用”的应答，设备S就会重新选择IP地址。本文使用的模型是由Cheshire等建立的MDP模型修改而来[18]，为environment模型添加了消息丢失的概率，表示网络中的其他设备在应答设备S的询问时，发送的信息有可能发生丢失，本文使用参数plost表示。则sender模型和environment模型如图1、2所示。

图1 sender模型Fig.1 sender model

图2 environment模型Fig.2 environment model

为了验证模型，在Prism中重新设计实现了PTSL逻辑语言，并使用PTA模型表示并发实时系统中的agent，使用PTA的组合模型表示整个PTCGS模型。组合后的PTA模型转换成区域图后，状态节点一共有631个，在本文中不能全部给出，本文只给出几个关键节点的图，如图3所示。

图3 区域图模型片段Fig.3 Fragment of region graph model

图3中每个节点的值如下所示：

l[0]=((s=0,probes=0,ip=0,coll=0,e=0),{x=0,y=0,x=y})

l[1]=((s=1,probes=0,ip=0,coll=0,e=0),{x=0,y=0,x=y})

l[2]=((s=3,probes=0,ip=1,coll=0,e=0),{x=0,y=20,x-y=-20})

l[3]=((s=3,probes=0,ip=1,coll=0,e=0),{x=1,y=20,x-y=-19})

l[4]=((s=3,probes=0,ip=1,coll=0,e=0),{x=2,y=20,x-y=-18})

l[5]=((s=3,probes=0,ip=2,coll=0,e=0),{x=0,y=20,x-y=-20})

l[6]=((s=3,probes=0,ip=2,coll=0,e=0),{x=1,y=20,x-y=-19})

l[7]=((s=3,probes=0,ip=2,coll=0,e=0),{x=2,y=20,x-y=-18})

l[8]=((s=3,probes=1,ip=1,coll=0,e=0),{x=0,y=40,x-y=-40})

l[9]=((s=3,probes=1,ip=1,coll=0,e=0),{x=0,y=39,x-y=-39})

l[10]=((s=3,probes=1,ip=1,coll=0,e=0),{x=0,y=38,x-y=-38})

l[11]=((s=3,probes=1,ip=2,coll=0,e=0),{x=0,y=0,x=y})

l[12]=((s=3,probes=1,ip=2,coll=0,e=1),{x=0,y=0,x=y})

首先求新入网的设备可以成功分配到未使用的IP的概率，使用PTSL的属性公式为

P≥λ∀x∀y(a,x)(b,y)(true∪(s=6amp;ip=2))

表1为测试时的数据取值，从结果可以看出，当网络中节点数N值变化较大时，最后成功获得IP地址的概率不会发生很大的变化。

表1 ZeroConf的实验结果1

使用PTSL求解在大于等于T时间内设备仍未成功分配到IP的概率的属性公式为

P≥λ∀x∃y(a,x)(b,y)z.(!(s=6amp;ip=2)∧z≥T)

表2为测试时的数据取值，从结果可以看出，当时间限界T较小时(≤10)，发生不能配置合适的IP的概率大一些，而时间限界T≥20时不能成功获得IP地址的概率几乎为0，完全符合ZeroConf协议的标准。

表2 ZeroConf的实验结果2

6 结束语

本文在CGS模型基础上添加了概率及时间约束，提出了一种新的并发模型PTCGS。并根据PTCGS特点，提出了新的逻辑语言PTSL，它在SL逻辑的基础上添加了时间与概率特性，把策略作为第一实体对象，能够针对每个模型所使用的策略进行描述，从而使我们能够以简单而自然的方式指定PTCGS系统中的非零和逻辑属性，并给出了基于区域图的模型检测算法。最后以ZeroConf协议为例来说明PTSL的模型检测方法的正确性。

[1]CLARKE E, GRUMBERG O, PELED D. Model Checking[M]. Cambridge : MIT press， 1999: 5-60.

[2]BEAUQUIER D. On probabilistic timed automata[J]. Theoretical computer science, 2003, 292(1): 65-84.

[3]KWIATKOWSKA M, NORMAN G, SEGALA R, et al. Automatic verification of real-time systems with discrete probability distributions[J]. Theoretical computer science ,2002, 282: 101-150.

[4]CLARKE E, EMERSON A. Design and synthesis of synchronization skeletons using branching time temporal logic[C]//Proceedinns of the Workshop Logic of Programs.Newyork, US, 1981: 52-71.

[5]HANSSON H， JONSSON B. A logic for reasoning about time and reliability[J]. Formal aspects of computing, 1994, 6(5): 512-535.

[6]ALFARO de L. Temporal Logics for the Specification of Performance and Reliability[C]//Proc STACS’97.New York, US, 1997: 165-176.

[7]ALUR R, HENZINGER T A, KUPFERMAN O. Alternating-time temporal logic[J]. Journal of the ACM, 2002, 49: 672-713.

[8]CHATTERJEE K， HENZINGER T A. Strategy improvement for stochastic Rabin and Strett Games[C]//Proc DBLP 2006. Bonn, Germany, 2006: 375-389.

[9]CHATTERJEE K, HENZINGER T A, PITERMAN N. Strategy logic[J]. Information and computation, 2007, 208(6): 677-693.

[10]Basset N, Kwiatkowska M, Topcu U, et al. Strategy synthesis for stochastic games with multiple long-run objectives[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Germany, 2015:256-271.

[11]KRISHNENDU Chatterjee, LUCA de Alfaro, THOMAS A,et al. Strategy improvement for concurrent reachability and turn-based stochastic safety games[J]. Journal of computer and system sciences， 2013, 79: 640-657.

[12]ALFARO L de, FAELLA M, HENZINGER T, et al. The element of surprise in timed games[C]//14thInternational Conference on Concurrency Theory. Marceille, France ,2003: 144-158.

[13]THOMAS Brihaye, FRAN Cois, LAROUSSINIE, et al. Timed Concurrent Game Structures[C]//Proceedings of the 18th international conference on Concurrency Theory. Lisbon, Portugal, 2007: 445-459.

[14]RAJEEV A, THOMAS A, HENZINGER, et al. Alternating-time temporal logic[J]. Journal of the ACM， 2002 ,49(5): 672-713 .

[15]CHEN Taolue, LU Jian. Probabilistic alternating-time temporal logic and model checking algorithm[C]// Fourth International Conference on Fuzzy Systems and Knowledge Discovery (FSKD), 2007. Haikou, China, 2007: 35-39.

[16]CHRISTEL Baier, TOMBrázdil, MARCUS Größer, et al. Stochastic game logic[C]//Conference: Quantitative Evaluation of Systems. Edinburgh, UK ,2007: 227-236.

[17]MARTA Kwiatkowska A , GETHIN Norman A , JEREMY Sproston B, et al. Symbolic model checking for probabilistic timed automata[J]. Information and computation, 2007, 205(2): 1027-1077.

[18]MARTA Kwiatkowska, GETHIN Norman, DAVID Parker, et al. Performance analysis of probabilistic timed automata using digital clocks[J]. Formal methods in system design, 2006, 29(1): 33-78.

王晓燕，女，1977年生，讲师，博士，主要研究方向为软件建模与验证技术、软件开发新方法。申请发明专利2项，并获得2010年中国国家专利优秀奖，2008年吉林省科技进步一等奖，中国商业科技进步二等奖。发表论文20余篇，其中被SCI收录5篇。

韩啸，男， 1981年生，编辑，博士研究生，主要研究方向为网络协同、软件建模和网络技术。

彭君，男，1981年生，讲师，博士，主要研究方向为模型驱动技术、构件技术、软件体系结构。

PTSLmodelcheckingoftimedconcurrentsystem

WANG Xiaoyan1， HAN Xiao1,2， PENG Jun1， LIU Shufen1

(1.College of Computer Science and Technology, Jilin University, Changchun 130012, China; 2. Editorial Office on Journal, Jilin University, Changchun 130012, China)

With the increased scale and complexity of real-time concurrent software systems, ensuringtheir correctness and reliability has become a matter of urgency. Current model-checking technology uses an automated demonstration algorithm to judgesystem properties, which must include the traversal in the system model and graph-based analysis techniques as well asextensive numerical computations. In this paper, we consider the timed concurrency model as an extension of the concurrent game model (CGS) and addprobability and time properties to propose a new probabilistic timed concurrent game structure (PTCGS). We also propose a new logic language called probabilistic timed strategy logic (PTSL), which uses strategy as the object in the first-order logic to specify the nonzero-sum attributes in a simple and natural way. Lastly, we give an example usingthe ZeroConf protocol to demonstrate the correctness of the PTSL model checking method.

model checking; probabilistic timed concurrent game structure; probabilistic timed strategy logic; probabilistic timed automata; region graph; timed concurrent system; game model

10.11992/tis.201706008

http://kns.cnki.net/kcms/detail/23.1538.TP.20170728.1901.012.html

TP311

A

1673-4785(2017)05-0694-08

中文引用格式：王晓燕，韩啸，彭君，等.实时并发系统的PTSL模型检测J.智能系统学报， 2017, 12(5): 694-701.

英文引用格式：WANGXiaoyan,HANXiao,PENGJun，etal.PTSLmodelcheckingoftimedconcurrentsystemJ.CAAItransactionsonintelligentsystems, 2017, 12(5): 694-701.

2017-06-05. < class="emphasis_bold">网络出版日期

日期：2017-07-28.

国家自然科学基金项目(61502196).

王晓燕. E-mail：wangxy@jlu.edu.cn.