Timed CSP的增强版本与封闭的时间自动机等价关系及其表达能力的研究

URL：http://www.elsevier.nl/locate/entcs/volume 68. html18页sTimed CSP = Closed Timed Automata1（闭合时间自动机1）JoéelOuaknine2，3andJamesWorrell杜兰大学数学系，美国摘要我们研究了一个增强版本的时间CSP的表达能力，并表明，它是完全等于封闭的时间自动机的时间自动机与封闭的不变量和使时钟约束。我们还表明，这个新版本的Timed CSP具有足够的表达能力，可以将时间系统上最广泛使用的规范捕获为进程之间的细化，此外，细化检查可以进行数字化分析。因此，我们能够使用模型检查器FDR（Formal Systems（Europe）Ltd.的商业产品）来验证一些最重要的时间规范，包括分支时间活性属性，如时间停止自由和常数可用性。1介绍实时系统的形式化分析通常涉及实现和规范形式化，以及决定特定实现是否满足给定规范的机制例如，人们可以选择时间自动机的框架[4]作为实现形式主义，并选择一些（定量）时间逻辑来表达规范[6]。然后可以使用模型检查进行验证[3]。在Reed和Roscoe验证过程满足其规范，然后通常通过某种证明系统进行[24，11，25]。在密集时间建模范式的情况下，很少有人尝试使用实现框架来表达规范，并将满意度作为细化（反向包含行为集我们知道的唯一例子是使用事件时钟自动机来表达（任意）时间自动机的规范[5]。最近，我们发现1这项研究得到了美国的支持ONR和NSF。2现在在CMU计算机科学学院，5000福布斯大街，Pittsburgh PA 15213，USA.3电子邮件地址：joelo@andrew.cmu.edu2002年2月由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。2在Timed CSP的上下文中，离散精化技术可以用于使用模型检查器FDR[16，17]来验证某些密集时间系统的规范Timed CSP的基于refinement的方法的主要缺点是，到目前为止，表现力非常差。这个问题不是精化方法的内在特征，而是Reed和Roscoe的Timed CSP版本的一个人工制品例如，为了表达“进程P不能执行事件a”的规范，必须证明P定义了传送除A之外语义假设Reed和Roscoe提出的良好时间性（过程需要良好定义）禁止了这种任意快速（或Zeno）的过程。因此，一个自然的解决方案是试图减轻对语言的一些限制，以获得更具表现力的TimedCSP版本，其中允许这样的进程在任何给定的时间点可以任意多个事件进行通信。另一个可取的特性是在语言中添加信号，以便能够表达诸如“进程必须在两个时间单位内执行a”之类的规范 当然，我们非常希望我们遵循的路径与CSP保持足够强大的联系，以保留FDR模型检查等技术的使用。因此，我们能够证明，在时间系统上最广泛使用的规范可以被捕获为时间CSP过程之间的精化，而且这些精化可以通过数字化技术在模型检查器FDR上进行验证事实上，我们甚至证明了一些分支时间活性属性，如时间停止自由和常数可用性，可以通过数字化（和FDR）进行验证，与时间自动机的情况相反。我们将这种增强版本的时间CSP的表达能力（当限制为有限状态过程时）与封闭时间自动机的表达能力完全封闭时间自动机是[13]中的时间安全自动机，具有唯一的封闭不变量和启用时钟约束（例如，形式为x≤3而不是x定时CSP似乎是最一般的建模形式主义系统地产生数字化下关闭的过程（因此服从数字化技术），使其成为定时系统的实际形式分析的主要候选人。2时间CSP的语义和语义我们提出了我们的增强版本的定时CSP的语法和语义更多细节可以在[19]中找到，其中我们特别解决了检测活锁进程（能够执行无限多个内部转换）的问题在本文中，我们只考虑无活锁的过程Leteafineitesete Weewriteetodenote{C}.3∈⊆−→Hǁ在下面的符号中，我们有一个和一个。 参数n的范围在非负整数N上。R表示一个关于R的（重命名）关系变量X从过程变量VAR的固定无限集合中提取。时间CSP项根据以下语法构造P：：=停止|定时器停止|a−→P|a−→！P|SKIP|随机|nnP1和P2|P1P2|P1和P2|P1HP2|P1和P2|P1P2|P\A|P [R] |µX。|µX . P.STOP是一个死锁的进程，它只能让时间流逝。TIMESTOP类似于STOP，除了时间本身也是阻塞的;它表示不一致的计时要求。预固定进程aP最初在任何时候都参与事件a，随后表现为likeP. 信号优先级是−→！PCO MUNICA TE SA立即并且随后表现得像P。SKIP表示成功终止，并且愿意在任何时候交流C随机非确定性n等待一个实值的时间量，然后变成SKIP。PQ是一个超时过程，最初在n个时间单位内变为P，之后n如果P未能传送任何可见事件，则其静默地变为Q。PQ是一个中断进程，在前n个时间单位内表现得像P，然后安静地开始表现得像Q（假设P在此期间没有成功P Q表示P和Q之间的非确定性选择，而PQ表示确定性选择。P/Q愿意像P或像Q那样行动，在第一个可见的地方做出决定。活动 平行组合P1一P2需要P1和P2同步在A中的所有事件上，并且对于所有其他事件。PQ是P和Q的顺序组合：它表示一个过程，它的行为像P，直到P选择终止（无声地），在这一点上，过程无缝地开始像Q一样行为。P\A是一个行为类似于P的过程，但集合A中的所有通信都是隐藏的;最大进度或τ-紧急性的假设表明没有时间可以流逝而隐藏的事件是开放的，换句话说，隐藏的事件一旦变得可用就立即发生。重命名的过程P[R]从P的行为中得到它的行为，因为只要P可以执行事件a，P[R]就可以参与任何事件b，使得a R b。最后是递归µX。P表示方程X=P的唯一解。要求所有延迟（项P1中的参数nnnP2，P1P2）be integral是非常有益的--感谢缩放时间的可能性单位，我们同样可以要求合理的延迟，而只是对我们的陈述进行微小的修改。我们写TCSP来表示由此生成的语言的封闭项的集合。（一个项是封闭的，如果变量X在其中的每次出现都是一4H✚✚✙时间在µX操作员的范围内）。我们偶尔会使用以下派生构造：如果S ={P1，.，P k}是一组有限的过程，S代表P1H……HPk，同样对于你好。交织运算符表示空接口上的并行组合最后，我们通常用等式符号X= P来表示递归，而不是函数μX。P.举个例子，让我们定义一个过程VM，它打算用以下行为来建模自动售货机：最初，自动售货机在任何时候都愿意接受硬币。一旦硬币被投入机器，顾客可以选择订购巧克力或饼干;但是，如果他在60秒内没有做出选择，他的钱将被退回，自动售货机将恢复到初始状态。我们在下面将该自动售货机描述为定时CSP过程和定时自动机（参见图1）。第4节）。VM=coin.in−→阿利乔克choc−→VM✛❄✞✎ ✘biscuit✛, ✘快60了！coin.in≤60饼干−→VM货币（coin.out−→VM）重置x比特币，出局x=60？✚✙✙现在我们来描述一下这个扩展版本的Timed CSP的稠密时间指称语义;附录A中也给出了一致的操作语义。指称语义是Reed和Roscoe的定时故障模型[22，21，23，27]和拒绝测试[20]的混合一个时间事件是一个pair（t，a）∈R+×R。 （定时）事件集是定时事件的集合，并且还可以包括（t，time）形式的特殊定时事件，其中time是指示时间不能过去的符号。从现在开始我们abbreviate Σ {time}为我们还要求拒绝是时间-有界（与拒绝的定时事件相关联的时间集必须有界）。（定时）拒绝跟踪是一个序列，（t1，a1），（t2，a2），.。 ，（t k，a k），k(withk0），其中每个i是拒绝，并且每个（ti，ai）是定时事件，子条件是时间戳不递减。所有拒绝迹的集合被写为RT。我们将拒绝痕迹T解释为实验者与过程的相互作用的总结然而，在采取沉默行动时，不记录拒绝。时间本身的拒绝是通过，比如说，红灯的闪烁传达给实验者的。拒绝跟踪本质上是线性时间行为，封装了少量的分支时间信息。考虑的主要动机5RRR·−→P时间TT与简单的定时跟踪相反的是，后者不允许合成模型，如[21]所示定时CSP的一个显著特征是点非确定性现象，由此在发生静默转换（诸如超时）的精确时刻非确定性地启用或禁用不同的在[23]中详细讨论的点不确定性由于组合性原因自然出现在时间CSP模型中有趣的是，在目前的情况下，它的主要后果之一是，它允许密集时间的活性属性（如时间停止自由）的数字化分析，其他建模范式，如定时自动机，通常缺乏。我们将在第5节中回到这一点我 们 可 以 定 义 一 个 组 合 语 义 图： TCSP（ RT），它将每个进程P与其（密集时间）拒绝轨迹集相 关联P.这个映射也可以通过操作语义来描述，如附录A所示。我们也可以组成地定义P，过程P的积分时间拒绝迹的集合。一个拒绝跟踪是整数时间的，如果它的每个事件都有一个整数时间戳，并且如果它的每个拒绝都可以写为一个具有整数端点的拒绝令牌拒绝令牌是以下形式的集合[t，TJ]×A，（t，TJ]×A，[t，TJ）×A，orr（t，TJ）×A，其中ret，TJ∈R+是拒绝令牌，A拒绝令牌是在相应的interval.最后，我们用P和P分别表示P的稠密时间和积分时间迹集。3规范作为改进和验证我们考虑将过程的规范表示为精化（行为集的反向包含）以及验证这些规范的问题。 我们对跟踪细化（捕获安全属性：“没有不好的事情发生”）和拒绝跟踪细化（捕获安全性和活性：“好的事情不会阻止发生”）都感兴趣。请注意，活性对我们来说是一个分支时间概念，不同于Alpern和Schneider的相关线性时间定义[1]。后者可以用请注意，并不要求有关的实际行为必须发生;事实上，例如核威慑所提供的安全恰恰在于它不必使用。实时规范通常用一些时间逻辑来表示，例如MTL（线性时间）或TCTL（分支时间）[6]。关于德林的问题-6∈∈在[15]中研究了在不计时的情况下，关于这种逻辑的精炼的精确表达能力，并表明这是一个微妙的问题。时间的增加自然增加了困难。因此，对这个问题的全面处理是一个具有挑战性的主题，需要进一步的工作;尽管如此，我们在这里展示了许多（如果不是大多数的话）有趣的实时特性确实可以被捕获为定时CSP细化。实现PTCSP符合规范STCSP，如果P的所有行为也是S的行为。这导致了四种可能的满足定义，根据所考虑的行为是痕迹还是拒绝痕迹，以及根据时间是密集的还是离散的（积分）：PTS惠TPTSPTS惠TPTSPRS惠RP惠RSPRS惠RPRS.我们在下面提出了三个典型的线性时间安全规范（安全可达性，有界不变性和有界响应），并简要描述了它们如何被表示为时间CSP过程。我们还提出了两个范式分支时间活性规格（常数可用性和时间停止自由），同样表明它们被定时CSP过程捕获。为了简单起见，我们忽略了全局成功终止（C的通信）的可能性其中四个规范给出了相应的MTL或TCTL公式作为名称，但不需要或假设这些逻辑的知识安全可达性（<$a）：根据到[10]，这是定时系统上最常见的规范，因为 这是由进程RUN−{a}. HereRUNB={b−→RUNB|b∈B}。RUNB可以执行一个只包含B中事件的任意迹。缺点是，我不知道。Iability（ESTA）：“THE E VE E N T A IS NEVERREFRUSED.”’！过程sLIVE=RANDOM（H{b−→LIVE|b∈N}HTI MESTO P）a−→LIVE捕获了这种拒绝跟踪活性指定。时间停止自由（TSF）：的过程s TSF=RANDOM（H{a-→！TSF|a∈H}HSTOP）捕获拒绝跟踪活性指定。TSF是最不确定的过程没有时间停止。[12]列出了实践中最常见的两个规范;请注意，安全可达性本质上是有界不变性的特殊情况。有界不变性（（aI<$b））：7−−∈在时间间隔I期间防止事件b发生，时间间隔I是从a发生的时间开始测量的。这里I=（k，kJ）是一个长度至少为2的开区间，端点为整数（或无穷）此跟踪指定可以由包含2个[kkJ−k|+2平行进程。除了一个之外，所有这些都是发生时，设置两个闹钟，一个以k个时间单位振铃，指示应当禁用B 现在，如果在kJk个时间单位内发生了一秒a（使用单个时钟来跟踪该时间段），则刚刚描述的两个闹钟被简单地复位以在将来振铃kJ个单个离散控制器可轻松管理所有这些时钟。注意“报警环”是内部的全球隐藏（强）有界响应（（ajb））：发生，则事件b必须在时间间隔J内发生，如从a发生的时间测量的。这里J=[k，kJ]是具有整数端点的闭区间，并且k kJ或k=kJ= 0。一般来说，满足有界响应性质的最不确定的过程将处于有限状态（需要无限多个时钟）;然而，定义一个有限状态过程，它捕获了这个迹规范的积分这样的过程包括离散控制器以及kJ+ 1个时钟。同样，对于事件a的给定发生，闹钟被设置为在k个时间单位过去之后响铃这表明，事件B必须发生的时间段响铃后，时钟被重置为在kJk个时间单位后响铃，即在所讨论的时间段的最后。B否则，ab被发出信号（因此必须在现场发生当第二个警报响起的时候。这个过程只捕捉相应的有界响应性质的积分行为，这一事实对于验证目的是足够的，正如我们现在所证明的。我们采用数字化技术[12，16，17]作为验证过程符合其规范的一种手段（附录B简要介绍了数字化下面的定理，扩展了[16，17]的结果，是我们方法的核心：定理3.1任何P TCSP在拒绝迹（因此也是迹）数字化下是封闭的。命题3.2安全可达性、有界不变性和有界响应在逆迹数字化下是封闭的[12]。时停自由和恒定的可用性是封闭的逆拒绝跟踪数字化。推论3.3设P ∈ TCSP是TimedCSP过程. 然后PT<$a惠 P T<$a PRa惠P8RPRTSF优惠券TSFPT（aI<$b）惠PT（aI<$b）PT（aJb）惠PT（aJb）。右手边的离散检查都可以在模型检查器FDR上执行;详情请参见[16，17]。4封闭时间自动机我们定义了一类封闭的时间自动机。这些基本上是[13]中的时间安全自动机，具有完全封闭的不变量和使能约束。封闭约束的一个例子是x≤3，其中x是一个时钟，而不是x3。由于任何时间自动机都可以用具有封闭约束的时间自动机无限近似，因此这种限制在实践中似乎是相当良性的[7]）。这类时间自动机完全对应于由于Timed CSP的语义是基于有限行为的，因此我们必须放弃Bür和Dill为了简化我们的阐述，我们假设自动机不能成功终止（communicateC）。设C是一个有限的时钟集合，记为x，y，x1，x2等。|x≤c|XC|x1+ c1≤x2+c2|σ1∧σ2|σ1<$σ2定义C上的时钟约束集合F C。（这里c，c1，c2是非负整数。注意，所有的约束都是封闭的：在非负实数上解释它们总是在通常的拓扑中定义闭子集定义4.1封闭时间自动机是一个元组（tuple，S，S0，C，E，inv），其中• 字母表是一个有限的字母，• S是状态的有限集合，• S0S是一组起始状态，• C是一组有限的时钟，• E<$S×S×F × P（C） ×FC是一组跃迁，• inv：S−→F C指定状态不变约束。这类闭时间自动机记作CTA。时间自动机A的稠密时间拒绝迹语义A现在可以用标准的方法来定义了;我们把精确的细节放在附录C中。分别表示A的稠密时间迹、A的积分时间拒绝迹和A的积分时间拒绝迹的集合TA、RA和TA9R∈∈∈我A的迹线都以与定时CSP过程相同的方式从A导出5时间自动机作为时间CSP进程（以及返回）给定任意时间自动机ACTA，我们构造了两个对应的时间CSP过程PA和PA，分别捕获稠密时间和A.的积分-时间行为我们的构造使用了[9]中介绍的一些思想我们首先给出PA的构造。 设A =（S，S，S0，C，E，inv）是一个具有k个时钟x1，x2，.，x k C.我们构建PA作为k+ 2个进程的并行组合：k个进程的网络时钟，一个进程区域来模仿时钟区域图，以及一个进程控制器用于离散状态控制器。对于A的每个时钟xi C，设cxi是在A的使能和不变约束中与xi进行比较的最大常数。我们假设读者熟悉时钟区域构造[2，3]，其划分（R+）k（循环ks的值的空间）在k中！ ·2k·1k（2cx+2）或我更少的等价类。两种时钟解释存在不同的等价性类，如果它们在时钟xi的读数的整数部分中不同（并且这些数字之一小于cxi+1），或者如果它们在所有时钟的小数部分的顺序中不同每个等价类或时钟区域r被建模为过程REGr。REGr在任何时候都愿意接受，在一些内部（即，全局隐藏）通道，来自CONTROL的事件query.r;在进入新的离散状态时，CONTROL因此可以检查不变约束是否满意了。现在假设RJ是紧跟着r节奏的区域。(In在“极值”区域r的情况下区域进程REGr在任何时候都愿意再次在某个内部信道上接受命令（即，event）switch.rJ，其将控制转移到区域进程REGrJ。命令switch.rJ由CLOCKS发起，也需要CONTROL的参与，作为强制执行状态不变约束的手段一个区域进程在任何时候也愿意接受任何一个命令reset.xi，再次在某个内部通道上，并随后将控制转移到与通过复位xi到达的区域相关联的进程。最后，对于任何a∈R，区域过程REGr总是愿意接受虽然后一个通信是外部的（未隐藏），但随后的全局重命名操作将所有此类通信恢复为它们的标称值（在本例中为简单事件a）。复合时钟区域图形处理被表示为REGIONS。每个时钟xi由过程CLxi建模。此过程可以处于以下2个cx+2个状态中的任何一个（表示为R+的子集）：{0}，（0，1），{1}，（1，2），. ，（c xi − 1，c xi），{c xi}，（c xi，∞）. CLxi从一个状态切换到另一个状态10∈∈∈∈∈R通过中断操作符;它在有界的“间隔”状态下花费单位持续时间在进入一个新的状态之前，它将switch.r形式的所有事件的选择作为信号，其中r是与新状态中xi的值兼容的任何区域此外，对于r在时间上是“边界”区域的所有时钟CLxi还可以在任何时候（甚至在操作交换机时）接受命令reset.xi，该命令会提示跳转到state{0}。所有CLxi的并行组合任何时钟约束σ∈F C都可以用子集{r|rσ}时钟区域。每当自动机A在以下情况下传递事件a时，一个特定的时钟估值ν，过程PA是为了传达一种a，其中r是对应于v的区域。4回想一下，此事件随后在最外层重命名为a。离散控制器由过程控制建模，该过程控制模仿自动机S中的各种状态最初，CONTROLnondeterminis- tically开始在S0的开始状态之一。在进入一个新的状态s S时，CONTROL做的第一件事是向REGIONS 发送一个query.r形式的事件选择信号，其中rinv（s）。如果REGIONS无法在这些事件中的任何一个上同步，这意味着已经达到了一种状态，在这种状态下，约束被违反，时间停止自动终止。否则，当处于状态s时，离散控制器总是愿意接受以下形式的事件switch.r，只要r inv（s）。对于每个边e=（s，s， J，a，D，σ），CONTROL在处于状态s时，连续地选择该边的区域注释事件形式r. a，其中r σ.如果这些转换中的任何一个被接受，则CONTROL立即继续发送事件reset .x的信号，每个时钟xD都要被重置。最后，它进入新的状态SJ，服从于初始满足检查SJ控制，区域和时钟并行组合，并要求在所有适当的事件同步然后隐藏内部通道上的事件，最后，全局重命名运算符将所有形式为r. a的通信转换回它们的标称值。所得到的过程表示为PA。事实证明，PA与A具有完全相同的时间迹，但不完全相同的拒绝：由于点非决定性，每当A在开放时间间隔（t，TJ）上拒绝一组事件时，PA能够拒绝相同的集合在[t，t，J]上）。有趣的是，正是点非决定论使得定时CSP流程在拒绝跟踪数字化下关闭。关闭时间另一方面，自动机没有这个属性，从下面的时间自动机A可以看出[4]然而，由点非决定论引入的无穷小不确定性，需要注意的是，一个给定的时钟解释可能属于两个不同的区域，至少就PA而言。11·∈✖✕ ✖✕✖✕TT✲✗✔a✲✗x=0✔b✲✗✔重置xy ≤ 1 y2？很明显，如果第一次跃迁严格地发生在1和2之间的任何时间，那么A然而，请注意，A的积分拒绝迹线RA不显示任何时间停止。注意到这些现象后，Bo在[8]中指出，数字化技术似乎不足以处理时间停止自由的要求。 推论5.2表明情况并非如此（尽管我们的基于区域图的方法肯定不比[13]的算法更有效）。下面的结果确定了时间CSP的表达能力是一个不需要封闭时间d自动机的问题;定义了pe rato r ←（−）的“左闭包”附录C。Theorem5. 1F或A ∈ C T A上的ytimeddau toma t，RP A=<$R−−A−.特别地，PA= A。因此，封闭的时间自动机在迹数字化下是封闭的。推论5.2设CTA是一个时间自动机。 以下是等效的：(i) A是timestop-free（ARTS F）。(ii) PA是timestop-f ree（PA RTS F）。(iii) PA的内部回复率为最佳值（P ARTS F）。最后一个是可以在FDR上执行的离散检查一个合理的问题是，时间CSP是否比封闭的时间自动机更具表达力。由于时间CSP是图灵完备的，所以答案一定是肯定的;然而，我们发现，如果我们将自己限制在有限状态过程中，两种形式主义都是同样具有表达性的，如下所述。任何P∈TCSP都有一个相关联的标号转移系统，使用附录A的操作语义P的子标号转移系统是P的离散标号转移系统，其中所有的发展都有单位持续时间。我们说P是有限态的，如果它的离散标号转移系统是有限的。定理5.3设P ∈ TCSP为有限状态过程。 则存在闭时间自动机A∈CTA使得RP= RP A.这个定理显著地改进了Jackson [14]以前的一个结果，因为我们的 见前引书。，严格的句法限制被强加在定时CSP句法上，以便导出相应的（较弱的）结果。PA的构造，意在捕捉A的积分时间迹，与PA的构造非常相似。本质的区别在于REGIONS过程要粗糙得多（相应地，其他两个组件也是如此）：唯一考虑的时钟区域是{（j1，j2，.，j，k）}，即，积分12singletonsin（R+）k.不是区域的n个b是n1ik（cx+2）。我确保流程正常运行和强制满足不变和使能约束（对积分行为）是以明显的方式沿着PA的路线设计的。所得到的过程表示为PA。定理5.4对任意时间自动机A∈CTA，TPA= TA.这一结果的重要性来自于数字化技术对验证问题的适用性，详见第3节。我们的结论是，一般来说，它似乎并不总是有必要构建完整的区域图来捕捉给定的时间自动机的密集时间行为同样，即使对于离散行为，也不总是需要考虑每个晶格点。需要构造的最小图既取决于要检查的规范，也取决于自动机的不变约束和使能约束的集合如何构造最小离散控制器是一个值得深入研究的课题。6结论和今后的工作我们已经将（有限状态）定时CSP的精确表达能力描述为具有闭合不变量和启用时钟约束的闭合时间自动机-时间安全自动机[13]我们还证明了Timed CSP的表达能力足以将时间系统上一些最重要的规范作为精化来捕获;这些规范包括安全可达性、有界不变性和有界响应，以及时间停止自由和常数可用性的分支时间活性属性。我们已经建立了定时CSP过程在拒绝跟踪数字化下是封闭的[16，17]，并且由于上面列出的所有规范在逆（拒绝）跟踪数字化下都是封闭的，因此相应的验证问题离散化并且可以由模型检查器FDR处理。一些问题仍然悬而未决。一个是关于Timed CSP作为一种具体形式的表现力。按照[15]在非定时情况下的引导，精确地确定定量线性时间时间逻辑（如MTL）的哪个片段可以通过细化来捕获将是有趣另一个有趣的项目将是开发技术，以最大限度地减少捕获给定时间自动机的行为所需的离散状态的数量最后，虽然决定一个过程或时间自动机是否在逆数字化下是封闭的是不可判定的[18]，但设计一个简单的标准来保证逆数字化下的封闭性是非常有用的。除了上述研究课题外，我们还积极将研究成果应用于案例研究。13引用[1] B. Alpern和F. B.施耐德定义liveness。Information Processing Letters，21（4）：181[2] R.巴尔角Courcoubetis和D.迪尔实时系统的模型检查。在LICS 90会议记录中，第414IEEE Computer Society Press，1990.[3] R. 巴尔角Courcoubetis和D.迪尔密集实时的模型检查。信息与计算，104（1）：2[4] R. Alzheimer和D.迪尔时间自动机理论。理论计算机科学，126：183[5] R.巴尔湖Fix和T. A.亨辛格事件时钟自动机：一类可确定的时间自动机。理论计算机科学，211：253[6] R. Alzheimer和T.A. 亨辛格实时逻辑：复杂性和表现力。信息与计算，104（1）：35[7] E.阿萨林岛Maler，和A.普努埃利论时间自动机与数字电路中延迟的离散化。在Proceedings of CONCUR 98，第1466卷，第470-484页中。SpringerLNCS，1998年。[8] D. 我也是。数据的数字化。1999年，FMICS 99的出版物。[9] R. Chapman和M.戈德史密斯将定时器自动机转换为TCSP。正式系统设计与开发公司，一九九五年[10] E. M. Clarke，O. Grumberg和D. A.佩尔德。模型检查。麻省理工学院出版社，马萨诸塞州剑桥，1999年。[11] J·戴维斯实时系统中的规范和证明。牛津大学博士论文，1991年。[12] T. A. Henzinger，Z. Manna和A.普努埃利 数字时钟有什么用？在ICALP 92会议录，第623卷，第545-558页。Springer LNCS，1992年。[13] T. A. Henzinger，X. Nicollin，J. Sifakis和S. 尤文实时系统的符号模型信息与计算，111（2）：193[14] D. M. Jackson. 反应式软件系统的逻辑验证。牛津大学博士论文，1992年。[15] M. Leuschel，T. Massart和A.柯里如何制作FDR Spin：使用细化的LTL模型检查。在FME 01的会议记录，第2021卷，第99- 99118. Springer LNCS，2001年。[16] J. Ouaknine. 实时并发系统中连续行为的离散分析。博士论文，牛津大学，2001年。技术报告PRG-RR-01-06。14[17] J. Ouaknine.密集时间模型检验的数字化和完全抽象。在TACAS 02的会议记录中，第2280卷，第37Springer LNCS，2002年。[18] J. Ouaknine和J.B. 沃瑞尔时间自动机的一些可判定性和不可判定性结果。2002年提交。www.math.tulane.edu/www.example.com[19] Ouaknine和J.B.沃瑞尔作为定时系统的细化。在AVoCS 02的诉讼。伯明翰大学，2002年。[20] I. 菲利浦拒绝测试。Theoretical Computer Science，50（3）：241[21] G. M.里德实时分布式计算的数学理论。牛津大学博士论文，1988年。[22] G. M. Reed和A. W.罗斯科一种用于顺序进程通信的定时模型。在ICALP 86的会议记录中，第314-323页。Springer LNCS，1986年。理论计算机科学，58：249-261。[23] G. M. Reed和A. W.罗斯科 CSP的定时故障稳定性模型。理论计算机科学，211：85[24] S. A.施耐德实时系统中的正确性和通信。牛津大学博士论文，1989年。[25] S. A.施耐德将CSP与Z结合应用于矿用水泵的实例研究。未出版，1994年。[26] S. A.施耐德Timed CSP的操作语义。信息与计算，116：193[27] S. A.施耐德并发和实时系统：CSP方法。约翰·威利，2000年。A时间CSP操作语义本附录的内容和风格与[26]相似。我们提出了一个集合的推理规则，使我们能够分配给任何定时CSP进程的一组密集时间执行。为此，我们必须放松语法要求，即所有延迟（pa-参数n在项P1nP2、P1nP2）是整数，并允许任意非负实数（用t代替n）。这一扩大封闭项的集合写成TCSP。我们列出了一些符号约定：a和b代表可见事件，即，属于一个。 一个人和一个 = A{C}。 γ可以是可见的事件，也可以是无声的事件。一个（γ∈θ {τ}）。PγPJ表示闭项P可以执行一个即时和即时的n−t→一个γ跃迁，并随后成为PJγ（如果γ是可见事件，则在过程中传达γ）。 P−→意味着P不能提供任何特定时间的数据。P~tPJmeanstPcann当t∈R+时，PJ15τ一ττττ一一ττ111111221122112211221u1γ不γP~意味着P不能让严格正的时间流逝。在下文中，u∈R+。如果P是一个具有单个自由出现的X且Q是一个封闭项，则[Q/X]P表示封闭项P，其中Q代替X的每个自由出现。停止~t 停止（a−→P）~t（a−→P）（a−→P）−→a P（a−→！ P）−a→PSKIP~t 跳过跳过−→停止RANDOM−→ 等待WAITu~tWAIT（u−t）[t≤u]WAIT0−→τSKIPP~tPJ1utJu−t[t≤u]P1-P2-P1P2P−→PJP−→PJ0τuτJuaJP1→P2−→P2P1<$P2−→P1<$P2P1→P2−→P1P~tPJ1PutJu−t[t≤u]1P2~P1 P2PJ J1−→P10P1−→P1u[γ/=C]uτPJγJuP1→P2−→P21P2−→P1P1P2−→P1P2P~tPJP~tPJP P ~tPJPJ1 2P−→PJ1 2P−→PJP1<$P2−→P1J<$P2P1<$P2−→P1<$P2JP−→PJP−→PJP1→P2−→ P1JP1→P2−→P2JP1HP2−→P1P1HP2−→P2P~tPJP~tPJPP~PJPJPγJ1 21 2A AγJ1−→P1γ[γ∈/A]P2−→P2[γ∈/A]P PJ PPPPJ1A2−→1A2 1A2−→1A2τ一一16γττ时间z1我的天啊aJ J JJz2P1−→ P1JP2−→一P2J[a∈A]PP−→ PJPJP~tPJP1 212A AP PJPγPJ1 11−→不1−→1τ1−→1[γ/=C]P1P2~P1JP2P1P2−→P2P1P2−→P1JP2P~tPj∈A. P−a→P−→aPJP\A~tPJ\AP−γ →PJP\A−τ→PJ\A[a∈A]γP\A−→PJ\A[γ∈/A]P~tPJP−→PJP−→aPJP[R]~tPJ[R]）P[R]−τ→PJ[R]P[R]−→bPJ[R][aR b]µ X。P−τ→ [（µX. P）/X]P。请注意，TIMESTOP没有规则。对于P∈TCSP，我们定义P立即拒绝的事件集，ref（P），如下：如果P−→，则ref（P）=。否则，对于a∈ n，一a∈ref（P）惠P−→，时间∈ref（P）惠P~。 （回忆一下，时间是（不属于任何人的特殊对于P∈TCSP，我们将P的执行定义为一个方程e=P0−→P1−→. . .−z→nPn，其中P0γ=P和每个子序列Pzi+1i−→ Pi+1的e是不过渡P，−→Pi+1（其中zi+1=γ），或演化式Pi~Pi+1（其中zi+1=t）。此外，每一次转换或更新都是有效的这是上面列出的操作推理规则所允许的P的执行集写为exec（P）。LetT=0，（t1，a1）， . . . ，K=0，k . ，JUJl. 我们的定义它们的胶合TT =0，（t1，a1），.，（t k，k），k0，（t1，a1），.、L.运算符-与其他运算符-表示实现序列级联。如果T是伪迹并且t∈R+，则T+t是其中T的所有定时事件（观察到的和拒绝的）的时间戳增加了t的伪迹。给定某个进程P的一个执行e，我们产生一个相关的典型拒绝迹rt（e）（给定执行e的最大可能），在e上归纳定义如下。rt（P）=^{0} ×ref（P）rt（（P−τ→rt（（P−→a）-e）=^rt（e））-e）=^<${0} ×ref（P），（0，a）<$-rt（e）rt（（P~t）-e）=^f[0，t）×ref（P）<$a（rt（e） +t）.一一17·时间^阿吉吉我们定义了一个关于拒绝迹的偏序矩阵，它根据拒绝迹包含的信息量对拒绝如果T=0，（t1，a1），. ，K=0，k . ，nJl= 0，kl=0 aJi=aiJii。这个定义产生了一个算子↓：对于P是一组拒绝迹，↓P是最小的下闭算子集合包含P.全等定理如下：定理A.1对任意P∈TCSP，RP= ↓rt（exec（P））.B数字化数字化技术首先在[12]中引入，后来在[16，17]中从跟踪扩展到拒绝跟踪我们审查的要点，适应本框架。设t∈R+，且0≤ε≤1是整数. DE COMPOSETIN到其整数和小数部分，因此：t=[t+tJ。如果tJ<ε，令[t] ε=否则t[t]ε=^[t|.[t]，然后，我们可以通过逐点应用于跟踪事件的时间戳来将[·]ε然后，我们进一步将[]ε以通常的方式扩展到迹的集合LetAR+×是一种拒绝。 写A=i∈I{Ii×Ai}，其中每个+i是开、半开或闭区间，端点为ui，vi∈R得双曲正弦值.时间. 此外，假设这个表示是最大的，因为间隔Ii尽可能大我们将以[A]为中心，应用于区间Ii的端点ui，vi。自然，这以明显的方式将[·]ε扩展到拒绝迹，并因此扩展到拒绝迹的集合符号的重载不会引起混淆，因为[·]ε的参数是不相交的类型。定义B.1（拒绝）道的集合P在（拒绝）道数字化下是封闭的，如果对于任何0≤ε≤ 1，[P]ε<$P。一个（拒绝）迹集S在逆（拒绝）迹数字化是的，如果，每当（拒绝）迹s使得[s]ε∈S，对所有0≤ε≤ 1，则s∈S。对于P和S时间CSP过程，上述定义分别适用于TP（RP）和TS（RS）。如果P是一个（拒绝）迹集，我们让Z（P）表示P的整（拒绝）迹子集。主要验证结果如下：定理B.2设P是在（拒绝）迹数字化下闭合的（拒绝）迹的集合，并且设S是在逆（拒绝）迹数字化下闭合的（拒绝）迹的集合。则P<$S当且仅当Z（P）<$Z（S）。18−→时间- −∈∈∈^ ^您的位置：·时间{i}⊆ ×⊇000111000111nnnC封闭时间自动机语义我们假设时间自动机A=（S，S，S0，C，E，inv）∈CTA.我们以类似于[4，13]的方式定义A的拒绝迹集。一个闭合的时间是一个函数ν：CR+。Clockin解释允许我们以明显的方式将真值分配给时钟约束;我们写νσ来表示时钟解释ν使时钟约束。这是真的。对于ν：C−→R+aclocki的解释和t∈R+，其中ν+t是时钟解释，使得对所有x∈C，（ν+t）（x）=ν（x）+t.对于DC，一组要重置的时钟，我们让[resetD]v是时钟解释它将D中的时钟评估为0，并与D之外的时钟的ν一致。在v的解压缩中，给出了一个新的表达式，使得f（s，v）∈R+×R定义dasfollows：ifv$inv（s），nref（s，v）=^{0} ×nt ime.Otherwise，因为t∈R+且a∈R，welet（t，a）∈ref （s，v ）if，对于所有δ∈[0，t]，v+δ∈v（s），并且如果不存在s-起源的、a-标记的和σ-使能的跃迁e E（即，e =（s，，a，，σ）），其中v + t$σ。 最后，我们让（t，时间）ref（s，v）ift是最大的有限实数，其性质是，对于所有δ[0，t]，v+δinv（s）.A是一个有限序列ee=（s， t， v）−α→1 （s， t， v）−α→2.... . . 你 好