Reachability of Communicating Timed Processes
Reachability of Communicating Timed Processes
复制标题
通信定时进程的可达性
DOI：
10.1007/978-3-642-37075-5_6
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
G. Sutre
中科院分区：
文献类型：
--
作者：
Lorenzo Clemente;F. Herbreteau;Amélie Stainer;G. Sutre
我们研究了离散时间和稠密时间下传递时间过程的可达性问题。我们的模型包括在无限FIFO通道上进行通信的具有局部时间约束的自动机。每个自动机只能访问其本地时钟集；所有时钟都以相同的速度进化。我们的主要贡献是完全刻画了离散和密集时间的可判定和不可判定通信拓扑。我们还得到了复杂性结果，证明了通信时滞过程至少和Petri网一样难；在离散时间，我们还证明了与Petri网的等价性。我们的结果源于时间自动机和(非时间)反自动机之间的相互拓扑保持约简。为了说明接收的紧迫性，我们还调查了进程可以测试通道空闲的情况。
We study the reachability problem for communicating timed processes, both in discrete and dense time. Our model comprises automata with local timing constraints communicating over unbounded FIFO channels. Each automaton can only access its set of local clocks; all clocks evolve at the same rate. Our main contribution is a complete characterization of decidable and undecidable communication topologies, for both discrete and dense time. We also obtain complexity results, by showing that communicating timed processes are at least as hard as Petri nets; in the discrete time, we also show equivalence with Petri nets. Our results follow from mutual topology-preserving reductions between timed automata and (untimed) counter automata. To account for urgency of receptions, we also investigate the case where processes can test emptiness of channels.