Decidability of timed language-inclusion for networks of real-time communicating sequential processes

An important verification problem for concurrent systems in general is that of establishing whether one system is a correct implementation, or refinement, of another system. For untimed systems, trace inclusion (or variants such as failure inclusion) is often used as a criterion of refinement. The natural extension of this criterion to timed systems is timed trace-inclusion. Unfortunately, this problem is undecidable for the commonly used model of timed automata (i.e. finite-state automata extended with clocks) due to the expressive power of the model. This is a serious obstacle to the application of automatic verification methods to timed automata. In this paper, we show that the problem of timed trace-inclusion is decidable for a large and natural class of processes in Reed and Roscoe’s Timed CSP [RR86]. Essentially, this class includes static networks of processes with finite-control structure and real-valued clocks (modelled implicitly by a delay operator).