进程代数中关于超时的分析及建模

理论计算机科学电子笔记162（2006）173-175www.elsevier.com/locate/entcs关于超时1Rob van Glabbeek2澳大利亚国家信息通信技术新南威尔士地址：Locked Bag 6016，Sydney，NSW 1466，Australia摘要本文提出了如何在进程代数中指定超时的问题，并发现基本的形式主义在这项任务中是不够的。关键词：并发，进程代数，活性，公平，超时，优先级，Petri网。考虑以下邮件服务器协议：设置一个定时器，设定一个未指定但有限的时间，并尝试一次又一次地发送在后一种情况下，返回错误消息。可选地，有人可以在计时器关闭之前将其停用，在这种情况下，系统可能永远运行我的问题是如何通过进程代数来建模这个简单的协议。尽管CCS、CSP和ACP等语言及其许多变体已经存在了25年，但要做到这一点仍然特别困难。由于这个问题没有指定任何实时约束，因此使用实时进程代数似乎不太自然。具体说明应该完全开放每个活动持续多长时间。特别是，在计时器关闭之前进行的试验次数没有上限。我们仍然知道，在有限的时间内，除非定时器被停用，否则消息要么成功发送，要么返回错误消息当从定时器中部分抽象时，该过程可以指定为set·μX。（失败·X+成功+超时·错误）整个协议的规范（自由混合ACCSP）可以是1部分依据与Frits Vaandrager的联合工作。2电子邮件：rvg@cs.stanford.edu1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.083174河van Glabbeek/Electronic Notes in Theoretical Computer Science 162（2006）173设置·.μX。（fail·X+fac+timeout·error）超时！τ·超时+停用。然而，这种规范留下了一个选项，即流程永远失败：ACCSP的标准操作语义生成了一个转换系统，其特征是一个具有无限多个失败操作且没有停用的路径（参见图1）。失败失败τ超时误差设置成功成功deact。τ失败deact。成功Fig. 1. ACCSP规范一个解决方案是调用Koomen然而，这取决于全局公平性假设，在这个例子中没有得到保证 即使动作停用发生，KFAR允许我们推导出，与规范相反，成功最终会发生。这里似乎需要某种优先级机制，即当超时发生时，它优先于替代操作失败和成功。当通过重命名为静默步骤来执行抽象时，优先级机制在进程代数中是麻烦的，因为在弱互模拟和分支互模拟语义中，（τ. （b+c）+b）和a（b+c）是等价的，但是如果c优先于b，则可以预期只有前者可以执行b-步骤。即使当优先级机制就位时，由于并行组合中的组件的交错，图1的过程仍然允许无限序列的失败动作而不停用也许可以通过将规范建模为Petri网来找到一个优雅的解决方案-参见图2。在正常的进度假设下，假设没有停用发生，迟早会有一个令牌在q位置。现在，timeout应该优先于竞争p中的token的操作fail和succeed，但是这个优先级只有在q中有token时才有效。如何最好地形式化这种推理建议作为未来研究的主题。QτR. van Glabbeek/Electronic Notes in Theoretical Computer Science 162（2006）173-175175引用图二. ACCSP规范[1] JCM Baeten，J.A. Bergstra J.W. Klop（1987）：关于Koomen公平抽象规则的一致性。理论计算机科学51（1/2），pp。129-176。设置·成功失败p误差超时deact。