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

在为此提出的诸多理论和方法中，模型检测(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 时钟与概率时间自动机

时钟x表示记录时间的非负实数变量，设X={x₁, x₂, …，x_n}是有限的时钟变量集合，则时钟赋值函数u:X→R_≥0表示对所有x_i∈X分配一个非负实数。设t≥0，u+t表示对所有x_i∈X增加t，即u+t(x)=u(x)+t, 其中x∈X。通常使用0表示对X中的所有时钟赋值0。时钟约束是一组有关时间变量的原子公式的合取，记为C(χ)，语法定义为Z∷=x~d|x-y~d|Z∧Z|true，其中x, y∈X, d∈N, ~∈{ < , ≤}。当时钟赋值v满足时钟约束χ时，记为υ⊨x。所有满足时钟约束的时钟赋值构成的集合称为时区(zone)。

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

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

1) 时间迁移：$(l, \eta)\xrightarrow{d}(l', \eta ')$, 当且仅当l=l′, η′=η+d，并且η′⊨inv(l)。

2) 位置迁移：$(l, \eta)\xrightarrow{m}(l', \eta ')$, 当且仅当η⊨enab(l, m)并且

$ \begin{array}{*{20}{c}} {\mu \left( {l',\eta '} \right) = \sum {\left\{ {\left| {{\rm{prob}}\left( {l,\eta } \right)\left( {X,l'} \right)} \right|X \in {2^\chi } \wedge } \right.} }\\ {\left. {\left. {\eta ' = \eta \left[ {X: = 0} \right]} \right|} \right\}} \end{array} $

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

定义2  PTA组合(PTA composition)。两个PTA(${\mathbb{P}_1}$和${\mathbb{P}_2}$)的组合定义为：${\mathbb{P}_1}\left\| {{\mathbb{P}_2}} \right.$=(L₁×L₂, (l₁, l₂), Act₁∪Act₂, χ₁∪χ₂, prob, inv, enab, $\mathscr{L}$)，其中对于位置(l₁, l₂)∈L₁×L₂及动作m∈Act₁∪Act₂:

$ \begin{array}{*{20}{c}} {{\rm{inv}}\left( {{l_1},{l_2}} \right) = {\rm{in}}{{\rm{v}}_1}\left( {{l_1}} \right) \wedge {\rm{in}}{{\rm{v}}_2}\left( {{l_2}} \right)}\\ {{\rm{enab}}\left( {\left( {{l_1},{l_2}} \right),m} \right) = }\\ {\left\{ \begin{array}{l} {\rm{ena}}{{\rm{b}}_1}\left( {{l_1},m} \right) \wedge {\rm{ena}}{{\rm{b}}_2}\left( {{l_2},m} \right),m \in {\rm{Ac}}{{\rm{t}}_1} \cup {\rm{Ac}}{{\rm{t}}_2}\\ {\rm{ena}}{{\rm{b}}_1}\left( {{l_1},m} \right),m \in {\rm{Ac}}{{\rm{t}}_1}\backslash {\rm{Ac}}{{\rm{t}}_2}\\ {\rm{ena}}{{\rm{b}}_2}\left( {{l_2},m} \right),m \in {\rm{Ac}}{{\rm{t}}_2}\backslash {\rm{Ac}}{{\rm{t}}_1} \end{array} \right.} \end{array} $

$ \begin{array}{*{20}{c}} {{\rm{prob}}\left( {\left( {{l_1},{l_2}} \right),m} \right) = }\\ {\left\{ \begin{array}{l} {\rm{pro}}{{\rm{b}}_1}\left( {{l_1},m} \right) \otimes {\rm{pro}}{{\rm{b}}_2}\left( {{l_2},m} \right),m \in {\rm{Ac}}{{\rm{t}}_1}\backslash {\rm{Ac}}{{\rm{t}}_2}\\ {\rm{pro}}{{\rm{b}}_1}\left( {{l_1},m} \right) \otimes {\mu _{\left( {\phi ,{l_2}} \right)}},m \in {\rm{Ac}}{{\rm{t}}_1}\backslash {\rm{Ac}}{{\rm{t}}_2}\\ {\mu _{\left( {\phi ,{l_1}} \right)}} \otimes {\rm{pro}}{{\rm{b}}_2}\left( {{l_2},m} \right),m \in {\rm{Ac}}{{\rm{t}}_2}\backslash {\rm{Ac}}{{\rm{t}}_1} \end{array} \right.}\\ {\mathscr{L}\left( {{l_1},{l_2}} \right) = {\mathscr{L}_1} \cup {\mathscr{L}_2}} \end{array} $

2.2 概率时间并发博弈结构

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

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

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

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

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

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

定义5  路径(path)。PTCGS的一条路径ρ是一条有限或者无限序列：$\rho =({{q}_{0}}, {{\eta }_{0}})\xrightarrow{{{t}_{0}}, {{m}_{0}}, {{p}_{0}}}({{q}_{1}}, {{\eta }_{1}})\xrightarrow{{{t}_{1}}, {{m}_{1}}, {{p}_{1}}}\cdots $。本文使用s(ρ, k)表示路径中的第k+1个状态。而m(ρ, k)表示路径中的第k+1个动作，last(ρ)表示最后一个状态。

定义6  路径持续时间(duration of a path)。给定PTA模型$\mathbb{P}$及其路径ω，则${{D}_{\omega }}(i)=\sum\limits_{j=0}^{i-1}{{{t}_{j}}}$表示路径ω上的节点i发生位置迁移时流逝的时间和，当i=0时，D_ω(0)=0。

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

3 概率时间策略逻辑语言

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

$ \varphi :: = p\left| \zeta \right|\neg \varphi \left| {{\varphi _1} \wedge {\varphi _2}} \right| $

$ \mathit{\Phi }:: = {\varphi _1}{ \cup ^{ \le k}}{\varphi _2}\left| {z.\mathit{\Phi }} \right. $

$ \Lambda :: = \forall x\left( {a,x} \right)\mathit{\Phi }\left| {\exists x\left( {a,x} \right)\mathit{\Phi }\left| {{\Lambda _1} \wedge {\Lambda _2}} \right|} \right.\neg \Lambda $

$ \psi :: = {P_{ \sim \lambda }}\Lambda $

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

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

$ \begin{array}{*{20}{c}} {{P_{ \ge 0.99}}\left[ {\forall {x_1}\forall {y_1}\left( {s,{x_1}} \right)\left( {r,{y_1}} \right)z.\left[ {{\rm{s}}.l. = 12 \cup } \right.} \right.}\\ {\left. {\left( {r.l = 4 \wedge z \le 1} \right)} \right]} \end{array} $

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

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

模型检测PTSL的问题就是，给定概率时间并发博弈结构PTCGS $\mathbb{T}$及PTSL的表达式∅，能否找到σ_A使之满足∅。在TCGS系统中，通常使用的属性验证公式是概率公式P_~λΛ，并且在公式中通常也含有公式时钟z，因此求解满足$\Pr {\rm{ob}}\left({\left\{ {\omega \left| \begin{array}{l} \omega \in {\rm{Path}}\left\langle {l, [\eta, \Im ]} \right\rangle \\ l, [\eta, \Im ], {\sigma _A} = \Lambda \end{array} \right.} \right\}} \right)$~λ公式的σ_A是算法的关键。

4.1 基本知识

对于时钟变量x，用k_x表示时钟x的上界值。对于实数t，用frac(t)表示t的小数部分，用$\left\lfloor t \right\rfloor $表示t的整数部分。

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

1) 对于每一个时钟变量x，要么$\left\lfloor {v(x)} \right\rfloor = \left\lfloor {v'(x)} \right\rfloor $, 要么v(x)>k_x并且v′(x)>k_x;

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

① 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, [η, $\Im $])，而使用〈l, [η, $\Im $]〉表示扩展区域。在扩展区域α中，使用zone(α)表示α中的等价时间类。

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

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

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

1) 时间迁移：当succ([η, $\Im $])⊨inv(l), 则

$ p_{{\rm{succ}}}^\alpha \beta = \left\{ \begin{array}{l} 1,\;\;\;\;\beta = {\rm{succ}}\left( \alpha \right)\\ 0,\;\;\;\;其他 \end{array} \right. $

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

$ p_{{\rm{succ}}}^\alpha \beta = \sum\limits_{\begin{array}{*{20}{c}} {X \subseteq \chi }\\ {{\rm{zone}}\left( \alpha \right)\left[ {{X_0}} \right]{\rm{zone}}\left( \beta \right)} \end{array}} {p'\left( {l',X} \right)} $

3) 自身循环

$ p_{{\rm{succ}}}^\alpha \beta = \left\{ \begin{array}{l} 1,\;\;\;\;\beta = \alpha \\ 0,\;\;\;\;其他 \end{array} \right. $

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

$ \begin{array}{*{20}{c}} {{L^ * }\left\langle {l,\left[ {\eta ,\Im } \right]} \right\rangle = L\left( l \right) \cup } \\ {\left\{ {{p_\zeta }\left| {\left[ {\eta ,\Im } \right]} \right.满足\;\zeta ,\zeta \in {Z_{\left( {\chi \cup \mathbb{Z}} \right)}}\left( \Lambda \right)} \right\}} \end{array} $

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

定义12  区域图上路径(path on the region graph)。${{\omega }^{*}}=\left\langle {{l}_{0}}, [{{\eta }_{0}}, {{\Im }_{0}}] \right\rangle \xrightarrow{{{p}_{0}}}\left\langle {{l}_{1}}, [{{\eta }_{1}}, {{\Im }_{1}}] \right\rangle \xrightarrow{{{p}_{1}}}\left\langle {{l}_{2}}, [{{\eta }_{2}}, {{\Im }_{2}}] \right\rangle \xrightarrow{{{p}_{2}}}\cdots $, 其中p_i∈Step s^*〈 l_i, [η_i, $\Im $_i]〉，且p_i>0。

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

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

定义14  PTSL的满足关系。给定区域图$\mathbb{R}$($\mathbb{P}$, Λ)以及PTSL公式ϕ，则PTSL在$\mathbb{R}$上的满足关系定义如下：

$ \begin{array}{*{20}{c}} {\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| { = {\rm{true}}} \right.,对于所有\;l,\eta ,\Im \;均成立}\\ {\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| { = p \Leftrightarrow p \in {L^ * }\left( {l,\left[ {\eta ,\Im } \right]} \right)} \right.}\\ {\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| { = {\phi _1} \wedge {\phi _2} \Leftrightarrow } \right.}\\ {\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| { = {\phi _1}\;{\rm{and}}} \right.\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| { = {\phi _2}} \right.}\\ {\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| { = \neg \phi \; \Leftrightarrow } \right.\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| { = \phi } \right.}\\ {\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| { = {\Lambda _1} \wedge {\Lambda _2} \Leftrightarrow } \right.}\\ {\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| { = {\Lambda _1}\;{\rm{and}}} \right.\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| { = {\Lambda _2}} \right.}\\ {\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| { = \neg \Lambda \; \Leftrightarrow } \right.\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| { = \Lambda } \right.} \end{array} $

(l, [η, $\Im $])⊨ϕ₁∪^≤kϕ₂ ⇔存在整数i, j及路径ω^*，且ω^*(i)⊨ϕ₁，且对于任意i≤j≤i+k，都有ω^*(j)⊨ϕ₂。

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

$ \begin{array}{*{20}{c}} {\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| { = z.\phi \Leftrightarrow } \right.}\\ {\left( {l,\left[ {\eta ,\Im \left[ {z: = 0} \right]} \right]} \right)\left| { = {\sigma _A}\phi } \right.}\\ {\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| = \right.\forall x\left( {a,x} \right)\mathit{\Phi } \Leftrightarrow \forall x \in \sigma \;{\rm{and}}\;a \in }\\ {A,\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| { = \mathit{\Phi }} \right.}\\ {\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| = \right.\exists x\left( {a,x} \right)\mathit{\Phi } \Leftrightarrow \exists x \in \sigma \;{\rm{and}}\;a \in }\\ {A,\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| { = \mathit{\Phi }} \right.} \end{array} $

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

$ \left( {l,\left[ {\eta ,\Im } \right]} \right)\left| { = {P_{ \ge \lambda }}\forall x\forall y} \right.\left( {a,x} \right)\left( {b,y} \right)\mathit{\Phi } $

(1)

$ \left( {l,\left[ {\eta ,\Im } \right]} \right)\left| { = {P_{ \ge \lambda }}\forall x\exists y} \right.\left( {a,x} \right)\left( {b,y} \right)\mathit{\Phi } $

(2)

$ \left( {l,\left[ {\eta ,\Im } \right]} \right)\left| { = {P_{ \ge \lambda }}\exists x\exists y} \right.\left( {a,x} \right)\left( {b,y} \right)\mathit{\Phi } $

(3)

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

4.2 验证算法

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

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

算法1  PTSL验证算法

$ {\rm{foreach}}\;\varphi '\;{\rm{in}}\;{\rm{sub}}\left( \varphi \right){\rm{do}} $

$ {\rm{case}}\;\varphi '\; = p: = \left[ {\varphi '} \right]: = \left\{ {\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| {l \in L\& l \in L\left( p \right)} \right.} \right\} $

$ {\rm{case}}\;\varphi '\; = \neg \theta : = \left[ {\varphi '} \right]: = \left\{ {\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| {\left( {l,\left[ {\eta ,\Im } \right]} \right)} \right| \ne \theta } \right\} $

$ \begin{array}{l} {\rm{case}}\;\varphi '\; = {\theta _1} \wedge {\theta _2}:\left[ {\varphi '} \right]: = \left\{ {\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| {\left( {l,\left[ {\eta ,} \right.} \right.} \right.} \right.\\ \left. {\left. {\left. \Im \right]} \right)\left| = \right.{\theta _1} \cap \left( {l,\left[ {\eta ,\Im } \right]} \right)\left| = \right.{\theta _2}} \right\} \end{array} $

$ {\rm{case}}\;\varphi '\; = \zeta :\left[ {\varphi '} \right]: = \left\{ {\left( {l,\left[ {\eta ,\Im } \right]} \right)\left| {l \in L \wedge \Im \in {p_\zeta }} \right.} \right\} $

$ \begin{array}{l} {\rm{case}}\;\varphi '\; = z.\theta :\\ \left[ {\varphi '} \right]: = \left\{ {\left( {l,\left[ {\eta ,\zeta \left[ {z: = 0} \right]} \right]} \right)\left| {\left( {l,\left[ {\eta ,\zeta } \right]} \right)\left| = \right.\theta } \right.} \right\} \end{array} $

$ {\rm{case}}\;\varphi '\; = {\theta _1}{ \cup ^{ \le k}}{\theta _2}:{\rm{Until}}\left( {{\theta _1},{\theta _2} \le k} \right) $

$ {\rm{case}}\;\varphi '\; = {P_{ \sim \lambda }}\forall x\forall y\left( {a,x} \right)\left( {b,y} \right)\theta : = \left[ {\varphi '} \right]: = {P_1}\theta $

$ {\rm{case}}\;\varphi '\; = {P_{ \sim \lambda }}\forall x\exists y\left( {a,x} \right)\left( {b,y} \right)\theta : = \left[ {\varphi '} \right]: = {P_2}\theta $

$ \begin{array}{*{20}{c}} {{\rm{case}}\;\varphi '\; = {P_{ \sim \lambda }}\exists x\exists y\left( {a,x} \right)\left( {b,y} \right)\theta : = \left[ {\varphi '} \right]: = {P_3}\theta }\\ \cdots \end{array} $

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

$ {P_{ \sim \lambda }}\Lambda = \left\{ \begin{array}{l} {p_{\max }}\Lambda ,\;\;\;\;\; \sim \in \left\{ { < , \le } \right\}\\ {p_{\min }}\Lambda ,\;\;\;\;\; \sim \in \left\{ { > , \ge } \right\} \end{array} \right. $

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

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

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

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

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

算法2  构建w过程

BuildPathFromRG($\mathbb{R}$, ω^*)

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

While i < length

  if(i=0) & (η₀, $\Im $)∈[η₀, $\Im $₀]

      ω:ω∪(l₀, η₀);

else

    if (η_i, $\Im $+D_ω(i))∈[η_i, $\Im $_i]

      ω:=ω∪(l_i, η_i);

Trans:=Trans∪{(l_i-1, η_i-1), (m_i, p_i), (l_i, η_i)}

      return (ω, Trans)

证明  ω^*与ω的概率是一样的, 即Prob(ω^*)= Prob(ω)。设在区域r_i发生转换前概率为p，区域r_i中包含m个时间转换，n个位置转换，k个自身循环。从区域图的定义可以看出，当发生时间迁移和自身循环时概率均为1，且这两个迁移不会改变区域位置，转换后的概率为p×1×1×1…=p, 故而概率值没有任何改变。而发生位置迁移时，ω^*中的概率为p_i^*={Σp_i(X, l_i+1)|X⊆χ, zone(α) [X:=0]=zone(β)}，ω中的概率为μ={Σp_i (X, l_i+1)|X∈2^χ∧(η_i+t_i)[X:=0]=η_i+1}，由于区域r_i中有m个时间转换，因此zone (α)=[η_i+d_m, ε+D_ω(i)+d_m]，zone (β)=[η_i+1, ε+D_ω(i+1)+d_i+1]，而(η_i+t_i)[X:=0]∈[η_i+d_m][X:=0], η_i+1∈[η_i+1]，因此p_i^*=μ。

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所示。

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

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

$ \begin{array}{l} l\left[ 0 \right] = \left( {\left( {s = 0,{\rm{probes}} = 0,{\rm{ip}} = 0,{\rm{coll}} = 0,e = 0} \right),} \right.\\ \left. {\left\{ {x = 0,y = 0,x = y} \right\}} \right) \end{array} $

$ \begin{array}{l} l\left[ 1 \right] = \left( {\left( {s = 1,{\rm{probes}} = 0,{\rm{ip}} = 0,{\rm{coll}} = 0,e = 0} \right),} \right.\\ \left. {\left\{ {x = 0,y = 0,{\rm{x}} = {\rm{y}}} \right\}} \right) \end{array} $

$ \begin{array}{l} l\left[ 2 \right] = \left( {\left( {s = 3,{\rm{probes}} = 0,{\rm{ip}} = 1,{\rm{coll}} = 0,e = 0} \right),} \right.\\ \left. {\left\{ {x = 0,y = 20,{\rm{x}} - {\rm{y}} = - 20} \right\}} \right) \end{array} $

$ \begin{array}{l} l\left[ 3 \right] = \left( {\left( {s = 3,{\rm{probes}} = 0,{\rm{ip}} = 1,{\rm{coll}} = 0,e = 0} \right),} \right.\\ \left. {\left\{ {x = 1,y = 20,x - y = - 19} \right\}} \right) \end{array} $

$ \begin{array}{l} l\left[ 4 \right] = \left( {\left( {s = 3,{\rm{probes}} = 0,{\rm{ip}} = 1,{\rm{coll}} = 0,e = 0} \right),} \right.\\ \left. {\left\{ {x = 2,y = 20,x - y = - 18} \right\}} \right) \end{array} $

$ \begin{array}{l} l\left[ 5 \right] = \left( {\left( {s = 3,{\rm{probes}} = 0,{\rm{ip}} = 2,{\rm{coll}} = 0,e = 0} \right),} \right.\\ \left. {\left\{ {x = 0,y = 20,x - y = - 20} \right\}} \right) \end{array} $

$ \begin{array}{l} l\left[ 6 \right] = \left( {\left( {s = 3,{\rm{probes}} = 0,{\rm{ip}} = 2,{\rm{coll}} = 0,e = 0} \right),} \right.\\ \left. {\left\{ {x = 1,y = 20,x - y = - 19} \right\}} \right) \end{array} $

$ \begin{array}{l} l\left[ 7 \right] = \left( {\left( {s = 3,{\rm{probes}} = 0,{\rm{ip}} = 2,{\rm{coll}} = 0,e = 0} \right),} \right.\\ \left. {\left\{ {x = 2,y = 20,x - y = - 18} \right\}} \right) \end{array} $

$ \begin{array}{l} l\left[ 8 \right] = \left( {\left( {s = 3,{\rm{probes}} = 1,{\rm{ip}} = 1,{\rm{coll}} = 0,e = 0} \right),} \right.\\ \left. {\left\{ {x = 0,y = 40,x - y = - 40} \right\}} \right) \end{array} $

$ \begin{array}{l} l\left[ 9 \right] = \left( {\left( {s = 3,{\rm{probes}} = 1,{\rm{ip}} = 1,{\rm{coll}} = 0,e = 0} \right),} \right.\\ \left. {\left\{ {x = 0,y = 39,x - y = - 39} \right\}} \right) \end{array} $

$ \begin{array}{l} l\left[ {10} \right] = \left( {\left( {s = 3,{\rm{probes}} = 1,{\rm{ip}} = 1,{\rm{coll}} = 0,e = 0} \right),} \right.\\ \left. {\left\{ {x = 0,y = 38,x - y = - 38} \right\}} \right) \end{array} $

$ \begin{array}{l} l\left[ {11} \right] = \left( {\left( {s = 3,{\rm{probes}} = 1,{\rm{ip}} = 2,{\rm{coll}} = 0,e = 0} \right),} \right.\\ \left. {\left\{ {x = 0,y = 0,x = y} \right\}} \right) \end{array} $

$ \begin{array}{l} l\left[ {12} \right] = \left( {\left( {s = 3,{\rm{probes}} = 1,{\rm{ip}} = 2,{\rm{coll}} = 0,e = 1} \right),} \right.\\ \left. {\left\{ {x = 0,y = 0,x = y} \right\}} \right) \end{array} $

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

$ {P_{ \ge \lambda }}\forall x\forall y\left( {a,x} \right)\left( {b,y} \right)\left( {{\rm{true}} \cup \left( {s = 6\& {\rm{ip}} = 2} \right)} \right) $

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

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

$ {P_{ \ge \lambda }}\forall x\exists y\left( {a,x} \right)\left( {b,y} \right)z.\left( {!\left( {s = 6\& {\rm{ip}} = 2} \right) \wedge z \ge T} \right) $

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

6 结束语

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