第12卷第5期 智能系统学报 Vol.12 No.5 2017年10月 CAAI Transactions on Intelligent Systems 0ct.2017 D0I:10.11992/is.201706008 网络出版地址：http:/kns.cmki.net/kcms/detail/23.1538.TP.20170728.1901.012.html 实时并发系统的PTSL模型检测 王晓燕，韩啸2，彭君，刘淑芬 (1.吉林大学计算机科学与技术学院，吉林长春130012：2.吉林大学学报编辑部，吉林长春130012) 摘要：随着实时并发系统的软件规模越来越大、复杂性日趋增加，如何保证并发实时系统正确性和可靠性成为日 益紧迫的问题。模型检测技术采用自动化的验证算法判断系统是否具有某一性质，它不仅包括对系统模型的遍历 以及基于图形的分析方法，而且还需要大量的数值计算。本文把实时并发模型看成对并发博弈模型(CGS)的扩展， 在此基础上添加了概率与时间性质，提出了概率时间并发博弈结构(PTCGS)。同时本文还提出了新的逻辑语言-概 率时间策略逻辑(PTSL),它显式地把策略作为一阶逻辑中的对象，从而使我们能够以简单而自然的方式指定PTCGS 系统中的非零和属性。PTSL模型检测方法能够让设计者准确知道模型是否满足用户的需求，从而提高系统的可靠 性。最后，本文以ZeroConf协议为例来说明PTSL模型检测方法的正确性。 关键词：模型检测：概率时间并发博弈结构：概率时间策略逻辑：概率时间自动机：区域图：实时并发系统：博弈模型 中图分类号：TP311文献标志码：A文章编号：1673-4785(2017)05-0694-08 中文引用格式：王晓燕，韩啸，彭君，等.实时并发系统的PTSL模型检测[J].智能系统学报，2017,12(5)：694-701. 英文引用格式：WANG Xiaoyan,HAN Xiao,.PENGJun,etal.PTSL model checking of timed concurrent system[J].CAAI transactions on intelligent systems,2017,12(5):694-701. PTSL model checking of timed concurrent system WANG Xiaoyan',HAN Xiao'2,PENG Jun',LIU Shufen' (1.College of Computer Science and Technology,Jilin University,Changchun 130012,China;2.Editorial Office on Journal,Jilin University,Changchun 130012,China) Abstract: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. Keywords:model checking;probabilistic timed concurrent game structure;probabilistic timed strategy logic; probabilistic timed automata;region graph;timed concurrent system;game model 实时并发系统被广泛应用在各领域中，例如并些构件之间使用实时信号通信，并具有随机性与不 发和分布式实时软件、离散事件模拟、通信网络的 确定性。随着计算机技术的发展，实时并发系统的 建模等。这些系统中通常包含若干个并发构件，这 软件规模越来越大、复杂性日趋增加，如何保证其 正确性和可靠性成为日益紧迫的问题，而且由于其 收稿日期：2017-06-05.网络出版日期：2017-07-28. 内在的非确定性，这个问题难度更大。 基金项目：国家自然科学基金项目(61502196). 通信作者：王晓燕.E-mail:wangxy@ju.cd.cm. 在为此提出的诸多理论和方法中，模型检测
第 １２ 卷第 ５ 期 智 能 系 统 学 报 Ｖｏｌ．１２ №．５ ２０１７ 年 １０ 月 ＣＡＡＩ Ｔｒａｎｓａｃｔｉｏｎｓ ｏｎ Ｉｎｔｅｌｌｉｇｅｎｔ Ｓｙｓｔｅｍｓ Ｏｃｔ． ２０１７ ＤＯＩ：１０．１１９９２ ／ ｔｉｓ．２０１７０６００８ 网络出版地址：ｈｔｔｐ： ／ ／ ｋｎｓ．ｃｎｋｉ．ｎｅｔ ／ ｋｃｍｓ／ ｄｅｔａｉｌ ／ ２３．１５３８．ＴＰ．２０１７０７２８．１９０１．０１２．ｈｔｍｌ 实时并发系统的 ＰＴＳＬ 模型检测 王晓燕１ ，韩啸１，２ ，彭君１ ，刘淑芬１ （１．吉林大学 计算机科学与技术学院，吉林 长春 １３００１２； ２． 吉林大学 学报编辑部，吉林 长春 １３００１２） 摘 要：随着实时并发系统的软件规模越来越大、复杂性日趋增加，如何保证并发实时系统正确性和可靠性成为日 益紧迫的问题。 模型检测技术采用自动化的验证算法判断系统是否具有某一性质，它不仅包括对系统模型的遍历 以及基于图形的分析方法，而且还需要大量的数值计算。 本文把实时并发模型看成对并发博弈模型（ＣＧＳ）的扩展， 在此基础上添加了概率与时间性质，提出了概率时间并发博弈结构（ＰＴＣＧＳ）。 同时本文还提出了新的逻辑语言－概 率时间策略逻辑（ＰＴＳＬ），它显式地把策略作为一阶逻辑中的对象，从而使我们能够以简单而自然的方式指定 ＰＴＣＧＳ 系统中的非零和属性。 ＰＴＳＬ 模型检测方法能够让设计者准确知道模型是否满足用户的需求，从而提高系统的可靠 性。 最后，本文以 ＺｅｒｏＣｏｎｆ 协议为例来说明 ＰＴＳＬ 模型检测方法的正确性。 关键词：模型检测；概率时间并发博弈结构；概率时间策略逻辑；概率时间自动机；区域图；实时并发系统；博弈模型 中图分类号：ＴＰ３１１ 文献标志码：Ａ 文章编号：１６７３－４７８５（２０１７）０５－０６９４－０８ 中文引用格式：王晓燕，韩啸，彭君，等．实时并发系统的 ＰＴＳＬ 模型检测［Ｊ］． 智能系统学报， ２０１７， １２（５）： ６９４－７０１． 英文引用格式：ＷＡＮＧ Ｘｉａｏｙａｎ， ＨＡＮ Ｘｉａｏ， ＰＥＮＧ Ｊｕｎ， ｅｔ ａｌ． ＰＴＳＬ ｍｏｄｅｌ ｃｈｅｃｋｉｎｇ ｏｆ ｔｉｍｅｄ ｃｏｎｃｕｒｒｅｎｔ ｓｙｓｔｅｍ ［ Ｊ］． ＣＡＡＩ ｔｒａｎｓａｃｔｉｏｎｓ ｏｎ ｉｎｔｅｌｌｉｇｅｎｔ ｓｙｓｔｅｍｓ， ２０１７， １２（５）： ６９４－７０１． ＰＴＳＬ ｍｏｄｅｌ ｃｈｅｃｋｉｎｇ ｏｆ ｔｉｍｅｄ ｃｏｎｃｕｒｒｅｎｔ ｓｙｓｔｅｍ ＷＡＮＧ Ｘｉａｏｙａｎ １ ， ＨＡＮ Ｘｉａｏ １，２ ， ＰＥＮＧ Ｊｕｎ １ ， ＬＩＵ Ｓｈｕｆｅｎ １ （１．Ｃｏｌｌｅｇｅ ｏｆ Ｃｏｍｐｕｔｅｒ Ｓｃｉｅｎｃｅ ａｎｄ Ｔｅｃｈｎｏｌｏｇｙ， Ｊｉｌｉｎ Ｕｎｉｖｅｒｓｉｔｙ， Ｃｈａｎｇｃｈｕｎ １３００１２， Ｃｈｉｎａ； ２． Ｅｄｉｔｏｒｉａｌ Ｏｆｆｉｃｅ ｏｎ Ｊｏｕｒｎａｌ， Ｊｉｌｉｎ Ｕｎｉｖｅｒｓｉｔｙ， Ｃｈａｎｇｃｈｕｎ １３００１２， Ｃｈｉｎａ） Ａｂｓｔｒａｃｔ： Ｗｉｔｈ ｔｈｅ ｉｎｃｒｅａｓｅｄ ｓｃａｌｅ ａｎｄ ｃｏｍｐｌｅｘｉｔｙ ｏｆ ｒｅａｌ⁃ｔｉｍｅ ｃｏｎｃｕｒｒｅｎｔ ｓｏｆｔｗａｒｅ ｓｙｓｔｅｍｓ， ｅｎｓｕｒｉｎｇｔｈｅｉｒ ｃｏｒｒｅｃｔｎｅｓｓ ａｎｄ ｒｅｌｉａｂｉｌｉｔｙ ｈａｓ ｂｅｃｏｍｅ ａ ｍａｔｔｅｒ ｏｆ ｕｒｇｅｎｃｙ． Ｃｕｒｒｅｎｔ ｍｏｄｅｌ⁃ｃｈｅｃｋｉｎｇ ｔｅｃｈｎｏｌｏｇｙ ｕｓｅｓ ａｎ ａｕｔｏｍａｔｅｄ ｄｅｍｏｎｓｔｒａｔｉｏｎ ａｌｇｏｒｉｔｈｍ ｔｏ ｊｕｄｇｅｓｙｓｔｅｍ ｐｒｏｐｅｒｔｉｅｓ， ｗｈｉｃｈ ｍｕｓｔ ｉｎｃｌｕｄｅ ｔｈｅ ｔｒａｖｅｒｓａｌ ｉｎ ｔｈｅ ｓｙｓｔｅｍ ｍｏｄｅｌ ａｎｄ ｇｒａｐｈ⁃ ｂａｓｅｄ ａｎａｌｙｓｉｓ ｔｅｃｈｎｉｑｕｅｓ ａｓ ｗｅｌｌ ａｓｅｘｔｅｎｓｉｖｅ ｎｕｍｅｒｉｃａｌ ｃｏｍｐｕｔａｔｉｏｎｓ． Ｉｎ ｔｈｉｓ ｐａｐｅｒ， ｗｅ ｃｏｎｓｉｄｅｒ ｔｈｅ ｔｉｍｅｄ ｃｏｎｃｕｒｒｅｎｃｙ ｍｏｄｅｌ ａｓ ａｎ ｅｘｔｅｎｓｉｏｎ ｏｆ ｔｈｅ ｃｏｎｃｕｒｒｅｎｔ ｇａｍｅ ｍｏｄｅｌ （ＣＧＳ） ａｎｄ ａｄｄｐｒｏｂａｂｉｌｉｔｙ ａｎｄ ｔｉｍｅ ｐｒｏｐｅｒｔｉｅｓ ｔｏ ｐｒｏｐｏｓｅ ａ ｎｅｗ ｐｒｏｂａｂｉｌｉｓｔｉｃ ｔｉｍｅｄ ｃｏｎｃｕｒｒｅｎｔ ｇａｍｅ ｓｔｒｕｃｔｕｒｅ （ ＰＴＣＧＳ）． Ｗｅ ａｌｓｏ ｐｒｏｐｏｓｅ ａ ｎｅｗ ｌｏｇｉｃ ｌａｎｇｕａｇｅ ｃａｌｌｅｄ ｐｒｏｂａｂｉｌｉｓｔｉｃ ｔｉｍｅｄ ｓｔｒａｔｅｇｙ ｌｏｇｉｃ （ＰＴＳＬ）， ｗｈｉｃｈ ｕｓｅｓ ｓｔｒａｔｅｇｙ ａｓ ｔｈｅ ｏｂｊｅｃｔ ｉｎ ｔｈｅ ｆｉｒｓｔ⁃ｏｒｄｅｒ ｌｏｇｉｃ ｔｏ ｓｐｅｃｉｆｙ ｔｈｅ ｎｏｎｚｅｒｏ⁃ｓｕｍ ａｔｔｒｉｂｕｔｅｓ ｉｎ ａ ｓｉｍｐｌｅ ａｎｄ ｎａｔｕｒａｌ ｗａｙ． Ｌａｓｔｌｙ， ｗｅ ｇｉｖｅ ａｎ ｅｘａｍｐｌｅ ｕｓｉｎｇｔｈｅ ＺｅｒｏＣｏｎｆ ｐｒｏｔｏｃｏｌ ｔｏ ｄｅｍｏｎｓｔｒａｔｅ ｔｈｅ ｃｏｒｒｅｃｔｎｅｓｓ ｏｆ ｔｈｅ ＰＴＳＬ ｍｏｄｅｌ ｃｈｅｃｋｉｎｇ ｍｅｔｈｏｄ． Ｋｅｙｗｏｒｄｓ：ｍｏｄｅｌ ｃｈｅｃｋｉｎｇ； ｐｒｏｂａｂｉｌｉｓｔｉｃ ｔｉｍｅｄ ｃｏｎｃｕｒｒｅｎｔ ｇａｍｅ ｓｔｒｕｃｔｕｒｅ； ｐｒｏｂａｂｉｌｉｓｔｉｃ ｔｉｍｅｄ ｓｔｒａｔｅｇｙ ｌｏｇｉｃ； ｐｒｏｂａｂｉｌｉｓｔｉｃ ｔｉｍｅｄ ａｕｔｏｍａｔａ； ｒｅｇｉｏｎ ｇｒａｐｈ； ｔｉｍｅｄ ｃｏｎｃｕｒｒｅｎｔ ｓｙｓｔｅｍ； ｇａｍｅ ｍｏｄｅｌ 收稿日期：２０１７－０６－０５． 网络出版日期：２０１７－０７－２８． 基金项目：国家自然科学基金项目（６１５０２１９６）． 通信作者：王晓燕． Ｅ⁃ｍａｉｌ：ｗａｎｇｘｙ＠ ｊｌｕ．ｅｄｕ．ｃｎ． 实时并发系统被广泛应用在各领域中，例如并 发和分布式实时软件、离散事件模拟、通信网络的 建模等。 这些系统中通常包含若干个并发构件，这 些构件之间使用实时信号通信，并具有随机性与不 确定性。 随着计算机技术的发展，实时并发系统的 软件规模越来越大、复杂性日趋增加，如何保证其 正确性和可靠性成为日益紧迫的问题，而且由于其 内在的非确定性，这个问题难度更大。 在为此提出的诸多理论和方法中，模型检测
第5期 王晓燕，等：实时并发系统的PTSL模型检测 695· (model checking)以其简洁明了和自动化程度高而 1 引人注目山。模型检测作为形式化验证的一种主 相关工作 流技术，它可以克服传统软件测试用例生成不完备 对实时并发系统的模型检测可以分为2类：对 的不足，同时具有验证自动化的优点，并且当验证 并发模型的研究：对并发模型中使用的逻辑语言的 的性质不满足时，能给出违背性质的反例。模型检 研究。在实时并发系统中，通常使用一些控制策 测采用了严格的形式化方法对系统进行验证，因此 略，该策略模型与系统并发模型交互作用，因此完 比测试和仿真更能保证系统的正确性。模型检测 全可以把实时并发模型看成对博弈模型的扩展。 中常使用数学抽象模型对系统进行建模，概率时间 而目前博弈模型通常分为两种类型：一种是轮流 自动机(probabilistic timed automata,PTA)就是其中 (turm-based)博弈模型[o],在整个系统中，可以存在 的一种[2-】，由于它能同时表示概率性、不确定性和 多个玩家，但是在每个状态只能有一个玩家做出选 实时性，因此是模型检测实时并发系统的有效工具。 择，从而系统转换到下一个状态：还有一种是并发 模型检测通过对状态空间的穷举搜索来判定 (concurrent)博弈模型[山，同样在整个系统中，可以 系统是否具有所关心的性质b,但是随着实时并发 存在多个玩家，但是在每个状态多个玩家可以同时 系统越来越多地应用在一些对安全性、可靠性要求 且独立地做出选择。Alfaro等[2]提出了时间博弈 非常高的领域，如航空系统、电力系统、智能交通系 自动机，每个游戏者不仅可以选择可能的转换，同 统等，系统一旦发生故障所带来的后果不堪设想， 时还可以选择转换发生前的等待时间。Thomas 因此设计者需要确切知道在什么情况下系统会出 Brihaye等u)提出了时间并发博弈结构TCGS,并使 现最坏或者最好的结果，这时候就需要通过模型检 用新的逻辑语言TALTL进行验证。目前在并发模 型中使用的逻辑语言的研究更丰富多彩。ATL是 测技术找到满足特定性质中的某个策略或者最佳 博弈模型中的一种典型，用来描述零和逻辑的语 策略。 言a)。Taolue Chen等[s]在ATL基础上添加了概 目前模型检侧主要用时序逻辑来刻画所关心 率算子，提出了PATL逻辑语言，Henzinger等提出 模型的性质，常用的逻辑包括线性时态逻辑LTL 了以策略为第一对象的非零和逻辑语言SL并给出 (linear temporal logic)、概率计算树逻辑PCTL 了模型检测算法，Christel Baier等[16也在ATL基础 (probabilistic computation tree logic)、概率时间计算 上提出了一种新的逻辑语言Stochastic Game Logic. 树逻辑PTCTL(probabilistic timed computation tree logic)、交替时间时态逻辑ATL(alternating-time 2 概率时间自动机与概率时间并发 temporal logic)等，当系统中存在多个agent时，LTL、 博奔结构 PCTL、PTCTL等不能够明确描述每个agent对象所 2.1 时钟与概率时间自动机 使用的策略46]，而ATL又不能够描述并发系统中 时钟x表示记录时间的非负实数变量，设X= 的非零和逻辑[-)，于是Henzinger等提出了策略逻 {x1,x2,…,xn}是有限的时钟变量集合，则时钟赋值 辑(strateg罗logic,SL)9,但是SL中缺少对不确定性 函数u:X一→R=表示对所有x:∈X分配一个非负实 以及时间的逻辑，因此本文提出概率时间策略逻辑 数。设t≥0，u+t表示对所有x:∈X增加t,即u+ (probabilistic timed strateg罗logic,PTSL）,把策略作 t(x)=u(x)+t,其中x∈X。通常使用0表示对X中 为第一实体对象，能够针对每个模型所使用的策略 的所有时钟赋值0。时钟约束是一组有关时间变量 进行描述，从而使我们能够以简单而自然的方式指 的原子公式的合取，记为C(X),语法定义为Z:= 定博弈系统中的非零和逻辑属性。 x~d|x-y~d|ZA Z true,其中x,y∈X,d∈N,~∈ 本文的目的是在概率时间并发博弈结构模型 {<,≤}。当时钟赋值v满足时钟约束X时，记为v 基础上，为PTSL逻辑语言提供验证方法。本文的 =x。所有满足时钟约束的时钟赋值构成的集合称 主要贡献如下： 为时区(zone)。 1)在并发博弈结构基础上提出了概率时间并 定义1概率时间自动机(probabilistic timed 发博弈结构模型： automata,PTA)。PTA是一个八元组P=(L,lo, 2)提出的PTSL逻辑语言，它将策略和时态与 Act,X,prob,inv,enab,,其中L表示自动机的位 概率度量相结合； 置集合：初始位置lo∈S;Act表示有限的动作集合； 3)提出基于区域图的PTSL模型检测算法，并 X表示P中使用的时钟集合：iv:L→C(X)是环境函 证明了区域图中的路径与PTA中的路径的等价性。 数，它为每个位置指定一个不变式；pob:L×Act→
（ｍｏｄｅｌ ｃｈｅｃｋｉｎｇ）以其简洁明了和自动化程度高而 引人注目［１］ 。 模型检测作为形式化验证的一种主 流技术，它可以克服传统软件测试用例生成不完备 的不足，同时具有验证自动化的优点，并且当验证 的性质不满足时，能给出违背性质的反例。 模型检 测采用了严格的形式化方法对系统进行验证，因此 比测试和仿真更能保证系统的正确性。 模型检测 中常使用数学抽象模型对系统进行建模，概率时间 自动机（ｐｒｏｂａｂｉｌｉｓｔｉｃ ｔｉｍｅｄ ａｕｔｏｍａｔａ， ＰＴＡ）就是其中 的一种［２－３］ ，由于它能同时表示概率性、不确定性和 实时性，因此是模型检测实时并发系统的有效工具。 模型检测通过对状态空间的穷举搜索来判定 系统是否具有所关心的性质 ϕ，但是随着实时并发 系统越来越多地应用在一些对安全性、可靠性要求 非常高的领域，如航空系统、电力系统、智能交通系 统等，系统一旦发生故障所带来的后果不堪设想， 因此设计者需要确切知道在什么情况下系统会出 现最坏或者最好的结果，这时候就需要通过模型检 测技术找到满足特定性质 ϕ 的某个策略或者最佳 策略。 目前模型检测主要用时序逻辑来刻画所关心 模型的性质，常用的逻辑包括线性时态逻辑 ＬＴＬ （ ｌｉｎｅａｒ ｔｅｍｐｏｒａｌ ｌｏｇｉｃ ）、 概 率 计 算 树 逻 辑 ＰＣＴＬ （ｐｒｏｂａｂｉｌｉｓｔｉｃ ｃｏｍｐｕｔａｔｉｏｎ ｔｒｅｅ ｌｏｇｉｃ）、概率时间计算 树逻辑 ＰＴＣＴＬ （ ｐｒｏｂａｂｉｌｉｓｔｉｃ ｔｉｍｅｄ ｃｏｍｐｕｔａｔｉｏｎ ｔｒｅｅ ｌｏｇｉｃ）、 交 替 时 间 时 态 逻 辑 ＡＴＬ （ ａｌｔｅｒｎａｔｉｎｇ⁃ｔｉｍｅ ｔｅｍｐｏｒａｌ ｌｏｇｉｃ）等，当系统中存在多个 ａｇｅｎｔ 时，ＬＴＬ、 ＰＣＴＬ、ＰＴＣＴＬ 等不能够明确描述每个 ａｇｅｎｔ 对象所 使用的策略［４－６］ ，而 ＡＴＬ 又不能够描述并发系统中 的非零和逻辑［７－８］ ，于是 Ｈｅｎｚｉｎｇｅｒ 等提出了策略逻 辑（ｓｔｒａｔｅｇｙ ｌｏｇｉｃ，ＳＬ） ［９］ ，但是 ＳＬ 中缺少对不确定性 以及时间的逻辑，因此本文提出概率时间策略逻辑 （ｐｒｏｂａｂｉｌｉｓｔｉｃ ｔｉｍｅｄ ｓｔｒａｔｅｇｙ ｌｏｇｉｃ，ＰＴＳＬ），把策略作 为第一实体对象，能够针对每个模型所使用的策略 进行描述，从而使我们能够以简单而自然的方式指 定博弈系统中的非零和逻辑属性。 本文的目的是在概率时间并发博弈结构模型 基础上，为 ＰＴＳＬ 逻辑语言提供验证方法。 本文的 主要贡献如下： １）在并发博弈结构基础上提出了概率时间并 发博弈结构模型； ２）提出的 ＰＴＳＬ 逻辑语言，它将策略和时态与 概率度量相结合； ３）提出基于区域图的 ＰＴＳＬ 模型检测算法，并 证明了区域图中的路径与 ＰＴＡ 中的路径的等价性。 １ 相关工作 对实时并发系统的模型检测可以分为 ２ 类：对 并发模型的研究；对并发模型中使用的逻辑语言的 研究。 在实时并发系统中，通常使用一些控制策 略，该策略模型与系统并发模型交互作用，因此完 全可以把实时并发模型看成对博弈模型的扩展。 而目前博弈模型通常分为两种类型：一种是轮流 （ｔｕｒｎ⁃ｂａｓｅｄ）博弈模型［１０］ ，在整个系统中，可以存在 多个玩家，但是在每个状态只能有一个玩家做出选 择，从而系统转换到下一个状态；还有一种是并发 （ｃｏｎｃｕｒｒｅｎｔ）博弈模型［１１］ ，同样在整个系统中，可以 存在多个玩家，但是在每个状态多个玩家可以同时 且独立地做出选择。 Ａｌｆａｒｏ 等［１２］ 提出了时间博弈 自动机，每个游戏者不仅可以选择可能的转换，同 时还可以选择转换发生前的等待时间。 Ｔｈｏｍａｓ Ｂｒｉｈａｙｅ 等［１３］提出了时间并发博弈结构 ＴＣＧＳ，并使 用新的逻辑语言 ＴＡＬＴＬ 进行验证。 目前在并发模 型中使用的逻辑语言的研究更丰富多彩。 ＡＴＬ 是 博弈模型中的一种典型，用来描述零和逻辑的语 言［１４］ 。 Ｔａｏｌｕｅ Ｃｈｅｎ 等［１５］ 在 ＡＴＬ 基础上添加了概 率算子，提出了 ＰＡＴＬ 逻辑语言，Ｈｅｎｚｉｎｇｅｒ 等提出 了以策略为第一对象的非零和逻辑语言 ＳＬ 并给出 了模型检测算法，Ｃｈｒｉｓｔｅｌ Ｂａｉｅｒ 等［１６］也在 ＡＴＬ 基础 上提出了一种新的逻辑语言 Ｓｔｏｃｈａｓｔｉｃ Ｇａｍｅ Ｌｏｇｉｃ。 ２ 概率时间自动机与概率时间并发 博弈结构 ２．１ 时钟与概率时间自动机 时钟 ｘ 表示记录时间的非负实数变量，设 Ｘ ＝ ｛ｘ１ ，ｘ２ ，…，ｘｎ ｝是有限的时钟变量集合，则时钟赋值 函数 ｕ：Ｘ→Ｒ≥０表示对所有 ｘｉ∈Ｘ 分配一个非负实 数。 设 ｔ ≥ ０，ｕ ＋ ｔ 表示对所有 ｘｉ∈Ｘ 增加 ｔ，即 ｕ＋ ｔ（ｘ）＝ ｕ（ｘ）＋ｔ，其中 ｘ∈Ｘ。 通常使用 ０ － 表示对 Ｘ 中 的所有时钟赋值 ０。 时钟约束是一组有关时间变量 的原子公式的合取，记为 Ｃ（ χ），语法定义为 Ｚ∷ ＝ ｘ～ ｄ ｘ－ｙ～ ｄ Ｚ∧Ｚ ｔｒｕｅ，其中 ｘ，ｙ∈Ｘ，ｄ∈Ｎ， ～ ∈ ｛＜，≤｝。 当时钟赋值 ｖ 满足时钟约束 χ 时，记为 υ ⊨ｘ。 所有满足时钟约束的时钟赋值构成的集合称 为时区（ｚｏｎｅ）。 定义 １ 概率时间自动机（ ｐｒｏｂａｂｉｌｉｓｔｉｃ ｔｉｍｅｄ ａｕｔｏｍａｔａ， ＰＴＡ）。 ＰＴＡ 是一个八元组 P ＝ （ Ｌ， ｌ ０ ， Ａｃｔ，χ，ｐｒｏｂ，ｉｎｖ，ｅｎａｂ，Ｌ）， 其中 Ｌ 表示自动机的位 置集合；初始位置 ｌ ０∈Ｓ；Ａｃｔ 表示有限的动作集合； χ 表示P中使用的时钟集合；ｉｎｖ：Ｌ→Ｃ（ χ）是环境函 数，它为每个位置指定一个不变式；ｐｒｏｂ：Ｌ ×Ａｃｔ→ 第 ５ 期 王晓燕，等：实时并发系统的 ＰＴＳＬ 模型检测 ·６９５·
·696· 智能系统学报 第12卷 Dist(2×L)表示概率转移函数，Dist(L)表示状态L agent的集合，M是系统中所有agent可能的动作集 上的条件转移的概率，且L上的所有条件转移的概 合，而T定义了每个agent的动作，Edg:QxM→r表 率和为1，即∑19()=1,0：L→[0,1：enab:L× 示状态转换表，它包含所有agent的每个状态的状 Act→C(X)表示动作使能条件；标签函数：L→ 态转移函数。本文使用Edg(q,ma,m,…,mu)表 2表示每个位置上的原子命题。 示状态q上的所有agent的动作。 PTA中的符号状态定义为二元组(l,),其中1 从上面的定义可以看出，在CGS中，由状态q: 是符号状态的位置信息，)是时钟赋值且)尸 转换成状态qt!是由所有的agent共同作用的结果， iv(l)。因此在符号状态(l,n)上，要么有一定的时 这也就是说，每个agent a:∈Agt都会根据当前的状 间流逝，要么某个动作m∈Act被执行，即 态q:选择一个动作m∈Mv(q:,a),因此状态q:转 1)时间迁移：（化，）4（化'，），当且仅当1= 换成状态q+1需使用Edg(q:,a1,a2,…,a:)表示。 在CGS模型中缺少时钟概念，因此本文对CGS 1',7'=n+d,并且n=inv(l)。 模型进行扩展，在模型中添加时钟，其定义如下 2)位置迁移：(L,n)"一('，7)，当且仅当 所示。 =enab(l,m)并且 定义4概率时间并发博弈结构(probabilistic u(,)=∑{prob(,n)(X,')lX∈2A timed concurrent game structure,PTCGS).PTCGS 7'=n[X:=0]} 是一个十元组T=(Q,Qo,,X,Inv,r,Agt,M,T, (X,')∈2×L表示支持动作m转换的一条边， Edg),其中(Q,Qo,∑，X,Inv,r)就是PTA,而Agt、 在位置(l,)上，所有的转换边记为(e1,e2,…,em〉。 M、T、Edg的含义与CGS中一样。 从位置迁移的定义可以看出，一旦一个动作m被选 因此在PTCGS系统中，每个agent都可以使用 择，则时钟会重置并随机选择后继位置。 -个PTA来表示，整个PTCGS系统就是多个PTA 定义2PTA组合(PTA composition)。两个 的集合。 PTA(P和P2)的组合定义为：P,‖P2=(L1×L2, 定义5路径(path)。PTCGS的一条路径p是 (7,72)Act UAct2,X UX2,prob,inv,enab,, 一条有限或者无限序列：p=(g,)6心(g, 中对于位置(l1,l2)∈L,×L2及动作m∈Act,U Act,: ,)4…。本文使用p,)表示路径中的 inv(,)=inv (A inv2() 第k+1个状态。而m(p,k)表示路径中的第k+1 enab((11,12),m)= 个动作，last(p)表示最后一个状态。 (enab(l,m)A enab2(12,m),m E Act U Act2 定义6路径持续时间(duration of a path)。 enab(,m),m E Act Actz 给定PTA模型P吸其路径如，则D.()=名，表示路 enab,(L,m),m E Act,Act 径ω上的节点i发生位置迁移时流逝的时间和，当 prob((,1),m)= i=0时，D(0)=0。 prob,(L1,m)☒prob2(l2,m),m∈Act1UAct2 定义7策略与联合策略(strategy and coalition prob(L1,m)☒u(.,m∈Act,\Act strategy)。策略通常表示系统中的agent在不确定 u(.)☒prob2(l2,m),m∈Act2lAct 性环境下如何在每个状态选择动作，从而找到满足 (l1,l2)=岁U写 某个性质的解决方案。agent a:的策略σ：是一个偏 2.2概率时间并发博弈结构 序函数，它将有限的路径映射到概率分布函数，即 由于可以把实时并发模型看成对博弈模型的 :p→(M),且满足当m∈M(last(p)时， 扩展，本文首先给出由Henzinger等提出的并发博弈 o(p)(m)>0。联合策略gA是指包含多个agent的 CGS模型的定义，如下所示。 策略集合。如果o,中包含所有的agent的策略，即 定义3并发博弈结构(concurrent game A=Agt,则称其为完全联合策略，否则为不完全联合 structure,CGS)。CGS是一个8元组G=(Q,Q。,∑， 策略。 T,Agt,M,T,Edg),其中Q是CGS的有限状态集 合，Q。是初始状态，∑表示输入与输出动作集合， 3概率时间策略逻辑语言 r:Q×M→u(M)是概率转换函数，其中u(M)是 为了描述博弈系统的非零和逻辑，Chatterjee和 概率分布函数，Agt={a1,a2,…,a}是系统中k个 Henzinger提出了策略逻辑(stragegy logic,SL),该
Ｄｉｓｔ（２ χ ×Ｌ）表示概率转移函数，Ｄｉｓｔ（ Ｌ）表示状态 Ｌ 上的条件转移的概率，且 Ｌ 上的所有条件转移的概 率和为 １，即 ∑ｌ∈Ｌ θ（ｌ） ＝ １，θ：Ｌ → ［０，１］；ｅｎａｂ：Ｌ × Ａｃｔ → Ｃ（χ） 表示动作使能条件；标签函数 Ｌ：Ｌ → ２ ＡＰ 表示每个位置上的原子命题。 ＰＴＡ 中的符号状态定义为二元组（ ｌ，ｖ），其中 ｌ 是符号 状 态 的 位 置 信 息， η 是 时 钟 赋 值 且 η ⊨ ｉｎｖ（ｌ）。 因此在符号状态（ｌ，η）上，要么有一定的时 间流逝，要么某个动作 ｍ∈Ａｃｔ 被执行，即 １）时间迁移： （ｌ，η） ｄ→ （ｌ′，η′），当且仅当 ｌ ＝ ｌ′，η′ ＝ η ＋ ｄ，并且 η′⊨ｉｎｖ（ｌ）。 ２） 位置迁移： （ｌ，η） ｍ→ （ｌ′，η′）， 当且仅当 η⊨ｅｎａｂ（ｌ，ｍ） 并且 μ（ｌ′，η′） ＝ ∑｛ ｐｒｏｂ（ｌ，η）（Ｘ，ｌ′） Ｘ ∈ ２ χ ∧ η′ ＝ η［Ｘ ∶ ＝ ０］ ｝ （Ｘ，ｌ′）∈２ χ ×Ｌ 表示支持动作 ｍ 转换的一条边， 在位置（ｌ，η）上，所有的转换边记为〈ｅ１ ，ｅ２ ，…，ｅｍ 〉。 从位置迁移的定义可以看出，一旦一个动作 ｍ 被选 择，则时钟会重置并随机选择后继位置。 定义 ２ ＰＴＡ 组合（ ＰＴＡ ｃｏｍｐｏｓｉｔｉｏｎ）。 两个 ＰＴＡ（ P１和 P２ ） 的组合定义为： P１‖ P２ ＝ （ Ｌ１ × Ｌ２ ， （ｌ － １ ，ｌ － ２ ），Ａｃｔ １∪Ａｃｔ ２ ， χ １∪χ ２ ，ｐｒｏｂ，ｉｎｖ，ｅｎａｂ，Ｌ），其 中对于位置 （ｌ １ ，ｌ ２ ） ∈ Ｌ１ × Ｌ２ 及动作 ｍ ∈ Ａｃｔ １ ∪ Ａｃｔ ２ ： ｉｎｖ（ｌ １ ，ｌ ２ ） ＝ ｉｎｖ１（ｌ １ ） ∧ ｉｎｖ２（ｌ ２ ） ｅｎａｂ（（ｌ １ ，ｌ ２ ），ｍ） ＝ ｅｎａｂ１（ｌ １ ，ｍ） ∧ ｅｎａｂ２（ｌ ２ ，ｍ），ｍ ∈ Ａｃｔ １ ∪ Ａｃｔ ２ ｅｎａｂ１（ｌ １ ，ｍ），ｍ ∈ Ａｃｔ １ ＼ Ａｃｔ ２ ｅｎａｂ２（ｌ ２ ，ｍ），ｍ ∈ Ａｃｔ ２ ＼ Ａｃｔ １ ì î í ï ï ïï ｐｒｏｂ（（ｌ １ ，ｌ ２ ），ｍ） ＝ ｐｒｏｂ１（ｌ １ ，ｍ） ｐｒｏｂ２（ｌ ２ ，ｍ），ｍ ∈ Ａｃｔ １ ∪ Ａｃｔ ２ ｐｒｏｂ１（ｌ １ ，ｍ） μ（ϕ，ｌ２ ） ，ｍ ∈ Ａｃｔ １ ＼ Ａｃｔ ２ μ（ϕ，ｌ１ ） ｐｒｏｂ２（ｌ ２ ，ｍ），ｍ ∈ Ａｃｔ ２ ＼ Ａｃｔ １ ì î í ï ï ï ï Ｌ（ｌ １ ，ｌ ２ ） ＝ Ｌ１ ∪ Ｌ２ ２．２ 概率时间并发博弈结构 由于可以把实时并发模型看成对博弈模型的 扩展，本文首先给出由 Ｈｅｎｚｉｎｇｅｒ 等提出的并发博弈 ＣＧＳ 模型的定义，如下所示。 定 义 ３ 并 发 博 弈 结 构 （ ｃｏｎｃｕｒｒｅｎｔ ｇａｍｅ ｓｔｒｕｃｔｕｒｅ，ＣＧＳ）。 ＣＧＳ 是一个 ８ 元组 G＝ （Ｑ，Ｑ０ ，Σ， τ，Ａｇｔ，Μ，Γ，Ｅｄｇ），其中 Ｑ 是 ＣＧＳ 的有限状态集 合，Ｑ０ 是初始状态， Σ 表示输入与输出动作集合， τ：Ｑ × Ｍ → μ（Ｍ） 是概率转换函数，其中 μ（Ｍ） 是 概率分布函数， Ａｇｔ ＝ ｛ａ１ ，ａ２ ，…，ａｋ｝ 是系统中 ｋ 个 ａｇｅｎｔ 的集合，Ｍ 是系统中所有 ａｇｅｎｔ 可能的动作集 合，而 Γ 定义了每个 ａｇｅｎｔ 的动作，Ｅｄｇ：Ｑ×Ｍ ｋ→τ 表 示状态转换表，它包含所有 ａｇｅｎｔ 的每个状态的状 态转移函数。 本文使用 Ｅｄｇ（ｑ，ｍａ１ ，ｍａ２ ，…，ｍａｋ ） 表 示状态 ｑ 上的所有 ａｇｅｎｔ 的动作。 从上面的定义可以看出，在 ＣＧＳ 中，由状态 ｑｉ 转换成状态 ｑｉ＋１ 是由所有的 ａｇｅｎｔ 共同作用的结果， 这也就是说，每个 ａｇｅｎｔ ａｊ ∈ Ａｇｔ 都会根据当前的状 态 ｑｉ 选择一个动作 ｍｊ ∈ Ｍｖ（ｑｉ，ａｊ），因此状态 ｑｉ 转 换成状态 ｑｉ＋１ 需使用 Ｅｄｇ（ｑｉ，ａ１ ，ａ２ ，…，ａｋ） 表示。 在 ＣＧＳ 模型中缺少时钟概念，因此本文对 ＣＧＳ 模型进行扩展， 在模型中添加时钟， 其定义如下 所示。 定义 ４ 概率时间并发博弈结构（ｐｒｏｂａｂｉｌｉｓｔｉｃ ｔｉｍｅｄ ｃｏｎｃｕｒｒｅｎｔ ｇａｍｅ ｓｔｒｕｃｔｕｒｅ，ＰＴＣＧＳ）。 ＰＴＣＧＳ 是一个十元组 T＝ （Ｑ，Ｑ０ ，Σ， χ，Ｉｎｖ，τ，Ａｇｔ，Μ，Γ， Ｅｄｇ），其中（Ｑ，Ｑ０ ，Σ， χ，Ｉｎｖ，τ） 就是 ＰＴＡ，而 Ａｇｔ、 Μ、Γ、Ｅｄｇ 的含义与 ＣＧＳ 中一样。 因此在 ＰＴＣＧＳ 系统中，每个 ａｇｅｎｔ 都可以使用 一个 ＰＴＡ 来表示，整个 ＰＴＣＧＳ 系统就是多个 ＰＴＡ 的集合。 定义５ 路径（ｐａｔｈ）。 ＰＴＣＧＳ 的一条路径ρ 是 一条有限或者无限序列：ρ ＝ （ｑ０ ，η０ ） ｔ ０ ，ｍ０ ，ｐ０→ （ｑ１ ， η１ ） ｔ １ ，ｍ１ ，ｐ１→ …。 本文使用 ｓ（ρ，ｋ） 表示路径中的 第 ｋ ＋ １ 个状态。 而 ｍ（ρ，ｋ） 表示路径中的第 ｋ ＋ １ 个动作，ｌａｓｔ（ρ） 表示最后一个状态。 定义 ６ 路径持续时间（ｄｕｒａｔｉｏｎ ｏｆ ａ ｐａｔｈ）。 给定 ＰＴＡ 模型P及其路径 ω，则 Ｄω（ｉ）＝ ∑ ｉ－１ ｊ ＝ ０ ｔ ｊ 表示路 径 ω 上的节点 ｉ 发生位置迁移时流逝的时间和，当 ｉ ＝０ 时，Ｄω（０） ＝ ０。 定义 ７ 策略与联合策略（ｓｔｒａｔｅｇｙ ａｎｄ ｃｏａｌｉｔｉｏｎ ｓｔｒａｔｅｇｙ）。 策略通常表示系统中的 ａｇｅｎｔ 在不确定 性环境下如何在每个状态选择动作，从而找到满足 某个性质的解决方案。 ａｇｅｎｔ ａｉ 的策略 σｉ 是一个偏 序函数，它将有限的路径映射到概率分布函数，即 σｉ：ρ → Ｄ （ Ｍ）， 且 满 足 当 ｍ ∈ Ｍ （ ｌａｓｔ （ ρ ）） 时， σ（ρ）（ｍ）＞０。 联合策略 σＡ 是指包含多个 ａｇｅｎｔ 的 策略集合。 如果 σＡ 中包含所有的 ａｇｅｎｔ 的策略，即 Ａ ＝Ａｇｔ，则称其为完全联合策略，否则为不完全联合 策略。 ３ 概率时间策略逻辑语言 为了描述博弈系统的非零和逻辑，Ｃｈａｔｔｅｒｊｅｅ 和 Ｈｅｎｚｉｎｇｅｒ 提出了策略逻辑（ ｓｔｒａｇｅｇｙ ｌｏｇｉｃ， ＳＬ），该 ·６９６· 智 能 系 统 学 报 第 １２ 卷
第5期 王晓燕，等：实时并发系统的PTSL模型检测 .697. 语言把策略作为第一实体对象，但缺少概率与时间 下列所有条件： 特性。本文在SL基础上提出概率时间策略逻辑 1)对于每一个时钟变量x,要么Lv(x)」=Lv (probabilistic timed strateg罗logic,PTSL),其语法如 (x)」，要么(x)>k并且'(x)>k; 下所示： 2)对于所有的时钟变量x和x',如果u(x)≤k p:=ppp1∧p2l 并且'(x)≤k,那么 Φ：=91U≤p2lz.Φ ①frac((x))=0当且仅当frac(v'(x))=0: A:=x(a,x)Φ|3x(a,x)Φ|A1ΛA2h ②frac(v(x))≤frac(v(x'))当且仅当 :=PA frac(v'(x))≤frac(v'(x'))。 为了更好地描述时间性质，在PTL中引入了 本文使用[]表示时钟v所属的等价类，同样可 一个新的时钟符号Z,称之为公式时钟，且X∩Z= 以将≈扩展到符号状态，使用(1，[]〉表示状态相 O,X是PTA模型中的时钟，称为系统时钟。（∈ 同，时间等价的等价类，称其为区域(region)。由于 Zuz)是一个时间区域Zone。z中表示从时钟z=0 在PTSL有公式时钟，因此在TCGS系统中使用扩展 的状态开始搜索满足中的路径，且z∈Z。Hx·p 的符号状态(l,[n,3]),而使用l,[n,S])表示扩 含义是任意策略x都满足p,而3x.φ表示存在一个 展区域。在扩展区域a中，使用zone(a)表示a中 策略x满足p,(a,x)p是策略赋值公式，表示模型a 的等价时间类。 使用策略x且满足p,~∈{，≥}，入∈[0， 在PTA模型G中存在多个状态，有的状态存在 1],k∈R,概率算子P表示满足公式p和界限符~ 后继状态，与之对应的区域也会有后继区域，而由 入的路径的概率。在本文中，我们只考虑有两个 多个区域组成的模型称为区域图。 agent的并发实时系统，因此使用x1,x2,…,表示一 定义l0后继区域(successor region)。扩展 个模型使用的策略，用y1,y2,…表示另外一个模型 区域B=〈L,[n',S]〉是=〈l,[n,3]〉的后继区 使用的不同策略。 域，当且仅当存在正数t∈R,t∈R,当l,[n'+t', 因此使用PTSL语言可以表达如下的属性，例 '+t']〉∈B,则对任意t≤t',都有(l,[n+t,3+ 如在ZeroConf协议中，发送者在发送信息后要求接 t]〉∈aUB,记为succ(a)=B。 收者要在1s内接收到消息的概率大于等于99%， 定义ll区域图(region graph)。与PTA对 P=9[x1y(s,x1)(r,y1)z.[s.l.=12U 应的区域图R是一个三元组R(P,△)=(R·, (r.l=4Λz≤1)] Steps·,L),其中R·表示扩展区域的集合，对于任 定义8扩展的时间区域。由于在PTSL中存 意扩展区域a=(l,[n,S]〉eR·转换函数Steps·包 在公式时钟变量：，因此本文将[m,S]称为扩展的 含以下3种类型的转换。 时间区域，其中η是系统时钟，3是公式时钟。从 1)时间迁移：当succ([n,S])=inv(L),则 而本文使用(l,[n,S])表示PTA中的状态，称为扩 展的符号状态。 B=(1.B=suee(a) 0.其他 4基于region graph的模型检测算法 2)位置迁移：如果存在概率p'∈prob(l)而且 [n,]满足PTA中的位置转换条件(p'),则 模型检测PT$L的问题就是，给定概率时间并发博 弈结构PTCGS T及PTSL的表达式☑，能否找到σ4使 psuceB= ∑ p'(1',X) 之满足☑。在TCGS系统中，通常使用的属性验证公式 onr(a)[XO】=2nme(B) 3)自身循环 是概率公式P△，并且在公式中通常也含有公式时钟 z,因此求解满足Pob w∈Path(l,[n,s]〉) 2月=6：9 (l,[n,3]),o=A 标签函数L·的定义如下所示： 入公式的σ4是算法的关键。 4.1基本知识 L(l,[n,S]〉=L(l)U 对于时钟变量x,用k表示时钟x的上界值。 {P:|[n,S]满足g,g∈Zxuz)(A)》 由于在验证过程中需要使用区域图上的策略，其定 对于实数t,用frac(t)表示t的小数部分，用t」表示 义如下。 t的整数部分。 定义12区域图上路径(path on the region 定义9时钟等价(clock equivalence)。两个时 钟赋值和是等价的，记为v≈'，当且仅当满足 gaph)。w°=(。，[no,o]〉o(41,[n1,31]）
语言把策略作为第一实体对象，但缺少概率与时间 特性。 本文在 ＳＬ 基础上提出概率时间策略逻辑 （ｐｒｏｂａｂｉｌｉｓｔｉｃ ｔｉｍｅｄ ｓｔｒａｔｅｇｙ ｌｏｇｉｃ，ＰＴＳＬ），其语法如 下所示： φ∷ ＝ ｐ ζ ¬ φ φ１ ∧ φ２ Φ∷ ＝ φ１ ∪≤ｋ φ２ ｚ．Φ Λ∷ ＝ ∀ｘ（ａ，ｘ）Φ ∃ｘ（ａ，ｘ）Φ Λ１ ∧ Λ２ ¬ Λ ψ∷ ＝ Ｐ ～ λΛ 为了更好地描述时间性质，在 ＰＴＳＬ 中引入了 一个新的时钟符号ℤ ，称之为公式时钟，且 χ∩ℤ ＝ ⌀， χ 是 ＰＴＡ 模型中的时钟，称为系统时钟。 ζ∈ ℤ （χ∪ℤ ）是一个时间区域 Ｚｏｎｅ。 ｚ．ϕ 表示从时钟 ｚ ＝ ０ 的状态开始搜索满足 ϕ 的路径，且 ｚ∈ℤ 。 ∀ｘ·φ 含义是任意策略 ｘ 都满足 φ，而∃ｘ．φ 表示存在一个 策略 ｘ 满足 φ，（ａ，ｘ）φ 是策略赋值公式，表示模型 ａ 使用策略 ｘ 且满足 φ， ～ ∈｛ ＜，≪，＞，≫｝，λ∈［０， １］，ｋ∈Ｒ ＋ ，概率算子 Ｐ 表示满足公式 φ 和界限符 ～ λ 的路径的概率。 在本文中，我们只考虑有两个 ａｇｅｎｔ 的并发实时系统，因此使用 ｘ１ ，ｘ２ ，…，表示一 个模型使用的策略，用 ｙ１ ，ｙ２ ，…表示另外一个模型 使用的不同策略。 因此使用 ＰＴＳＬ 语言可以表达如下的属性，例 如在 ＺｅｒｏＣｏｎｆ 协议中，发送者在发送信息后要求接 收者要在 １ｓ 内接收到消息的概率大于等于 ９９％， Ｐ≥０．９９ ［∀ｘ１∀ｙ１（ｓ，ｘ１ ）（ｒ，ｙ１ ）ｚ．［ｓ．ｌ． ＝ １２ ∪ （ｒ．ｌ ＝ ４ ∧ ｚ ≤ １）］ 定义 ８ 扩展的时间区域。 由于在 ＰＴＳＬ 中存 在公式时钟变量 ｚ，因此本文将 [η，Ｉ] 称为扩展的 时间区域，其中 η 是系统时钟，Ｉ 是公式时钟。 从 而本文使用（ｌ，［η，Ｉ］）表示 ＰＴＡ 中的状态，称为扩 展的符号状态。 ４ 基于 ｒｅｇｉｏｎ ｇｒａｐｈ 的模型检测算法 模型检测 ＰＴＳＬ 的问题就是，给定概率时间并发博 弈结构 ＰＴＣＧＳ T及 ＰＴＳＬ 的表达式⌀，能否找到 σＡ 使 之满足⌀。 在 ＴＣＧＳ 系统中，通常使用的属性验证公式 是概率公式 Ｐ～λΛ，并且在公式中通常也含有公式时钟 ｚ，因此求解满足 Ｐｒｏｂ ω ω ∈ Ｐａｔｈ〈ｌ，［η，Ｉ］〉 （ｌ，［η，Ｉ］），σＡ⊨Λ { } æ è ç ö ø ÷ ～ λ 公式的 σＡ 是算法的关键。 ４．１ 基本知识 对于时钟变量 ｘ，用 ｋｘ 表示时钟 ｘ 的上界值。 对于实数 ｔ，用 ｆｒａｃ（ｔ）表示 ｔ 的小数部分，用⌊ｔ」表示 ｔ 的整数部分。 定义 ９ 时钟等价（ｃｌｏｃｋ ｅｑｕｉｖａｌｅｎｃｅ）。 两个时 钟赋值 ｖ 和 ｖ′是等价的，记为 ｖ≈ｖ′，当且仅当满足 下列所有条件： １）对于每一个时钟变量 ｘ，要么⌊ ｖ（ ｘ）」 ＝ ⌊ ｖ′ （ｘ）」，要么 ｖ（ｘ）＞ｋｘ 并且 ｖ′（ｘ）＞ｋｘ； ２）对于所有的时钟变量 ｘ 和 ｘ′，如果 ｖ（ｘ）≤ｋｘ 并且 ｖ′（ｘ）≤ｋｘ，那么 ①ｆｒａｃ（ｖ（ｘ））＝ ０ 当且仅当 ｆｒａｃ（ｖ′（ｘ））＝ ０； ② ｆｒａｃ （ ｖ （ ｘ ）） ≤ ｆｒａｃ （ ｖ （ ｘ′）） 当 且 仅 当 ｆｒａｃ（ｖ′（ｘ））≤ｆｒａｃ（ｖ′（ｘ′））。 本文使用 [ｖ] 表示时钟 ｖ 所属的等价类，同样可 以将≈扩展到符号状态，使用〈 ｌ，［ ｖ］〉 表示状态相 同，时间等价的等价类，称其为区域（ ｒｅｇｉｏｎ）。 由于 在 ＰＴＳＬ 有公式时钟，因此在 ＴＣＧＳ 系统中使用扩展 的符号状态（ｌ，［η，Ｉ］），而使用〈ｌ，［η，Ｉ］〉 表示扩 展区域。 在扩展区域 α 中，使用 ｚｏｎｅ（α） 表示 α 中 的等价时间类。 在 ＰＴＡ 模型 Ｇ 中存在多个状态，有的状态存在 后继状态，与之对应的区域也会有后继区域，而由 多个区域组成的模型称为区域图。 定义 １０ 后继区域（ｓｕｃｃｅｓｓｏｒ ｒｅｇｉｏｎ）。 扩展 区域 β ＝ 〈ｌ，［η′，Ｉ′］〉 是 α ＝ 〈ｌ，［η，Ｉ］〉 的后继区 域，当且仅当存在正数 ｔ ∈ R，ｔ′ ∈ R，当〈ｌ，［η′ ＋ ｔ′， Ｉ′ ＋ ｔ′］〉 ∈ β，则对任意 ｔ ≤ ｔ′，都有〈ｌ，［η ＋ ｔ，Ｉ ＋ ｔ］〉 ∈ α ∪ β，记为 ｓｕｃｃ（α） ＝ β。 定义 １１ 区域图（ｒｅｇｉｏｎ ｇｒａｐｈ）。 与 ＰＴＡ P对 应的区 域 图 R是 一 个 三 元 组 R （ P，Λ） ＝ （Ｒ ∗ ， Ｓｔｅｐｓ ∗ ，Ｌ ∗ ），其中 Ｒ ∗ 表示扩展区域的集合，对于任 意扩展区域 α＝ 〈ｌ，［η，Ｉ］〉∈Ｒ ∗转换函数 Ｓｔｅｐｓ ∗ 包 含以下 ３ 种类型的转换。 １）时间迁移：当 ｓｕｃｃ（［η，Ｉ］）⊨ｉｎｖ（ｌ），则 ｐ α ｓｕｃｃβ ＝ １， β ＝ ｓｕｃｃ（α） {０， 其他 ２）位置迁移：如果存在概率 ｐ′∈ｐｒｏｂ（ ｌ） 而且 ［η，Ｉ］满足 ＰＴＡ 中的位置转换条件 τｌ（ｐ′），则 ｐ α ｓｕｃｃβ ＝ ∑Ｘ⊆χ ｚｏｎｅ（α）［Ｘ０ ］ ＝ ｚｏｎｅ（β） ｐ′（ｌ′，Ｘ） ３）自身循环 ｐ α ｓｕｃｃβ ＝ １， β ＝ α {０， 其他 标签函数 Ｌ ∗的定义如下所示： Ｌ ∗ 〈ｌ，［η，Ｉ］〉 ＝ Ｌ（ｌ） ∪ ｐ{ ζ ［η，Ｉ］ 满足 ζ，ζ ∈ Ｚ（χ∪ℤ ）（Λ）} 由于在验证过程中需要使用区域图上的策略，其定 义如下。 定义 １２ 区域图上路径 （ ｐａｔｈ ｏｎ ｔｈｅ ｒｅｇｉｏｎ ｇｒａｐｈ）。 ω ∗ ＝ 〈 ｌ ０ ， ［ η０ ， Ｉ０ ］〉 ｐ０→ 〈 ｌ １ ， ［ η１ ， Ｉ１ ］〉 第 ５ 期 王晓燕，等：实时并发系统的 ＰＴＳＬ 模型检测 ·６９７·
698· 智能系统学报 第12卷 L(2,[n2,32]）2…,其中p:∈teps(, 子命题，而内部节点标识PTSL中的操作符标识包 括∧，，U,P等，PTSL的验证算法如下所示。 [m,5]〉，且p>0。 定义l3区域图上的策略(adversary)。在区 算法1PTSL验证算法 foreach o'in sub()do 域图中的策略σR将有限路径ω·映射到概率p且 pESteps(last(w·))。 case '=p:[o']:=(1,[n,3])lELE(p) 下面介绍在区域图上的PTSL满足关系。 case p'=0:[p]:={(l,[n,S])l(l,[n,3]) 定义14PTSL的满足关系。给定区域图R case'=61A02:[p']:={(l,[7,S])l(l,[n, (P,A)以及PTSL公式中，则PTSL在R上的满足关 5])=0,n(l,[n,])=02} 系定义如下： case '=[']:=1(1,[n,])1ELAEp, (l,[n,3])true,对于所有l,n,3均成立 case o'=z.0: (I,[n,3])Epep L'(I,n,]) [p']:={(l,[m,[z:=0]])|(l,[7,5])=则 (l,[n,S])=中1∧中2台 case =0U0:Until(0,02,k) (l,[n,s])=中，and(l,[n,3])=中2 case o'=P.,YxYy(a,x)(b,y)0:[o']:=P 0 case o'=PVx3y(a,x)(b,y)0:[o']:=P20 (l,[n,])=中台(l,[n,S])=中 (L,[7,S])=A1AA2曰 case o'=P3x3y(a,x)(b,y)0:[o']:=P:0 (1,[n,])=A:and(1,[n,])A2 PTSL与PCTL的不同之处在于存在以下几个 (l,[n,S])=△台(l,[7,S])=A (l,[7,S])片中U中2台存在整数i,及路径w·,且 操作：时钟重置z.中、任意Vx(a,x)·④以及存在 w'(i)=中，且对于任意i≤≤i+k,都有w“()=中2。 3x(a,x)·④，因此对于PTsL中其他的操作符，例 如，，∧，V,U等，都可以采用PCTL中原有的算 以上定义的满足关系与PCTL的满足关系的定 义基本相同，而PTSL中独有的3个操作符一时 法，这里不作详细介绍。是公式时钟，P:的定义在 钟重置z、任意算子H以及存在算子3满足关系定 区域图中已经给出，表示满足时间赋值的命题。依 义如下。 据PCTL语义，PA的计算方法如下所示： (l,[n,5])=z.台 p.=PmmA,E, (l,[n,5[z:=0])=o4中 PnA,~∈{>，≥} (l,[n,S])=Vx(a,x)Φ曰Hx∈o and a∈ 从定义可以看出，求解P-A的值的问题其实 A,(l,[n,5])=Φ 是求解极值的问题。依据这个思路，我们来叙述式 (l,[n,])=3x(a,x)Φ3x∈o and a∈ (1)~(3)的计算过程。 A,(l,[n,5])=Φ 为了叙述的方便，下面将~入直接定义为≥入。 将带有概率算子公式PaA展开，可以得到公式 从PTSL的满足关系可知，式(1)的含义是，无论 (1)、(2)、(3): agent a和agent b使用任何策略，所找到的路径的目 (1,[n,])=P=VxVy(a,x)(b,y)(1) 标状态都满足中且概率大于等于入，因此入是agent (1.[n,3])EP=Vx3y(a,x)(b.y)(2) a和agent b使用联合策略oA=(x,y)下所得的最小 (l,[7,S])=P=a3x3y(a,x)(b,y)Φ(3) 值。从而我们可以将式(1)转换为求解最小值问 公式(1)~(3)的概率值以及σ4的求解过程是 题。式(2)中P3x3y(a,x)(b,y)④的含义是， 本文验证算法的核心。 agent a和agent b存在某个策略，所找到的路径的目 4.2验证算法 标状态满足④且概率≥入，这也就是说，找到一条满 本节将介绍基于区域图的PTSL验证算法。本 足条件的路径即可，因此可以将式(2)转换为求解 文将该算法分为3步：1)构建TCGS系统的区域图： 最大概率问题。式(3)的含义是无论agent a使用 2)在区域图上解析PTSL公式：3)在TCGS系统中 任何策略，gent b都会找到某个策略y使所找到的 找到满足公式的路径。 路径的目标状态满足Φ且概率≥入。因为a可以使 从PTA构造区域图的方法按照区域图的定义 用任意策略，所以式(3)其实是求解最小概率问题。 就可以得到，本文不再给出转换算法。本文重点介 以上将式(1)~(3)求解概率≥入的情形进行了分 绍在区域图上解析PTSL公式的过程，首先仍旧是 析，而≤入恰好是相反的情形，在这里不再赘述。有 构建PTL的语法树。在语法树上，叶节点代表原 关在区域图中寻找概率最优解的方法与在MDP中
ｐ１→〈 ｌ ２ ， ［ η２ ， Ｉ２ ］〉 ｐ２→…，其中 ｐｉ ∈ Ｓｔｅｐ ｓ ∗ 〈 ｌ ｉ， ［ηｉ，Ｉｉ］〉，且 ｐｉ＞０。 定义 １３ 区域图上的策略（ ａｄｖｅｒｓａｒｙ）。 在区 域图中的策略 σＲ 将有限路径 ω ∗ 映射到概率 ｐ 且 ｐ∈Ｓｔｅｐｓ ∗ （ｌａｓｔ（ω ∗ ））。 下面介绍在区域图上的 ＰＴＳＬ 满足关系。 定义 １４ ＰＴＳＬ 的满足关系。 给定区域图 R （ P，Λ）以及 ＰＴＳＬ 公式 ϕ，则 ＰＴＳＬ 在R上的满足关 系定义如下： （ｌ，［η，Ｉ］）⊨ｔｒｕｅ，对于所有 ｌ，η，Ｉ 均成立 （ｌ，［η，Ｉ］）⊨ｐ⇔ｐ ∈ Ｌ ∗ （ｌ，［η，Ｉ］） （ｌ，［η，Ｉ］）⊨ϕ１ ∧ ϕ２⇔ （ｌ，［η，Ｉ］）⊨ϕ１ ａｎｄ（ｌ，［η，Ｉ］）⊨ϕ２ （ｌ，［η，Ｉ］）⊨¬ ϕ⇔（ｌ，［η，Ｉ］）⊨ϕ （ｌ，［η，Ｉ］）⊨Λ１ ∧ Λ２⇔ （ｌ，［η，Ｉ］）⊨ Λ１ ａｎｄ（ｌ，［η，Ｉ］）⊨ Λ２ （ｌ，［η，Ｉ］）⊨¬ Λ⇔（ｌ，［η，Ｉ］）⊨Λ （ｌ，［η，Ｉ］）⊨ϕ１∪≤ｋϕ２⇔存在整数 ｉ，ｊ 及路径 ω ∗ ，且 ω ∗ （ｉ）⊨ϕ１ ，且对于任意 ｉ≤ｊ≤ｉ＋ｋ，都有 ω ∗ （ｊ）⊨ϕ２ 。 以上定义的满足关系与 ＰＣＴＬ 的满足关系的定 义基本相同，而 ＰＴＳＬ 中独有的 ３ 个操作符———时 钟重置 ｚ、任意算子∀以及存在算子∃满足关系定 义如下。 （ｌ，［η，Ｉ］）⊨ｚ．ϕ⇔ （ｌ，［η，Ｉ［ｚ： ＝ ０］］）⊨σＡϕ （ｌ，［η，Ｉ］）⊨∀ｘ（ａ，ｘ）Φ⇔∀ｘ ∈ σ ａｎｄ ａ ∈ Ａ，（ｌ，［η，Ｉ］）⊨Φ （ｌ，［η，Ｉ］）⊨∃ｘ（ａ，ｘ）Φ⇔∃ｘ ∈ σ ａｎｄ ａ ∈ Ａ，（ｌ，［η，Ｉ］）⊨Φ 将带有概率算子公式 Ｐ～ λ Λ 展开，可以得到公式 （１）、（２）、（３）： （ｌ，［η，Ｉ］）⊨Ｐ≥λ∀ｘ∀ｙ（ａ，ｘ）（ｂ，ｙ）Φ （１） （ｌ，［η，Ｉ］）⊨Ｐ≥λ∀ｘ∃ｙ（ａ，ｘ）（ｂ，ｙ）Φ （２） （ｌ，［η，Ｉ］）⊨Ｐ≥λ∃ｘ∃ｙ（ａ，ｘ）（ｂ，ｙ）Φ （３） 公式（１） ～ （３）的概率值以及 σＡ 的求解过程是 本文验证算法的核心。 ４．２ 验证算法 本节将介绍基于区域图的 ＰＴＳＬ 验证算法。 本 文将该算法分为 ３ 步：１）构建 ＴＣＧＳ 系统的区域图； ２）在区域图上解析 ＰＴＳＬ 公式；３） 在 ＴＣＧＳ 系统中 找到满足公式的路径。 从 ＰＴＡ 构造区域图的方法按照区域图的定义 就可以得到，本文不再给出转换算法。 本文重点介 绍在区域图上解析 ＰＴＳＬ 公式的过程，首先仍旧是 构建 ＰＴＳＬ 的语法树。 在语法树上，叶节点代表原 子命题，而内部节点标识 ＰＴＳＬ 中的操作符标识包 括∧，¬ ，∪≤ｋ ，Ｐ 等，ＰＴＳＬ 的验证算法如下所示。 算法 １ ＰＴＳＬ 验证算法 ｆｏｒｅａｃｈ φ′ ｉｎ ｓｕｂ（φ）ｄｏ ｃａｓｅ φ′＝ｐ： ［φ′］：＝｛（ｌ，［η，Ｉ］） ｌ∈Ｌ＆ｌ∈Ｌ（ｐ）｝ ｃａｓｅ φ′＝¬ θ： ［φ′］：＝｛（ｌ，［η，Ｉ］） （ｌ，［η，Ｉ］）⊨／ θ｝ ｃａｓｅφ′＝ θ１∧θ２ ：［φ′］： ＝ ｛（ ｌ，［η，Ｉ］） （ ｌ，［η， Ｉ］）⊨θ１∩（ｌ，［η，Ｉ］）⊨θ２ ｝ ｃａｓｅ φ′＝ζ： ［φ′］：＝｛（ｌ，［η，Ｉ］） ｌ∈Ｌ∧Ｉ∈ｐζ｝ ｃａｓｅ φ′＝ ｚ．θ： ［φ′］：＝ ｛（ｌ，［η，ζ［ｚ：＝ ０］］） （ｌ，［η，ζ］）⊨θ｝ ｃａｓｅ φ′ ＝ θ１ ∪≤ｋ θ２ ：Ｕｎｔｉｌ（θ１ ，θ２ ， ≤ ｋ） ｃａｓｅ φ′ ＝ Ｐ ～ λ∀ｘ∀ｙ（ａ，ｘ）（ｂ，ｙ）θ： ［φ′］： ＝ Ｐ１ θ ｃａｓｅ φ′ ＝ Ｐ ～ λ∀ｘ∃ｙ（ａ，ｘ）（ｂ，ｙ）θ：［φ′］： ＝ Ｐ２ θ ｃａｓｅ φ′ ＝ Ｐ ～ λ∃ｘ∃ｙ（ａ，ｘ）（ｂ，ｙ）θ：［φ′］： ＝ Ｐ３ θ … ＰＴＳＬ 与 ＰＣＴＬ 的不同之处在于存在以下几个 操作：时钟重置 ｚ．ϕ、任意∀ｘ（ ａ，ｘ） ·Φ 以及存在 ∃ｘ（ａ，ｘ）·Φ，因此对于 ＰＴＳＬ 中其他的操作符，例 如¬ ，∧，∨，∪≤ｋ等，都可以采用 ＰＣＴＬ 中原有的算 法，这里不作详细介绍。 ζ 是公式时钟，ｐζ 的定义在 区域图中已经给出，表示满足时间赋值的命题。 依 据 ＰＣＴＬ 语义，Ｐ～ λΛ 的计算方法如下所示： Ｐ ～ λΛ ＝ ｐｍａｘΛ， ～ ∈ ｛ ＜ ， ≤｝ ｐ{ ｍｉｎΛ， ～ ∈ ｛ ＞ ， ≥｝ 从定义可以看出，求解 Ｐ ～ λΛ 的值的问题其实 是求解极值的问题。 依据这个思路，我们来叙述式 （１） ～ （３）的计算过程。 为了叙述的方便，下面将～λ 直接定义为≥λ。 从 ＰＴＳＬ 的满足关系可知，式（ １） 的含义是，无论 ａｇｅｎｔ ａ 和 ａｇｅｎｔ ｂ 使用任何策略，所找到的路径的目 标状态都满足 Φ 且概率大于等于 λ，因此 λ 是 ａｇｅｎｔ ａ 和 ａｇｅｎｔ ｂ 使用联合策略 σＡ ＝ （ｘ，ｙ）下所得的最小 值。 从而我们可以将式（１） 转换为求解最小值问 题。 式（２）中 Ｐ≥λ∃ｘ∃ｙ（ａ，ｘ） （ｂ，ｙ） Φ 的含义是， ａｇｅｎｔ ａ 和 ａｇｅｎｔ ｂ 存在某个策略，所找到的路径的目 标状态满足 Φ 且概率≥λ，这也就是说，找到一条满 足条件的路径即可，因此可以将式（２）转换为求解 最大概率问题。 式（３） 的含义是无论 ａｇｅｎｔ ａ 使用 任何策略，ａｇｅｎｔ ｂ 都会找到某个策略 ｙ 使所找到的 路径的目标状态满足 Φ 且概率≥λ。 因为 ａ 可以使 用任意策略，所以式（３）其实是求解最小概率问题。 以上将式（１） ～ （３） 求解概率≥λ 的情形进行了分 析，而≤λ 恰好是相反的情形，在这里不再赘述。 有 关在区域图中寻找概率最优解的方法与在 ＭＤＰ 中 ·６９８· 智 能 系 统 学 报 第 １２ 卷
第5期 王晓燕，等：实时并发系统的PTSL模型检测 699. 的方法一样，可以使用value iteration的方法查找整 本文使用的模型是由Cheshire等建立的MDP模型 个模型中的概率最大最小值)。而公式时钟z值 修改而来[us),为environment模型添加了消息丢失 的计算则是将找到的满足日的路径中的各个区域的 的概率，表示网络中的其他设备在应答设备S的询 时间最大值相加起来即可。 问时，发送的信息有可能发生丢失，本文使用参数 当在区域图中找到了满足条件的路径ω·后， plost表示。则sender模型和environment模型如图 这并不是最终解，还需要在TCGS系统中构建与w· 1、2所示。 相对应的路径w,另外还需要证明ω·与ω的概率是 X=0 一样的，这样才能保证最终找到的路径ω是正 recv Coll<MAXCOLL 确的。 x:=0 (5 [Send ARP] 构建ω过程采用递归方法，算法如下所示。 [Recv] X-CONSEC& coll-=MAXCOLL Coll:=min(coll+1. probes=1 算法2构建w过程 [send_used]x [send fresh MAXCOLL))&(probes:-0) BuildPathFromRG(R,@*) X=0 Probes:=0 length:=(lw·l;i:=0:w:=☑；Trans:=☑； x-20 &Trecv] x-LONGWAIT [recv]probes= [send ARP While i<length xCONSEC& probes<1 if(i=0)&(7o,3)∈[7o,3] 图1 sender模型 w:wU(lo,no); Fig.1 sender model else [Send used if(n:,S+D(i))∈[n:,5] [Send used] [send APR] [send_APR] w:=wU(L,7:); e Trans:=TransU(),(m:P:),(,n) return (@Trans) =0 证明w”与w的概率是一样的，即Pob(w·)= 1月 Prob(w)。设在区域r:发生转换前概率为p,区域r 中包含m个时间转换，n个位置转换，k个自身循 [recv] y≥1 环。从区域图的定义可以看出，当发生时间迁移和 e 自身循环时概率均为1，且这两个迁移不会改变区 图2 environment模型 域位置，转换后的概率为p×1×1×1…=p,故而概率 Fig.2 environment model 值没有任何改变。而发生位置迁移时，ω·中的概 为了验证模型，在Pism中重新设计实现了 率为p·={p:(X,l+1)1XCX,zone(a)[X:=0]= PTSL逻辑语言，并使用PTA模型表示并发实时系 zone(B)},w中的概率为μ={∑P:(X,l1)IX∈2 统中的agent,使用PTA的组合模型表示整个 八(n:+t:)[X:=0]=7+},由于区域r中有m个 PTCGS模型。组合后的PTA模型转换成区域图后， 时间转换，因此zone(a)=[n:+dn,s+D.(i)+ 状态节点一共有631个，在本文中不能全部给出，本 dn],zone(B)=[n+1,E+D(i+1)+d+1],而(n:+ 文只给出几个关键节点的图，如图3所示。 )[X:=0]∈[n:+dn][X:=0],n+1∈[n+1],因 8 此P=uo 5实验与结果 1/3 -③ 1/3 本文以ZeroConf协议为例说明PTSL的模型检 @ ①0 测方法。ZeroConf协议是一种用于局域网内自动生 10 10 1i3 ⑤ ① 成可用P地址的网络技术。设备S连接网络后，首 N/3 先随机地选择一个P地址，然后设备S会向网络中 1/3X 6 ① 的其他设备连续K次发送“这个P地址是否已经 被占用”的询问信息，如果设备S没有收到任何应 ⑦ 答，则它会使用该P地址，否则只要收到过1个“P 图3区域图模型片段 地址被占用”的应答，设备S就会重新选择P地址。 Fig.3 Fragment of region graph model
的方法一样，可以使用 ｖａｌｕｅ ｉｔｅｒａｔｉｏｎ 的方法查找整 个模型中的概率最大最小值［１７］ 。 而公式时钟 ｚ 值 的计算则是将找到的满足 θ 的路径中的各个区域的 时间最大值相加起来即可。 当在区域图中找到了满足条件的路径 ω ∗ 后， 这并不是最终解，还需要在 ＴＣＧＳ 系统中构建与 ω ∗ 相对应的路径 ω，另外还需要证明 ω ∗与 ω 的概率是 一样的， 这样才能保证最终找到的路径 ω 是正 确的。 构建 ω 过程采用递归方法，算法如下所示。 算法 ２ 构建 ｗ 过程 ＢｕｉｌｄＰａｔｈＦｒｏｍＲＧ（ R，ω ∗ ） ｌｅｎｇｔｈ ∶ ＝ （ ｜ ω ∗ ｜ ；ｉ ∶ ＝ ０；ω ∶ ＝⌀；Ｔｒａｎｓ：＝⌀； Ｗｈｉｌｅ ｉ＜ｌｅｎｇｔｈ ｉｆ（ｉ ＝ ０） ＆（η０ ，Ｉ）∈［η０ ，Ｉ０ ］ ω：ω∪（ｌ ０ ，η０ ）； ｅｌｓｅ ｉｆ （ηｉ，Ｉ＋Ｄω（ｉ））∈［ηｉ，Ｉｉ］ ω：＝ω∪（ｌ ｉ，ηｉ）； Ｔｒａｎｓ：＝ Ｔｒａｎｓ∪｛（ｌ ｉ－１ ，ηｉ－１ ），（ｍｉ，ｐｉ），（ｌ ｉ，ηｉ）｝ ｒｅｔｕｒｎ （ω，Ｔｒａｎｓ） 证明 ω ∗ 与 ω 的概率是一样的，即Ｐｒｏｂ（ω ∗ ）＝ Ｐｒｏｂ（ω）。 设在区域 ｒｉ 发生转换前概率为 ｐ，区域 ｒｉ 中包含 ｍ 个时间转换，ｎ 个位置转换，ｋ 个自身循 环。 从区域图的定义可以看出，当发生时间迁移和 自身循环时概率均为 １，且这两个迁移不会改变区 域位置，转换后的概率为 ｐ×１×１×１… ＝ ｐ，故而概率 值没有任何改变。 而发生位置迁移时， ω ∗ 中的概 率为ｐｉ∗ ＝ ｛Σｐｉ（Ｘ，ｌ ｉ＋１ ） ｜ Ｘ ⊆χ，ｚｏｎｅ（α）［Ｘ ∶ ＝ ０］ ＝ ｚｏｎｅ（β）｝，ω 中的概率为 μ ＝ ｛Σｐｉ（Ｘ，ｌ ｉ＋１ ） ｜ Ｘ ∈ ２ χ ∧ （ηｉ ＋ ｔ ｉ）［Ｘ ∶ ＝ ０］ ＝ ηｉ＋１ ｝ ，由于区域 ｒｉ 中有 ｍ 个 时间转换，因此 ｚｏｎｅ（α） ＝ ［ηｉ ＋ ｄｍ ，ε ＋ Ｄω（ｉ） ＋ ｄｍ ］，ｚｏｎｅ（β） ＝ ［ηｉ＋１ ，ε ＋ Ｄω（ｉ ＋ １） ＋ ｄｉ＋１ ］，而（ηｉ ＋ ｔ ｉ）［Ｘ ∶ ＝ ０］ ∈［ηｉ ＋ ｄｍ ］［Ｘ ∶ ＝ ０］，ηｉ＋１ ∈［ηｉ＋１ ］，因 此 ｐ ∗ ｉ ＝ μ。 ５ 实验与结果 本文以 ＺｅｒｏＣｏｎｆ 协议为例说明 ＰＴＳＬ 的模型检 测方法。 ＺｅｒｏＣｏｎｆ 协议是一种用于局域网内自动生 成可用 ＩＰ 地址的网络技术。 设备 Ｓ 连接网络后，首 先随机地选择一个 ＩＰ 地址，然后设备 Ｓ 会向网络中 的其他设备连续 Ｋ 次发送“这个 ＩＰ 地址是否已经 被占用”的询问信息， 如果设备 Ｓ 没有收到任何应 答，则它会使用该 ＩＰ 地址，否则只要收到过 １ 个“ＩＰ 地址被占用”的应答，设备 Ｓ 就会重新选择 ＩＰ 地址。 本文使用的模型是由 Ｃｈｅｓｈｉｒｅ 等建立的 ＭＤＰ 模型 修改而来［１８］ ，为 ｅｎｖｉｒｏｎｍｅｎｔ 模型添加了消息丢失 的概率，表示网络中的其他设备在应答设备 Ｓ 的询 问时，发送的信息有可能发生丢失，本文使用参数 ｐｌｏｓｔ 表示。 则 ｓｅｎｄｅｒ 模型和 ｅｎｖｉｒｏｎｍｅｎｔ 模型如图 １、２ 所示。 图 １ ｓｅｎｄｅｒ 模型 Ｆｉｇ．１ ｓｅｎｄｅｒ ｍｏｄｅｌ 图 ２ ｅｎｖｉｒｏｎｍｅｎｔ 模型 Ｆｉｇ．２ ｅｎｖｉｒｏｎｍｅｎｔ ｍｏｄｅｌ 为了验证模型，在 Ｐｒｉｓｍ 中重新设计实现了 ＰＴＳＬ 逻辑语言，并使用 ＰＴＡ 模型表示并发实时系 统中 的 ａｇｅｎｔ， 使 用 ＰＴＡ 的 组 合 模 型 表 示 整 个 ＰＴＣＧＳ 模型。 组合后的 ＰＴＡ 模型转换成区域图后， 状态节点一共有 ６３１ 个，在本文中不能全部给出，本 文只给出几个关键节点的图，如图 ３ 所示。 图 ３ 区域图模型片段 Ｆｉｇ．３ Ｆｒａｇｍｅｎｔ ｏｆ ｒｅｇｉｏｎ ｇｒａｐｈ ｍｏｄｅｌ 第 ５ 期 王晓燕，等：实时并发系统的 ＰＴＳＬ 模型检测 ·６９９·
·700 智能系统学报 第12卷 图3中每个节点的值如下所示： 使用PT$L求解在大于等于T时间内设备仍未 l[0]=((s=0,probes=0,ip=0,coll=0,e=0), 成功分配到P的概率的属性公式为 {x=0,y=0,x=y}) Px3y(a,x)(b,y)z(！(s=6&ip=2)Az≥T) I[1]=((s=1,probes=0,ip=0,coll=0,e=0), 表2为测试时的数据取值，从结果可以看出，当 {x=0,y=0,x=y}) 时间限界T较小时（≤10），发生不能配置合适的P l[2]=(s=3,probes=0,ip=1,coll=0,e=0), 的概率大一些，而时间限界T≥20时不能成功获得 {x=0,y=20,x-y=-20}) IP地址的概率几乎为0，完全符合ZeroConf协议的 l[3]=((s=3,probes=0,ip=1,coll=0,e=0), 标准。 {x=1,y=20,x-y=-19}) 表2 ZeroConf的实验结果2 I[4]=((s=3,probes=0,ip=1,coll=0,e=0), Table 2 Result 2 of ZeroConf experiment {x=2,y=20,x-y=-18}) 发包次数丢失率 时间 概率 l[5]=((s=3,probes=0,ip=2,coll=0,e=0), N节点数 Plost T Probability {x=0,y=20,x-y=-20}) 100 0.1 10 0.0014 l[6]=(s=3,probes=0,ip=2,coll=0,e=0), {x=1,y=20,x-y=-19}) 100 0.1 20 0.00010073 l[7]=((s=3,probes=0,ip=2,coll=0,e=0), 100 0 30 0.00010063 {x=2,y=20,x-y=-18}) I[8]=((s=3,probes=1,ip=1,coll=0,e=0), 100 40 0.00010063 {x=0,y=40,x-y=-40}) 100 0.01 10 0.0014 I[9]=((s=3,probes=1,ip=1,coll=0,e=0), {x=0,y=39,x-y=-39}) 100 0.01 20 0.0000012221 l[10]=((s=3,probes=1,ip=1,coll=0,e=0), 100 0.01 30 0.0000012077 {x=0,y=38,x-y=-38}) l[11]=((s=3,probes=1,ip=2,coll=0,e=0), 100 0.01 40 0.0000012077 {x=0,y=0,x=y}) l[12]=((s=3,probes=1,ip=2,coll=0,e=1), 6 结束语 x=0,y=0,x=y) 本文在CGS模型基础上添加了概率及时间约 首先求新人网的设备可以成功分配到未使用 束，提出了一种新的并发模型PTCGS。并根据 的P的概率，使用PTSL的属性公式为 PTCGS特点，提出了新的逻辑语言PTSL,它在SL P=VxVy(a,x)(b,y)(true U(s =6&ip =2)) 逻辑的基础上添加了时间与概率特性，把策略作为 表1为测试时的数据取值，从结果可以看出，当 第一实体对象，能够针对每个模型所使用的策略进 网络中节点数N值变化较大时，最后成功获得P 行描述，从而使我们能够以简单而自然的方式指定 地址的概率不会发生很大的变化。 PTCGS系统中的非零和逻辑属性，并给出了基于区 表1 ZeroConf的实验结果1 域图的模型检测算法。最后以ZeroConf协议为例 Table 1 Result 1 of ZeroConf experiment 来说明PTSL的模型检测方法的正确性。 发包次数 丢失率 概率 N节点数 参考文献： K Plost Probability 10 0.1 0.9998 [1]CLARKE E.GRUMBERG O,PELED D.Model Checking [M].Cambridge MIT press,1999:5-60. 100 2 0.1 0.9987 [2]BEAUQUIER D.On probabilistic timed automata J]. 1000 2 0.1 0.9875 Theoretical computer science,2003,292(1):65-84. 10 2 0.01 0.9998 [3]KWIATKOWSKA M,NORMAN G,SEGALA R,et al. 50 2 0.01 0.9992 Automatic verification of real-time systems with discrete 100 probability distributions[J].Theoretical computer science, 2 0.01 0.9984 2002,282:101-150. 1000 2 0.01 0.9849 [4]CLARKE E,EMERSON A.Design and synthesis of
图 ３ 中每个节点的值如下所示： ｌ［０］ ＝ （（ｓ ＝ ０，ｐｒｏｂｅｓ ＝ ０，ｉｐ ＝ ０，ｃｏｌｌ ＝ ０，ｅ ＝ ０）， ｛ｘ ＝ ０，ｙ ＝ ０，ｘ ＝ ｙ｝） ｌ［１］ ＝ （（ｓ ＝ １，ｐｒｏｂｅｓ ＝ ０，ｉｐ ＝ ０，ｃｏｌｌ ＝ ０，ｅ ＝ ０）， ｛ｘ ＝ ０，ｙ ＝ ０，ｘ ＝ ｙ｝） ｌ［２］ ＝ （（ｓ ＝ ３，ｐｒｏｂｅｓ ＝ ０，ｉｐ ＝ １，ｃｏｌｌ ＝ ０，ｅ ＝ ０）， ｛ｘ ＝ ０，ｙ ＝ ２０，ｘ－ｙ ＝ －２０｝） ｌ［３］ ＝ （（ｓ ＝ ３，ｐｒｏｂｅｓ ＝ ０，ｉｐ ＝ １，ｃｏｌｌ ＝ ０，ｅ ＝ ０）， ｛ｘ ＝ １，ｙ ＝ ２０，ｘ－ｙ ＝ －１９｝） ｌ［４］ ＝ （（ｓ ＝ ３，ｐｒｏｂｅｓ ＝ ０，ｉｐ ＝ １，ｃｏｌｌ ＝ ０，ｅ ＝ ０）， ｛ｘ ＝ ２，ｙ ＝ ２０，ｘ－ｙ ＝ －１８｝） ｌ［５］ ＝ （（ｓ ＝ ３，ｐｒｏｂｅｓ ＝ ０，ｉｐ ＝ ２，ｃｏｌｌ ＝ ０，ｅ ＝ ０）， ｛ｘ ＝ ０，ｙ ＝ ２０，ｘ－ｙ ＝ －２０｝） ｌ［６］ ＝ （（ｓ ＝ ３，ｐｒｏｂｅｓ ＝ ０，ｉｐ ＝ ２，ｃｏｌｌ ＝ ０，ｅ ＝ ０）， ｛ｘ ＝ １，ｙ ＝ ２０，ｘ－ｙ ＝ －１９｝） ｌ［７］ ＝ （（ｓ ＝ ３，ｐｒｏｂｅｓ ＝ ０，ｉｐ ＝ ２，ｃｏｌｌ ＝ ０，ｅ ＝ ０）， ｛ｘ ＝ ２，ｙ ＝ ２０，ｘ－ｙ ＝ －１８｝） ｌ［８］ ＝ （（ｓ ＝ ３，ｐｒｏｂｅｓ ＝ １，ｉｐ ＝ １，ｃｏｌｌ ＝ ０，ｅ ＝ ０）， ｛ｘ ＝ ０，ｙ ＝ ４０，ｘ－ｙ ＝ －４０｝） ｌ［９］ ＝ （（ｓ ＝ ３，ｐｒｏｂｅｓ ＝ １，ｉｐ ＝ １，ｃｏｌｌ ＝ ０，ｅ ＝ ０）， ｛ｘ ＝ ０，ｙ ＝ ３９，ｘ－ｙ ＝ －３９｝） ｌ［１０］ ＝ （（ｓ ＝ ３，ｐｒｏｂｅｓ ＝ １，ｉｐ ＝ １，ｃｏｌｌ ＝ ０，ｅ ＝ ０）， ｛ｘ ＝ ０，ｙ ＝ ３８，ｘ－ｙ ＝ －３８｝） ｌ［１１］ ＝ （（ｓ ＝ ３，ｐｒｏｂｅｓ ＝ １，ｉｐ ＝ ２，ｃｏｌｌ ＝ ０，ｅ ＝ ０）， ｛ｘ ＝ ０，ｙ ＝ ０，ｘ ＝ ｙ｝） ｌ［１２］ ＝ （（ｓ ＝ ３，ｐｒｏｂｅｓ ＝ １，ｉｐ ＝ ２，ｃｏｌｌ ＝ ０，ｅ ＝ １）， ｛ｘ ＝ ０，ｙ ＝ ０，ｘ ＝ ｙ｝） 首先求新入网的设备可以成功分配到未使用 的 ＩＰ 的概率，使用 ＰＴＳＬ 的属性公式为 Ｐ≥λ∀ｘ∀ｙ（ａ，ｘ）（ｂ，ｙ）（ｔｒｕｅ ∪ （ｓ ＝ ６＆ｉｐ ＝ ２）） 表 １ 为测试时的数据取值，从结果可以看出，当 网络中节点数 Ｎ 值变化较大时，最后成功获得 ＩＰ 地址的概率不会发生很大的变化。 表 １ ＺｅｒｏＣｏｎｆ 的实验结果 １ Ｔａｂｌｅ １ Ｒｅｓｕｌｔ １ ｏｆ ＺｅｒｏＣｏｎｆ ｅｘｐｅｒｉｍｅｎｔ Ｎ 节点数 发包次数 Ｋ 丢失率 Ｐｌｏｓｔ 概率 Ｐｒｏｂａｂｉｌｉｔｙ １０ ２ ０．１ ０．９９９ ８ １００ ２ ０．１ ０．９９８ ７ １ ０００ ２ ０．１ ０．９８７ ５ １０ ２ ０．０１ ０．９９９ ８ ５０ ２ ０．０１ ０．９９９ ２ １００ ２ ０．０１ ０．９９８ ４ １ ０００ ２ ０．０１ ０．９８４ ９ 使用 ＰＴＳＬ 求解在大于等于 Ｔ 时间内设备仍未 成功分配到 ＩＰ 的概率的属性公式为 Ｐ≥λ∀ｘ∃ｙ（ａ，ｘ）（ｂ，ｙ）ｚ．（！ （ｓ ＝ ６＆ｉｐ ＝ ２） ∧ ｚ ≥ Ｔ） 表 ２ 为测试时的数据取值，从结果可以看出，当 时间限界 Ｔ 较小时（≤１０），发生不能配置合适的 ＩＰ 的概率大一些，而时间限界 Ｔ≥２０ 时不能成功获得 ＩＰ 地址的概率几乎为 ０，完全符合 ＺｅｒｏＣｏｎｆ 协议的 标准。 表 ２ ＺｅｒｏＣｏｎｆ 的实验结果 ２ Ｔａｂｌｅ ２ Ｒｅｓｕｌｔ ２ ｏｆ ＺｅｒｏＣｏｎｆ ｅｘｐｅｒｉｍｅｎｔ Ｎ 节点数 发包次数 Ｋ 丢失率 Ｐｌｏｓｔ 时间 Ｔ 概率 Ｐｒｏｂａｂｉｌｉｔｙ １００ ２ ０．１ １０ ０．００１ ４ １００ ２ ０．１ ２０ ０．０００ １００ ７３ １００ ２ ０．１ ３０ ０．０００ １００ ６３ １００ ２ ０．１ ４０ ０．０００ １００ ６３ １００ ２ ０．０１ １０ ０．００１ ４ １００ ２ ０．０１ ２０ ０．０００ ００１ ２２２ １ １００ ２ ０．０１ ３０ ０．０００ ００１ ２０７ ７ １００ ２ ０．０１ ４０ ０．０００ ００１ ２０７ ７ ６ 结束语 本文在 ＣＧＳ 模型基础上添加了概率及时间约 束，提 出 了 一 种 新 的 并 发 模 型 ＰＴＣＧＳ。 并 根 据 ＰＴＣＧＳ 特点，提出了新的逻辑语言 ＰＴＳＬ，它在 ＳＬ 逻辑的基础上添加了时间与概率特性，把策略作为 第一实体对象，能够针对每个模型所使用的策略进 行描述，从而使我们能够以简单而自然的方式指定 ＰＴＣＧＳ 系统中的非零和逻辑属性，并给出了基于区 域图的模型检测算法。 最后以 ＺｅｒｏＣｏｎｆ 协议为例 来说明 ＰＴＳＬ 的模型检测方法的正确性。 参考文献： ［１］ ＣＬＡＲＫＥ Ｅ， ＧＲＵＭＢＥＲＧ Ｏ， ＰＥＬＥＤ Ｄ． Ｍｏｄｅｌ Ｃｈｅｃｋｉｎｇ ［Ｍ］． Ｃａｍｂｒｉｄｇｅ ： ＭＩＴ ｐｒｅｓｓ， １９９９： ５－６０． ［２ ］ ＢＥＡＵＱＵＩＥＲ Ｄ． Ｏｎ ｐｒｏｂａｂｉｌｉｓｔｉｃ ｔｉｍｅｄ ａｕｔｏｍａｔａ ［ Ｊ ］． Ｔｈｅｏｒｅｔｉｃａｌ ｃｏｍｐｕｔｅｒ ｓｃｉｅｎｃｅ， ２００３， ２９２（１）： ６５－８４． ［３］ ＫＷＩＡＴＫＯＷＳＫＡ Ｍ， ＮＯＲＭＡＮ Ｇ， ＳＥＧＡＬＡ Ｒ， ｅｔ ａｌ． Ａｕｔｏｍａｔｉｃ ｖｅｒｉｆｉｃａｔｉｏｎ ｏｆ ｒｅａｌ⁃ｔｉｍｅ ｓｙｓｔｅｍｓ ｗｉｔｈ ｄｉｓｃｒｅｔｅ ｐｒｏｂａｂｉｌｉｔｙ ｄｉｓｔｒｉｂｕｔｉｏｎｓ［Ｊ］． Ｔｈｅｏｒｅｔｉｃａｌ ｃｏｍｐｕｔｅｒ ｓｃｉｅｎｃｅ ， ２００２， ２８２： １０１－１５０． ［４ ］ ＣＬＡＲＫＥ Ｅ， ＥＭＥＲＳＯＮ Ａ． Ｄｅｓｉｇｎ ａｎｄ ｓｙｎｔｈｅｓｉｓ ｏｆ ·７００· 智 能 系 统 学 报 第 １２ 卷
第5期 王晓燕，等：实时并发系统的PTSL模型检测 .701· synchronization skeletons using branching time temporal [15 CHEN Taolue,LU Jian.Probabilistic alternating-time logic[C]//Proceedinns of the Workshop Logic of Programs. temporal logic and model checking algorithm [C]/ Newyork,US,1981:52-71. Fourth International Conference on Fuzzy Systems and [5]HANSSON H,JONSSON B.A logic for reasoning about Knowledge Discovery (FSKD),2007.Haikou,China, time and reliability[.Formal aspects of computing, 2007:35-39. 1994,6(5):512-535. [16]CHRISTEL Baier,TOMAS Brazdil,MARCUS GroBer,et [6]ALFARO de L.Temporal Logics for the Specification of al.Stochastic game logic[C]//Conference:Quantitative Performance and Reliability C]//Proc STACS'97.New Evaluation of Systems.Edinburgh,UK,2007:227-236. York,US,1997:165-176. [17]MARTA Kwiatkowska A,GETHIN Norman A,JEREMY [7]ALUR R,HENZINGER T A,KUPFERMAN O. Sproston B,et al.Symbolic model checking for Alternating-time temporal logic[J].Journal of the ACM, probabilistic timed automata[J].Information and 2002.49:672-713. computation,2007,205(2):1027-1077. [8]CHATTERJEE K,HENZINGER T A.Strategy improvement [18]MARTA Kwiatkowska,GETHIN Norman,DAVID Parker, for stochastic Rabin and Strett Games[C]//Proc DBLP et al.Performance analysis of probabilistic timed automata 2006.Bonn,Germany,2006:375-389. using digital clocks [J].Formal methods in system [9]CHATTERJEE K,HENZINGER T A,PITERMAN N. design,2006,29(1):33-78. Strategy logic[J].Information and computation,2007,208 作者简介： (6):677-693. 王晓燕，女，1977年生，讲师，博士， [10]Basset N,Kwiatkowska M,Topcu U,et al.Strategy 主要研究方向为软件建模与验证技术、 synthesis for stochastic games with multiple long-run 软件开发新方法。申请发明专利2项， objectives[C]//International Conference on Tools and 并获得2010年中国国家专利优秀奖. Algorithms for the Construction and Analysis of Systems. 2008年吉林省科技进步一等奖，中国商 Berlin,Germany,2015:256-271. 业科技进步二等奖。发表论文20余 [11]KRISHNENDU Chatterjee,LUCA de Alfaro.THOMAS A. 篇，其中被SCI收录5篇。 et al.Strategy improvement for concurrent reachability and 韩啸，男，1981年生，编辑.博士研 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]//14 International Conference on Concurrency Theory.Marceille,France, 2003:144-158. [13]THOMAS Brihaye,FRAN Cois,LAROUSSINIE,et al. 彭君，男，1981年生，讲师，博士，主 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
ｓｙｎｃｈｒｏｎｉｚａｔｉｏｎ ｓｋｅｌｅｔｏｎｓ ｕｓｉｎｇ ｂｒａｎｃｈｉｎｇ ｔｉｍｅ ｔｅｍｐｏｒａｌ ｌｏｇｉｃ［Ｃ］ ／ ／ Ｐｒｏｃｅｅｄｉｎｎｓ ｏｆ ｔｈｅ Ｗｏｒｋｓｈｏｐ Ｌｏｇｉｃ ｏｆ Ｐｒｏｇｒａｍｓ． Ｎｅｗｙｏｒｋ， ＵＳ， １９８１： ５２－７１． ［５］ ＨＡＮＳＳＯＮ Ｈ， ＪＯＮＳＳＯＮ Ｂ． Ａ ｌｏｇｉｃ ｆｏｒ ｒｅａｓｏｎｉｎｇ ａｂｏｕｔ ｔｉｍｅ ａｎｄ ｒｅｌｉａｂｉｌｉｔｙ［Ｊ］． Ｆｏｒｍａｌ ａｓｐｅｃｔｓ ｏｆ ｃｏｍｐｕｔｉｎｇ， １９９４， ６（５）： ５１２－５３５． ［６］ ＡＬＦＡＲＯ ｄｅ Ｌ． Ｔｅｍｐｏｒａｌ Ｌｏｇｉｃｓ ｆｏｒ ｔｈｅ Ｓｐｅｃｉｆｉｃａｔｉｏｎ ｏｆ Ｐｅｒｆｏｒｍａｎｃｅ ａｎｄ Ｒｅｌｉａｂｉｌｉｔｙ ［ Ｃ］ ／ ／ Ｐｒｏｃ ＳＴＡＣＳ ’ ９７． Ｎｅｗ Ｙｏｒｋ， ＵＳ， １９９７： １６５－１７６． ［ ７ ］ ＡＬＵＲ Ｒ， ＨＥＮＺＩＮＧＥＲ Ｔ Ａ， ＫＵＰＦＥＲＭＡＮ Ｏ． Ａｌｔｅｒｎａｔｉｎｇ⁃ｔｉｍｅ ｔｅｍｐｏｒａｌ ｌｏｇｉｃ ［ Ｊ］． Ｊｏｕｒｎａｌ ｏｆ ｔｈｅ ＡＣＭ， ２００２， ４９： ６７２－７１３． ［８］ＣＨＡＴＴＥＲＪＥＥ Ｋ， ＨＥＮＺＩＮＧＥＲ Ｔ Ａ． Ｓｔｒａｔｅｇｙ ｉｍｐｒｏｖｅｍｅｎｔ ｆｏｒ ｓｔｏｃｈａｓｔｉｃ Ｒａｂｉｎ ａｎｄ Ｓｔｒｅｔｔ Ｇａｍｅｓ［Ｃ］ ／ ／ Ｐｒｏｃ ＤＢＬＰ ２００６． Ｂｏｎｎ， Ｇｅｒｍａｎｙ， ２００６： ３７５－３８９． ［９ ］ ＣＨＡＴＴＥＲＪＥＥ Ｋ， ＨＥＮＺＩＮＧＥＲ Ｔ Ａ， ＰＩＴＥＲＭＡＮ Ｎ． Ｓｔｒａｔｅｇｙ ｌｏｇｉｃ［Ｊ］． Ｉｎｆｏｒｍａｔｉｏｎ ａｎｄ ｃｏｍｐｕｔａｔｉｏｎ， ２００７， ２０８ （６）： ６７７－６９３． ［１０ ］ Ｂａｓｓｅｔ Ｎ， Ｋｗｉａｔｋｏｗｓｋａ Ｍ， Ｔｏｐｃｕ Ｕ， ｅｔ ａｌ． Ｓｔｒａｔｅｇｙ ｓｙｎｔｈｅｓｉｓ ｆｏｒ ｓｔｏｃｈａｓｔｉｃ ｇａｍｅｓ ｗｉｔｈ ｍｕｌｔｉｐｌｅ ｌｏｎｇ⁃ｒｕｎ ｏｂｊｅｃｔｉｖｅｓ ［ Ｃ］ ／ ／ Ｉｎｔｅｒｎａｔｉｏｎａｌ Ｃｏｎｆｅｒｅｎｃｅ ｏｎ Ｔｏｏｌｓ ａｎｄ Ａｌｇｏｒｉｔｈｍｓ ｆｏｒ ｔｈｅ Ｃｏｎｓｔｒｕｃｔｉｏｎ ａｎｄ Ａｎａｌｙｓｉｓ ｏｆ Ｓｙｓｔｅｍｓ． Ｂｅｒｌｉｎ， Ｇｅｒｍａｎｙ， ２０１５：２５６－２７１． ［１１］ＫＲＩＳＨＮＥＮＤＵ Ｃｈａｔｔｅｒｊｅｅ， ＬＵＣＡ ｄｅ Ａｌｆａｒｏ， ＴＨＯＭＡＳ Ａ， ｅｔ ａｌ． Ｓｔｒａｔｅｇｙ ｉｍｐｒｏｖｅｍｅｎｔ ｆｏｒ ｃｏｎｃｕｒｒｅｎｔ ｒｅａｃｈａｂｉｌｉｔｙ ａｎｄ ｔｕｒｎ⁃ｂａｓｅｄ ｓｔｏｃｈａｓｔｉｃ ｓａｆｅｔｙ ｇａｍｅｓ［Ｊ］． Ｊｏｕｒｎａｌ ｏｆ ｃｏｍｐｕｔｅｒ ａｎｄ ｓｙｓｔｅｍ ｓｃｉｅｎｃｅｓ， ２０１３， ７９： ６４０－６５７． ［１２］ＡＬＦＡＲＯ Ｌ ｄｅ， ＦＡＥＬＬＡ Ｍ， ＨＥＮＺＩＮＧＥＲ Ｔ， ｅｔ ａｌ． Ｔｈｅ ｅｌｅｍｅｎｔ ｏｆ ｓｕｒｐｒｉｓｅ ｉｎ ｔｉｍｅｄ ｇａｍｅｓ［Ｃ］ ／ ／ １４ ｔｈ Ｉｎｔｅｒｎａｔｉｏｎａｌ Ｃｏｎｆｅｒｅｎｃｅ ｏｎ Ｃｏｎｃｕｒｒｅｎｃｙ Ｔｈｅｏｒｙ． Ｍａｒｃｅｉｌｌｅ， Ｆｒａｎｃｅ ， ２００３： １４４－１５８． ［１３］ ＴＨＯＭＡＳ Ｂｒｉｈａｙｅ， ＦＲＡＮ Ｃｏｉｓ， ＬＡＲＯＵＳＳＩＮＩＥ， ｅｔ ａｌ． Ｔｉｍｅｄ Ｃｏｎｃｕｒｒｅｎｔ Ｇａｍｅ Ｓｔｒｕｃｔｕｒｅｓ［Ｃ］ ／ ／ Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ １８ｔｈ ｉｎｔｅｒｎａｔｉｏｎａｌ ｃｏｎｆｅｒｅｎｃｅ ｏｎ Ｃｏｎｃｕｒｒｅｎｃｙ Ｔｈｅｏｒｙ． Ｌｉｓｂｏｎ， Ｐｏｒｔｕｇａｌ， ２００７： ４４５－４５９． ［ １４ ］ ＲＡＪＥＥＶ Ａ， ＴＨＯＭＡＳ Ａ， ＨＥＮＺＩＮＧＥＲ， ｅｔ ａｌ． Ａｌｔｅｒｎａｔｉｎｇ⁃ｔｉｍｅ ｔｅｍｐｏｒａｌ ｌｏｇｉｃ［ Ｊ］． Ｊｏｕｒｎａｌ ｏｆ ｔｈｅ ＡＣＭ， ２００２ ，４９（５）： ６７２－７１３ ． ［１５ ］ ＣＨＥＮ Ｔａｏｌｕｅ， ＬＵ Ｊｉａｎ． Ｐｒｏｂａｂｉｌｉｓｔｉｃ ａｌｔｅｒｎａｔｉｎｇ⁃ｔｉｍｅ ｔｅｍｐｏｒａｌ ｌｏｇｉｃ ａｎｄ ｍｏｄｅｌ ｃｈｅｃｋｉｎｇ ａｌｇｏｒｉｔｈｍ ［ Ｃ ］ ／ ／ Ｆｏｕｒｔｈ Ｉｎｔｅｒｎａｔｉｏｎａｌ Ｃｏｎｆｅｒｅｎｃｅ ｏｎ Ｆｕｚｚｙ Ｓｙｓｔｅｍｓ ａｎｄ Ｋｎｏｗｌｅｄｇｅ Ｄｉｓｃｏｖｅｒｙ （ ＦＳＫＤ）， ２００７． Ｈａｉｋｏｕ， Ｃｈｉｎａ， ２００７： ３５－３９． ［１６］ＣＨＲＩＳＴＥＬ Ｂａｉｅｒ， ＴＯＭÁŠ Ｂｒáｚｄｉｌ， ＭＡＲＣＵＳ Ｇｒößｅｒ， ｅｔ ａｌ． Ｓｔｏｃｈａｓｔｉｃ ｇａｍｅ ｌｏｇｉｃ［Ｃ］ ／ ／ Ｃｏｎｆｅｒｅｎｃｅ： Ｑｕａｎｔｉｔａｔｉｖｅ Ｅｖａｌｕａｔｉｏｎ ｏｆ Ｓｙｓｔｅｍｓ． Ｅｄｉｎｂｕｒｇｈ， ＵＫ ，２００７： ２２７－２３６． ［１７］ＭＡＲＴＡ Ｋｗｉａｔｋｏｗｓｋａ Ａ ， ＧＥＴＨＩＮ Ｎｏｒｍａｎ Ａ ， ＪＥＲＥＭＹ Ｓｐｒｏｓｔｏｎ Ｂ， ｅｔ ａｌ． Ｓｙｍｂｏｌｉｃ ｍｏｄｅｌ ｃｈｅｃｋｉｎｇ ｆｏｒ ｐｒｏｂａｂｉｌｉｓｔｉｃ ｔｉｍｅｄ ａｕｔｏｍａｔａ［Ｊ］． Ｉｎｆｏｒｍａｔｉｏｎ ａｎｄ ｃｏｍｐｕｔａｔｉｏｎ， ２００７， ２０５（２）： １０２７－１０７７． ［１８］ＭＡＲＴＡ Ｋｗｉａｔｋｏｗｓｋａ， ＧＥＴＨＩＮ Ｎｏｒｍａｎ， ＤＡＶＩＤ Ｐａｒｋｅｒ， ｅｔ ａｌ． Ｐｅｒｆｏｒｍａｎｃｅ ａｎａｌｙｓｉｓ ｏｆ ｐｒｏｂａｂｉｌｉｓｔｉｃ ｔｉｍｅｄ ａｕｔｏｍａｔａ ｕｓｉｎｇ ｄｉｇｉｔａｌ ｃｌｏｃｋｓ ［ Ｊ ］． Ｆｏｒｍａｌ ｍｅｔｈｏｄｓ ｉｎ ｓｙｓｔｅｍ ｄｅｓｉｇｎ， ２００６， ２９（１）： ３３－７８． 作者简介： 王晓燕，女，１９７７ 年生，讲师，博士， 主要研究方向为软件建模与验证技术、 软件开发新方法。 申请发明专利 ２ 项， 并获得 ２０１０ 年中国国家专利优秀奖， ２００８ 年吉林省科技进步一等奖，中国商 业科技进步二等奖。 发表论文 ２０ 余 篇，其中被 ＳＣＩ 收录 ５ 篇。 韩啸，男， １９８１ 年生，编辑，博士研 究生，主要研究方向为网络协同、软件 建模和网络技术。 彭君，男，１９８１ 年生，讲师，博士，主 要研究方向为模型驱动技术、构件技 术、软件体系结构。 第 ５ 期 王晓燕，等：实时并发系统的 ＰＴＳＬ 模型检测 ·７０１·