Communicating Timed Automata: The More Synchronous, the More Difficult to Verify
Communicating Timed Automata: The More Synchronous, the More Difficult to Verify
复制标题
通信定时自动机：越同步，越难验证
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
W. Yi
中科院分区：
文献类型：
--
作者：
P. Krcál;W. Yi
我们研究了其行为(通过无限FIFO通道发送和接收消息)必须遵循指定本地组件的执行速度的给定时间约束的通道系统。我们提出用通信时间自动机(CTA)来建模这类系统。我们的目标是研究在定时设置下可判定和不可判定的渠道系统类别之间的界限。我们的技术结果包括：(1)(A1，A2，c1，2)形式的一个通道无共享状态的CTA等价于一台计数器机器，这意味着检查状态可达性和通道有界性等验证问题是可判定的；(2)(A1，A2，A3，c1，2，c2，3)形式的两个通道无共享状态的CTA具有图灵机的能力。请注意，在无计时设置中，这些系统并不比有限状态机更具表现力。这表明，准时同步的能力使得验证通道系统变得更加困难。
We study channel systems whose behaviour (sending and receiving messages via unbounded FIFO channels) must follow given timing constraints specifying the execution speeds of the local components. We propose Communicating Timed Automata (CTA) to model such systems. The goal is to study the borderline between decidable and undecidable classes of channel systems in the timed setting. Our technical results include: (1) CTA with one channel without shared states in the form (A1,A2, c1,2) is equivalent to one-counter machine, implying that verification problems such as checking state reachability and channel boundedness are decidable, and (2) CTA with two channels without sharing states in the form (A1,A2,A3, c1,2,c2,3) has the power of Turing machines. Note that in the untimed setting, these systems are no more expressive than finite state machines. This shows that the capability of synchronizing on time makes it substantially more difficult to verify channel systems.