Verification of programs with half-duplex communication
Verification of programs with half-duplex communication
复制标题
DOI：
10.1016/j.ic.2005.05.006
复制
发表时间：
2005-11-01
影响因子：
1
通讯作者：
Finkel, A
中科院分区：
文献类型：
--
作者：
Cécé, G;Finkel, A
我们考虑分析无限半双工系统的有限状态机，在无界信道上进行通信。两台机器和两个通道（每个方向一个）的半双工属性表示每个可达配置最多有一个非空通道。本文证明了这样的半双工系统有一个可识别的可达集。我们将展示如何计算，在多项式时间内，这个可达集的符号表示，以及如何使用该描述来解决几个验证问题。此外，虽然通信有限状态机的模型是图灵强大的，我们证明了半双工系统类的成员资格是可判定的。不幸的是，对两台以上机器的系统的自然推广是图灵强大的。我们还证明了这些系统对PLTL（命题线性时态逻辑）或CTL（计算树逻辑）的模型检查是不可判定的。最后，我们展示了如何将先前的可判定性结果应用于正则模型检测。我们提出了一个新的加速符号可达半算法，它成功地终止于两台机器的半双工系统和一些有趣的非半双工系统。(c)2005年爱思唯尔公司All rights reserved.
We consider the analysis of infinite half-duplex systems made of finite state machines that communicate over unbounded channels. The half-duplex property for two machines and two channels (one in each direction) says that each reachable configuration has at most one channel non-empty. We prove in this paper that such half-duplex systems have a recognizable reachability set. We show how to compute, in polynomial time, a symbolic representation of this reachability set and how to use that description to solve several verification problems. Furthermore, though the model of communicating finite state machines is Turing-powerful, we prove that membership of the class of half-duplex systems is decidable. Unfortunately, the natural generalization to systems with more than two machines is Turing-powerful. We also prove that the model-checking of those systems against PLTL (propositional linear temporal logic) or CTL (computational tree logic) is undecidable. Finally, we show how to apply the previous decidability results to the Regular Model Checking. We propose a new symbolic reachability semi-algorithm with accelerations which successfully terminates on half-duplex systems of two machines and some interesting non-half-duplex systems. (c) 2005 Elsevier Inc. All rights reserved.