参数化系统的模型检查方法研究与验证

理论计算机科学电子札记98（2004）57-74www.elsevier.com/locate/entcs实时系统奥尔加·格林奇坦1马丁·卢克尔2乌普萨拉大学IT系瑞典乌普萨拉摘要我们扩展的方法，通过网络不变量的设置实时系统的模型检查参数化网络的过程。 我们引入了时间转换结构（在精神上类似于时间自动机），并定义了一个抽象的概念，它对线性时间属性是安全的。 我们加强了抽象的概念，允许一个有限的系统，然后称为网络不变，是一个抽象的网络的实时系统。一般来说，实时系统的抽象检验问题是不可判定的。因此，我们提供了足够的标准，可以自动检查，得出结论，一个系统是一个具体的抽象。 我们的方法是基于定时叠加和离散化的定时系统。我们通过证明一个简单协议的互斥性来验证我们的方法，该协议的灵感来自Fischer协议，使用Weizmann关键词：模型检测，网络不变量，参数化系统，叠加1介绍模型检查是一种验证并发系统的方法，其中将系统的高级描述的计算与逻辑需求规范制定的计算进行比较，以确定它们是兼容的。检查有限状态系统的线性时序逻辑（LTL）规范是很好理解的。然而，面对由任意数量的进程并行工作组成的并发系统，模型检测更具挑战性，因为我们必须处理无限多的状态。一1电子邮件：Olga. it.uu.se2电子邮件：Martin. it.uu.se本文作者由欧洲研究TrainingNe twork“G a mes“支持。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2003.10.00658O. Grinchtein，M. Leucker / Electronic Notes in Theoretical Computer Science 98（2004）检查这些参数化系统的有效方法是使用抽象和网络不变量。抽象的思想是检查一个更小的有限状态系统，而不是原来的系统。如果较小的系统提供了更多的计算，包括原始系统的计算，它满足的每个线性时间逻辑属性也适用于原始系统。对于分支时间逻辑，如果我们将逻辑限制为通用片段，则类似的想法也适用[6]。原始系统的抽象在第一种情况下，必须证明抽象系统确实包含了原始系统的所有计算构建抽象模型的基本原理可以从以下几个方面[8、7、9]。通过网络不变量的验证在[19]中引入，并在[14]中成为一种工作方法。简而言之，这个想法可以概括如下。假设我们有一个有限状态过程Φ，例如，重复请求和释放某些资源。我们想推理一个设置，其中任意数量的Φ实例并行工作。 换句话说，我们研究系统Φ1<$···<$ Φn，其中Φ的实例数n未知提前虽然对于每个n，我们处理的是一个有限系统，但显然不可能对所有n迭代地检查系统。利用抽象的思想，它可以找到一个满足我们的要求规范的有限状态系统ΦA，它对任意n抽象Φ1···Φn。类似于自然数上的归纳法，如果ΦA是一个不变量，即，ΦA是一个Φ的抽象以及ΦA的抽象。第一项表明，Φ A可以抽象为ΦA， ΦA可以进一步抽象为ΦA，使用第二个要求。通过这种方式，检查参数化系统被简化为找到一个可能的网络不变量，该网络不变量满足对参数化系统的要求，并证明它确实是一个网络不变量。 找到一个可能的不变量通常是手动执行的，而检查它是否满足需求规范可以使用模型检查自动完成。证明一个系统是一个网络不变量可以简化为检查抽象，这可以自动完成有限状态系统。这种方法在[13]中被详细阐述用于检查公平离散系统的线性时间规范，其中还讨论了寻找不变量的技术。传统的模型检测技术不承认显式建模的时间，因此不适合实时系统的分析。 布雷尔Dill引入了时间自动机来模拟实时系统的行为。此外，还开发了模型检查技术[4]。O. Grinchtein，M. Leucker / Electronic Notes in Theoretical Computer Science 98（2004）59本文研究了参数化时间系统的推理问题据我们所知，这是研究时间系统网络中[19我们遵循[13]的大纲，其中研究了公平离散系统的并行系统，但用时钟来丰富底层系统以模拟定时行为。我们将抽象和网络不变量的概念扩展到定时设置。本文的一个主要贡献是检查一个给定的定时转换结构是否是另一个抽象的过程。我们引入了类似于定时自动机的定时转换结构。主要的区别在于我们区分了私有变量和全局变量，并且通信是通过共享变量而不是消息传递。因此，我们的通信模型更接近Java类并发编程语言。我们说ΦA是Φ的抽象，如果ΦA至少包含Φ的计算这个想法被使用，例如。在[1]中。我们表明，我们的抽象概念是安全的线性时序逻辑，即，一个抽象系统的线性时间特性也适用于一个具体系统。提供进一步的环境行为被考虑在内，我们表明，检查系统是否是一个网络不变可以减少到证明抽象。请注意，虽然时钟可以被理解为实值变量，但它们与普通的数据变量不同，因为所有时钟的时间都是同步进行的。如果时间δ对于时钟x通过，那么它对于时钟y也通过。将时钟视为实值变量会忽略时钟的这种这种隐含的时钟依赖性是将网络不变量方法扩展到实时系统设置我们提供了足够的标准，可以自动检查，以断定一个系统是一个具体的抽象。我们的方法基于时间叠加[12]。Φ和ΦA的叠加是类似于定时转移结构的结构，其计算可以被投影到Φ和ΦA的计算，其中尽可能好地，ΦA试图跟随Φ的移动。我们证明，如果叠加满足某些LTL性质，ΦA确实是Φ的抽象。为了检查叠加是否满足LTL性质，我们使用由[10]和[5]开发的时间转移结构的离散化概念这允许我们使用标准验证工具，如TLV [16]。作为副产品，我们的工作还澄清了60O. Grinchtein，M. Leucker / Electronic Notes in Theoretical Computer Science 98（2004）实时系统的设置。我们的方法是通过使用Weizmann的模型检查器TLV [ 16 ]证明受Fischer协议启发的简单协议的互斥来证明的我们将自己限制在有限的数据变量域。使用谓词抽象（见[11]，[13]），应该可以将我们的结果扩展到变量范围在无限域上的系统。类似于我们的定时转移结构的系统已经在[15]中进行了研究该方法基于自动抽象，但仅限于检查整数时域的时间系统的安全性。文献[2]和[3]提出了一种研究参数化系统的不同方法。它基于无限状态集的有限符号表示以及计算原像和收敛。结果表明，这种系统的可达性是可判定的，如果每个进程有一个单一的时钟。我们的方法也适用于验证具有任意数量的时钟系统的活性性质由于我们是在LTL的背景下发展我们的理论的，所以我们的抽象概念当考虑分支时间逻辑时，模拟对于定义抽象变得很自然这种方法是针对定时系统[18]进行研究的，结果表明仿真是可判定的。然而，网络不变量的问题没有得到解决。注意，模拟是比语言包含更强的关系，即，当抽象基于语言包含而不是模拟时，可能更在下一节中，我们将定义时间转换结构。第3节回顾了LTL的语法和语义（在定时设置）。在第4节中，我们开发了使用网络不变量的验证方案，我们定义了时间转移系统的离散化，并证明了我们的离散化在LTL性质方面是正确的。我们在第5节中说明了我们的方法。最后，我们总结了我们的研究结果。2时间转换结构时域I是一个全序幺半群，其最小元素等于中性元素。通常，我们考虑I= R+，非负实数的集合，和I= IN，自然数的集合（包括0）。一个时钟，用x，x1，. 是在时域上解释的变量。 给定一组有限的时钟C ={x1，. ，xn}，时钟赋值是函数v：C→ I，它为每个时钟x∈C分配一个时间。如果I= R+，则我们表示y[v（x）<$（ respectivelyTv（x）2）x相对于给定时钟估值v的整数（分数）p。设t ∈ I，v + t和v↓复位O. Grinchtein，M. Leucker / Electronic Notes in Theoretical Computer Science 98（2004）61+和reset_C表示对于所有时钟x ∈ C满足（v + t）（x）= v（x）+t的时钟赋值，并且对于x ∈ reset分别满足（v↓reset）（x）= 0和对于x∈ /re s e t分别满足（v ↓ r e set）（x）=v（x）。如果C是一组时钟，则时钟约束的集合XC是形式为x<$c的原子公式的布尔组合的集合，其中<$∈ {<，≤，>，≥}且c∈IN。定义2.1元组Φ =（D，C，W，O，Θ，λ， θ）是一个时间转换结构（TTS），其中• D ={d1，.，d r}是在有限域上的离散变量的有限集合。设D是（数据）赋值的集合，其中（数据）赋值将D中的变量映射到它们的域。• C ={x1，.，xn}是一组有限的时钟，每个时钟的范围都在R +上。时钟不能是数据变量。• 除了C中的时钟之外，TTS还有一个主时钟，用now表示，它不会因为任何一次跃迁而改变。 我们用y C <$表示C与现在的结合。• WecallV=DC<$3 系统变量集和Φ的状态集S=D ×RC。因此，一个状态的形式是（κ，v），其中κ是一个赋值，v是一个clock赋值，它在C时间内表示一个v的clock。We表示s（d）和s（c）变量d的值和状态s中时钟c的值。• W是一组有限的自有变量，不能被环境修改。• OV是环境可以观察到的变量的有限集合。我们需要V=WO。我们现在要求是可观察的，即，现在∈O.• Θ是初始条件，它是一组对表征初始状态的状态的断言（一阶公式）。要求在初始状态下所有时钟都等于0。• λ<$D ×D × XC×2C是转换表。一个条目（κ，κJ，g，reset）∈λ应该读作：如果保护g满足，则从赋值为κ的状态移动到赋值为κJ的状态，并重置reset中列出的时钟。• 其中φκ是一个断言，它在赋值为κ的状态下成立，且对于κ∈ D，pκ∈XC。我们把O中的变量称为全局变量，把O−W中的变量称为共享变量，把W−O中的变量称为局部变量。全局、共享和本地时钟和数据变量以预期的方式定义3 XY表示X和Y的不相交并集。62O. Grinchtein，M. Leucker / Electronic Notes in Theoretical Computer Science 98（2004）λ−→RT[x≤2]Fig. 1. 例如示例2.2TTS的一个简单示例如图1所示。我们有（数据）变量d和s。d表示资源繁忙，也可能被并行运行的其他进程更改，而s只是标识系统是处于初始阶段还是已经启动。我们将d设为可观察的，假设s是本地的。我们有一个时钟X。从s和d等于0的初始状态，如果已经过去了至少一个时间单位，有时，我们在边上添加一个标签，如s：= 1，以强调在进行此转换时变量s确实发生了在第二种状态下，系统可以保持直到时间达到2，或者，它移动到第三种状态，其中d的值被重置。LetusfixaTTSΦ =（D，C，W，O，Θ，λ，λ）（其中h|C|=n）对于本节的内容。 对于TTS，我们区分两种类型的转换，−→RT和蜱λJ J J−→RT，S × S的两个子集。我们写s=（κ，v）−→RTs=（κ，v）i <$，存在（κ，κJ，g，reset）∈λ使得v| = g，vJ|= p κJ，且vJ= v↓reset。换句话说，如果满足κJ的时间进展条件和跃迁的保护，我们从s移动到sJ，在这在这种情况下，我们称SJ为s的λ-后继。 我们写s =（κ，v）ticksJ=（κJ，vJ）i跃迁仅由某个时间延迟δ引起，也就是说，如果κJ=κ，a δ > 0，使得vJ=v + δ，且φ 0 ≤t≤δ：v + t| = p κ。 在这种情况下，我们称sj为s的tick-successor。因此，一个时间跃迁结构Φ诱导出一个无限态跃迁系统，表示为[Φ]RT=（S，−→RT），状态S转换关系−→RT=−λ→蜱RT− →RT。Φ的游程是状态π=s0，s1，.的有限或无限序列。 使得s0<$Θ（初始性），且对于每个j≥0sj−→RTsj+1（连续性）。此外，如果现在的值增长超过任何界限（时间发散），我们称π为Φ的计算。形式上，我们要求对于每个c∈R+，有一个j∈IN使得sj（现在）> c。当比较两个时间转移结构的计算时，我们通常只对可观测变量感兴趣。设Ocomp（Φ）={π|O|π是Φ的计算，其中对于计算π = s0，s1，. 我们用π表示|0序列s0|O，s1|噢...如果TTS与环境（例如同一进程的其他实例）并行运行，则环境可能会更改共享数据变量或重置共享时钟。因此，我们还研究了一个[x≥1]s：=1d：=1d=0d =0d =1s=0s =1s =1O. Grinchtein，M. Leucker / Electronic Notes in Theoretical Computer Science 98（2004）63JJJ当把它放到一个任意的环境中。 设λ env={（κ，κJ，true，reset）|κ（d）= κJ（d），如果d∈W，则复位后的k_（W）=k_j（d）表示给定变量的一个有效值的可能变化。Wewritees=（κ，v）−λe→nvRTsJ=（κJ，vJ）i <$存在（κ，κJ，true，reset）∈λenv，其中vJ=v↓reset.Φ的模游程是一个有限或无限序列π =（s0，λ）（s1，m1）.在{λ，env，tick}中的状态和标记，使得s0<$Θ（初始化）和对于每个j≥0s−λ→RT sj+1 mj+1=λ，s−λe→λ eRTs j+1 mj+1=env且nots−λ→RTsj+1，或s蜱j−→RTsj+1 mj+1=tick。 π被称为模，如果时间发散的话，我们用mocomp（Φ）={π|O|π是Φ}的模计算，Φ}是限制于可观测变量的模计算的集合对于模计算π =（s0，m0）（s1，m1）. 我们用π表示|0序列（s0|O，m0）（s1|O，m1）.设Φ1 =（D1，C1，W1，O1，θ1，λ1， λ1）和Φ2 =（D2，C2，W2，O2，θ2，λ2， λ2）betwoTTSswithD1C2=D2C1= 。 我 们 说 如 果 W1<$W2= ， W1<$O2= 和 W2<$O1 =，则Φ 1和Φ2是可合并的. 在这两个词中，Φ1和Φ 2拥有不同的变量，只有共同的可观测变量。如果Φ 1和Φ 2是可合成的并且是TTS Φ=（D，C，W，O，Θ，λ，λ），则定义Φ 1和Φ 2的平行合成，表示为Φ 1 <$Φ 2，其中D= D12，Θ = Θ1< $Θ2，λ是D× D ×XC×2C中投影到Φi的变量上的最大关系，当i∈{1， 2}时，它与λi一致。注意，并行组合是可交换的，即，Φ1< $Φ2 =Φ2< $Φ1。为了简化我们的演示，我们假设无论何时构建两个TTS的并行组合，它们都是可组合的。3线性时序逻辑作为一种需求规范语言，我们使用线性时态逻辑（LTL）的口吃不变版本。时间公式p的模型是状态π = s0，s1，...的无限序列。其中每个状态s提供对p中的变量的解释。状态公式由陈述可观测数据变量和时间变量的属性的命题构造而成，其中后者是仅限于时钟约束，以及布尔运算符<$和<$。 的时间公式是由状态公式构造的，我们对状态公式应用布尔运算符和时态运算符U（直到）。与一般的LTL相反，我们不考虑下一个状态算子，因为下一个状态的概念在（密集）定时系统的设置给定一个模型π，我们给出了一个时间公式p在π中的位置j≥ 0的概念的归纳定义，记为（π，j）|= p。64O. Grinchtein，M. Leucker / Electronic Notes in Theoretical Computer Science 98（2004）• 对于一个状态公式p，（π，j）|= p惠s j|= p，• （π，j）|=<$p惠（π，j）|= p，• （π，j）|= p q惠（π，j）|= p或（π，j）|= q，• （π，j）|= pUq惠k≥j（π，k）|= q且对于每个i使得j≤i< k，（π，i）|= p。像往常一样，可以定义额外的时间运算符，例如Qp=真实的Up和Qp=<$Q <$p。如果（π，0）|= p，我们说π满足p，写π| = p。一个公式p被称为有效的，如果p在所有模型上成立。给定一个TTS Φ和一个时间公式p，我们说p是Φ-有效的，记为Φ |=p，如果p在所有计算Φ的模型上成立。这个概念通过考虑模块化计算而扩展到模块化有效性。4网络不变量在本节中，我们定义了由时间转移结构构建的参数化系统的网络不变量的概念。我们把问题归结为对两个时间转移结构叠加的某些公式的模型检验。对于后者，我们将展示如何构建离散化系统，可以使用标准的LTL模型检查器进行检查。4.1网络不变量和连续时间给 定 两 个 TTS Φ 和 ΦJ ， 我 们 说 它 们 是 可 比 的 ， 如 果 O=OJ ，O<$W=OJ<$WJ，也就是说，它们具有“相同”的可观测变量。为了简化我们的演示，让我们为此固定两个可比较的TTS Φ和ΦA科.我们首先定义了时间转换结构的抽象概念。定义4.1我们说ΦA是Φ 的抽象，记为Φ ±RT ΦA，iocomp （Φ ）ocomp（ΦA），并称Φ为具体系统，ΦA为抽象系统。因此，ΦA是Φ的抽象，如果对于投影到可观测变量的具体系统的每一次计算，都存在具有相同投影的抽象系统的计算很容易看出，抽象关系是传递的。例4.2图2所示的TTS是例2.2中所解释的TTS的抽象。我们记得，d是唯一可观察到的变量。在前面的例子中，唯一可观察到的计算是O. Grinchtein，M. Leucker / Electronic Notes in Theoretical Computer Science 98（2004）65d：=1d= 0时d= 1d：= 0图二. 例如（d = 0）（d = 0）（d = 1）（d = 0）（d = 1）.. . .这显然包含在图2所示的TTS的可观察计算中。抽象关系在以下意义上是安全的：定理4.3设p是LTL公式。 如果Φ A|= p和Φ ±RTΦ A，则Φ |= p.注意，另一个方向通常不成立，即，如果ΦA不满足性质p，Φ仍然可以满足。网络不变量的基本思想由以下定理捕获定理4.4如果Φ和 ΦA满足（一）Φ ±RTΦA，（一2）对于所有的TTS，我们有Φππ ±RT ΦA π，（I3）ΦA≤ ΦA±RT ΦA，和（I4）对所有的TTS <$我们有（Φ A<$Φ A）<$<$T±RTΦ A<$T，则Φ A···<$Φ ±RTΦ A。证据由于（I2），ΦA······Φ可以抽象为Φ A····由于交换性，这等于Φ<$ ΦA <$Φ <$··<$Φ。同样由于（I2），这可以抽象为ΦA<$ΦA <$Φ <$··<$Φ。迭代这一论证并利用抽象关系的传递性，我们得到了Φ··· Φ±RT ΦA<$··· ΦA.请注意，我们假设Φ有多个副本对于一个副本（I1）给出了相同的参数。利用（I3）和（I4），可以很容易地看出，ΦA≤···≤ ΦA±RT ΦA。总之，这意味着Φ··· Φ±RTΦA。Q注意，前面的定理可以用下面的方式来简化：取Φ为Φ的副本，但去掉不可观测的变量，那么Φ等于Φ。因此，（I2）包含（I1），（I4）包含（I3）。4定理4.4提出了以下策略来验证网络的性质：找到一个抽象ΦA，检查它是否满足所讨论的性质，并证明（I1）-（I4）。然而，（I2）和（I4）在以下情况中不是建设性的：4.一个没有“empty”TTS的国王将为他服务。66O. Grinchtein，M. Leucker / Electronic Notes in Theoretical Computer Science 98（2004）[x >1]d：= 001(a)Φ[x= 1]d：= 001(b)ΦA[x >1]d：= 101(c)Ψ图三. 例如它需要检查所有TTS的意义。因此，我们追求一种更强的抽象关系，使该方法有效。定义4.5我们说Φ A是Φ的模抽象，表示为 Φ ±MΦ A，i_（？）模块化抽象是我们正在寻找的：定理4.6如果Φ ±MΦA，则对于所有TTS，我们有Φ 100±RT Φ100证据 我们给出一个证明的草图。给出了一个计算Φ的公式，一个任意的系统，我们可以通过标记随着环境的变迁，模块抽象指出，当将该序列限制为Φ的可观测变量时，它也是ΦA限制为可观测变量的序列之一。现在仔细的研究表明，对于φ的跃迁，这个序列可以具体化为ΦA φ的计算Q前面的定理得到（I2），取Φ = ΦA< $ΦA也是（I4）。虽然这看起来很简单，但它之所以成立，是因为我们现在要求时钟是可观察的：例4.7现在考虑图3中没有隐式可观测时钟的TTS Φ、ΦA和Φ B。在所有限制于可观测变量的Φ和ΦA的模计算中，我们观察到0被分配给d。我们可以得出Φ ±MΦA. 然而，Φφ的一个计算是d= 1;d= 0，这在Φ A中是不可能的现在要求可观察揭示了，Φ/±M ΦA。如何证明Φ ±MΦA？使用时间自动机的结果，很容易看出这个问题是不可判定的，不像离散系统.因此，我们专注于充分的条件。我们使用叠加的思想（扩展到定时设置），然后是时间的离散化。两个TTS Φ和ΦA的叠加是确保ΦA在模拟Φ时尽力的TTS。此外，我们允许用户提供额外的我们添加一个布尔数据变量mis，它是O. Grinchtein，M. Leucker / Electronic Notes in Theoretical Computer Science 98（2004）67S一一如果ΦA不可能跟随Φ，或者用户定义4.8对于两个可组合和可比较的时间跃迁结构Φ =（D，C，W，O，Θ，λ， λ）和ΦA =（DA，CA，WA，OA，A，λA，λA），我们定义它们的叠加sp（Φ， ΦA， Θd，λd）为定时转移结构ΦS =（DS，CS，WS，OS，θS，λS，λS），其中• D S= DD A{mis}，C S= CC A，• WS=WWA{mis}，OS=O{mis}=OA{mis}，• ΘS =（Θ θA θd（mis=false））（Θθ（ΘA θd）（mis=true）），θS=A，• θ d是D S上的断言，使得θ → θ d D，|CSJ• λd<$DS× DS× XCS×2，使得（κ，κ，g，reset）∈λ意味着存在is（κ，κJ，g，r^eset）∈λdwiththκ|D=κ，κJ|D=κJ，g→g，且d^eeet |D=reset，• λS=λ<$S<$λd，其中reλ <$S<$D S×DS×XC×2CS，其中h（κ，κJ，g，reset）∈λ<$S，如果下列之一成立：(i) 如果κ（miss）=f，则还没有发生失配我们区分：·如果存在一个gJ使得（κ|D，κJ|D，g，J，复位|C）∈λ，设gΦ为距离，所有这些GJ的连接点。设gΦ是所有gJ的析取，使得（κ|DA，κJ|D，gJ，reset|C）∈λA，其中空析取为假。J然后我们要求g=gΦgΦA和κ（mis）=false，说明两者都系统的保护是满意的，没有发现不匹配，或者，g=gΦ<$gΦ和κJ（mis）=真，描述了Φ可以移动但ΦA不能移动的情况，因此发现了失配·或者，取一个环境转换，我们要求g=true，κ（d）=κJ（d）如果d∈W，resetW=，且ndκJ（mis）=false(ii) 如果κ（miss）=true，那么我们需要g=true，κ=κJ，reset=k简单地说，叠加将两个结构的变量结合起来，以合取的方式将初始条件和级数条件结合起来，并允许两个系统中的步骤同步进行（第i项）。如果一步在Φ中是可能的，但在ΦA中是不可能的，我们就进入一个mis=true的状态（第ii项），并停留在那里。定理4.9设Φ和Φ A是两个可比较的时间转移结构。设λ d和Θ d为用户定义的确定条件。 如果sp（Φ J，Φ A，Θ d，λ d）满足然后是Φ ±MΦA。Φ S|= Q（（<$A）mis = false）（1）在（1）中，我们还检查了进度条件，以保证ΦA能够应付一一68O. Grinchtein，M. Leucker / Electronic Notes in Theoretical Computer Science 98（2004）12N对于Φ的所有刻度转换现在仍需检查Φ S|= Q（（<$A）mis = false）. 为了能够使用标准的LTL模型检查器，我们采用了TTS的离散化。4.2时间转移结构在本小节中，我们将满足相同线性时间性质的有限状态转移系统与定时转移结构相关联。这允许我们使用有限状态机的LTL模型检查器来分析定时转换结构。我们使用[10]和[5]中给出的离散化，尽管我们的表示不同。首先，我们定义时钟赋值的标准区域等价关系[4]如下：令K表示出现在定时转移结构的保护和不变条件中的最大常数。We letv vJ i for allx，y∈C，• v（x）> KivJ（x）> K，• 如果v（x）≤K，则then[（v（x））]=[vJ（x）]且Tv（x）2=0i<$TvJ（x）2=0，且，• 若v（x）≤K且v（y）≤K，则Tv（x）2≤Tv（y）2 i <$TvJ（x）2≤ TvJ（y）2。赋值v关于的等价类称为时钟区域，用[v]表示。根据定义，每个时钟区域都可以通过时钟的整数值及其小数部分的排序来唯一识别。换句话说，对于赋值v和vJ以及序列0 <$1Tv（x i）2<$2···<$n，Tv（xi ）<$1和0<$JTvJ（xi）<$$>J···<$JTvJ（xi<）²<1我们有vvJin112nn[v（xi）<$=[vJ（xi）<$]且<$i=<$J，<其中对于i∈{1， . . ，n}。我我时钟的分数值的顺序可以存储在包含时钟的插槽阵列中（见图4（a））。第一个时隙包含所有Tv（x）²= 0的时钟x，其余时隙根据分数值的顺序填充。[5]虽然一般情况下会有n+1个槽，但为了简单起见，我们取2n个槽。我们区分偶数和奇数槽，并遵循惯例，只要其中一个小数值为0，我们就只使用偶数槽，而如果所有小数值都大于0，我们就使用奇数槽，并以二维方式绘制数组（图4（b））。现在很明显，所有的区域等价类都可以用K乘以2n个时隙来表示，加上一个时隙用于值为K的时钟，一个时隙用于值大于K的时钟。图4（c）显示了K= 2和n= 3的设置现在可以直接定义定时转换结构的离散化语义设k =1为离散化步长。离散化时间[5]当然，如果不施加进一步的限制，这种表示就不是唯一的O. Grinchtein，M. Leucker / Electronic Notes in Theoretical Computer Science 98（2004）69∆−→RTJ我0<<<< 1x1x2X3X4X50奇偶...0 1KX1X2X3(a) 槽（1b）2nslo2tns−1（c）时域> K见图4。 时隙和离散时域定义域I={s} |s ∈ IN，0 ≤ s ≤ 2 nK +1}（见图4（c）。对于j ∈ {0，.2 n − 1}如果Tv（x）²= j<$$>，我们说时钟x占用时隙j，并称x的值为偶数（奇数）i <$j分别为0或偶数（奇数）。Φ的离散化转移系统记为[Φ]DT，是一个有限状态转移系统（SDT，ΘDT，−→DT），其中状态集为SDT=D×IC<$ ，初始状态条件ΘDT满足Θ，并且−→DT，λ tick关系，定义为−→DT=定义为−→DT−→DT。后一种关系是蜱• s=（κ，v）−→DTsJ=（κ，vJ）istick（κ，v+ε）和dvJ=v+ε，其中Δ=min{x + y，K + k}扩展到预期的估值。• s=（κ，v）−λ→DTsJ=（κJ，vJ）i<$（κ，v）−λ→RT（κJ，vJJ）and，· 如果存在具有v（x）= 0的时钟x和具有奇数值的时钟yj∈ {0，. ，2 n-1}是不被任何时钟占用的奇数时隙。 对于vJJ（x） K，我们令vJ（x）=vJJ（x）。· 否则仅使用偶数槽和槽0，或者所有槽都是奇数，并且我们让vJ=vJJ。[Φ]DT的游程是它在初始状态开始的任何无限路径。[Φ]DT的计算是一次运行，其中进行了无限多次滴答转换。让我们检查一下，相对于计算，Φ和[Φ]DT可以被识别。设（κ，v）<$ （ κJ ， vJ ） i <$κ=κJ 且 v vJ. 对 于 计 算 π ： s0 ， s1 ， . .对 于 Φ ， letπ<$beesequenceπ<$：s<$0，s<$1， . . . 这是π的子序列，其中当y等于π时，π的后续状态被压缩为单个状态。 Thatis，π<$：si0，si1， . . . 和，0= i0 β]d：=4[φ]d：=0[<$φ][d4≤2]xi：= 0，d：=i[d4i> 3]xi：=0，d：= 37 6 4 3[φxi>β]φ=（（i≤2<$d =i）<$（i >3<$d = 3））图五. Fischer协议的改进我们想证明，进程Φ1和Φ2都不能到达状态7，而且它们永远不会都处于状态4，这是一个标准的互斥性质。它可以被形式化为p=Q（loc1≤6Ω（loc1 = 4Ωloc2 = 4））我们的目标是构造一个网络不变量ΦA，满足ΦA··· Φ±MΦA和Φ1< $Φ2<$ ΦA<$p。一个自然可能的网络不变量，用Φc如图所示，图6（a）.它的状态空间由d的所有可能值和根据目标状态设置的转换d组成。 由于ΦA应该抽象Φ3，因此状态1和2（其被示出为单个状态以简化呈现）是只能通过环境迁移才能到达我们加上Φc一个时钟x，当移动到状态0或4时由Φ施加的定时约束保存当3被分配给d时，我们必须重置时钟x。我们可以自动检查Φ±M Φc。然而，如果我们试图证明因此，Φc公司简介±MΦc我们得到一个反例：考虑运行的Φc [1]<$ Φc [2]由6给出A A（d=0，x [1]= 0，x [2]= 0）→···→（d=0，x [1]> β，x[2]> β）→（d= 3，x [1]= 0，x [2]> β）→（d= 4，x [1]= 0，x [2]> β）有一个运行s0，...，si，. 的Φ c[3]，使得si（d）= 0且si+1（d）= 3。那么，由于Φc将值d修改为3重置x，不可能进行从si+1到si+2的转换，使得si+2（d）= 4。因此Φc不是网络不变的。例如，我们通过将时钟y添加到Φc来获得网络不变量ΦA它永远不会被Φc使得设置d= 4的转换只取决于新的时钟。这个不变量如图6（b）所示。我们可以O. Grinchtein，M. Leucker / Electronic Notes in Theoretical Computer Science 98（2004）736我们使用附言[i]来区分Φ实例的局部变量74O. Grinchtein，M. Leucker / Electronic Notes in Theoretical Computer Science 98（2004）x：=0x：=0x：=0x：=0d：=3x：=03d：=0[x≤β]d：= 0d：= 3x