Communicating Timed Processes with Perfect Timed Channels

TL;DR

This paper introduces the model of communicating timed automata with perfect timed channels, analyzing the decidability of reachability problems under various configurations and establishing both undecidability and decidability results.

Contribution

It extends classical models to include timed automata with message ages, and provides new decidability and undecidability results for reachability in these models.

Findings

Reachability is undecidable with two automata and one unidirectional channel with global clocks.

Reachability remains undecidable with three automata and two channels without global clocks.

Reachability is decidable (EXPTIME) with two automata and one channel without global clocks.

Abstract

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.