What is Decidable about Perfect Timed Channels?
What is Decidable about Perfect Timed Channels?
复制标题
完美定时频道的可判定性是什么？
DOI：
10.1007/978-3-662-44584-6_28
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
S. Krishna
中科院分区：
文献类型：
--
作者：
P. Abdulla;M. Atig;S. Krishna
本文介绍了通信时间自动机(CTA)模型，该模型扩展了有限状态过程通过FIFO完全通道和时间自动机进行通信的经典模型，即用时间自动机代替有限状态过程，并在理想通道内的消息配备代表其年龄的时钟。除了时间自动机的标准操作外，每个自动机可以(1)将消息附加到具有初始年龄的信道的尾部，或者(2)如果年龄满足一组给定的约束，则在信道的头部接收消息。在这篇文章中，我们证明了即使在两个由一个单向定时通道连接的时间自动机的情况下，如果其中一个允许全局时钟(两个自动机可以检查和操纵)，可达性问题也是不可判定的。我们证明了，即使对于由三个时间自动机和两个单向定时通道组成的CTA(并且没有任何全局时钟)，这种不可判断性仍然成立。然而，在两个自动机与一个单向定时通道链接并且没有全局时钟的情况下，可达性问题变得可判定。最后，我们考虑了有界上下文的情况，在每个上下文中，只允许一个时间自动机从一个通道接收消息，同时能够向所有其他时间通道发送消息。在这种情况下，我们证明了可达性问题是可判定的。
In this paper, we introduce the model of communicating timed automata (CTA) that extends the classical models of finite-state processes communicating through FIFO perfect channels and timed automata, in the sense that the finite-state processes are replaced by timed automata, and messages inside the perfect channels are equipped with clocks representing their ages. In addition to the standard operations of timed automaton, each automaton can either (1) append a message to the tail of a channel with an initial age or (2) receive the message at the head of a channel if it is age satisfies a set of given constraints. In this paper, we show that the reachability problem is undecidable even in the case of two timed automata connected by one unidirectional timed channel if one allows global clocks (that the two automata can check and manipulate). We prove that this undecidability still holds even for an CTA consisting of three timed automata and two unidirectional timed channels (and without any global clock). However, the reachability problem becomes decidable in the case of two automata linked with one unidirectional timed channel and with no global clock. Finally, we consider the bounded-context case, where in each context only one timed automaton is allowed to receive messages from one channel while being able to send messages to all the other timed channels. In this case we show that the reachability problem is decidable.