用完美的定时通道沟通定时流程
Communicating Timed Processes with Perfect Timed Channels
摘要：
我们引入了通信时间自动机（CTA）的模型，扩展了经典的有限状态进程通过FIFO完美通道和时间自动机进行通信的模型，在这个意义上，有限状态进程被时间自动机所取代，完美通道内的消息配备有代表其年龄的时钟。除了标准操作（重置时钟，检查时钟的保护），每个自动机可以（1）将消息附加到具有初始年龄的通道的尾部，或者（2）如果其年龄满足一组给定的约束，则在通道的头部接收消息。在本文中，我们表明，可达性问题是不可判定的，即使在两个时间自动机连接一个单向定时通道的情况下，如果允许全球时钟（这两个自动机可以检查和操纵）。我们证明了这种不可判定性仍然成立，即使CTA由三个定时自动机和两个单向定时通道（没有任何全局时钟）。然而，可达性问题变得可判定（在$\mathsf{EXPTIME}$）的情况下，两个自动机链接一个单向定时通道，没有全局时钟。最后，我们考虑有界上下文的情况下，在每个上下文中，只有一个定时自动机被允许从一个通道接收消息，同时能够发送消息到所有其他定时通道。在这种情况下，我们证明了可达性问题是可判定的。
英文摘要：
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 (resetting clocks, checking guards of clocks) 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 its 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 CTA consisting of three timed automata and two unidirectional timed channels (and without any global clock). However, the reachability problem becomes decidable (in $\mathsf{EXPTIME}$) 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
