Closed, Open, and Robust Timed Networks

We consider verification of safety properties for parameterized systems of timed processes, so called timed networks. A timed network consists of a finite state process, called a controller, and an arbitrary set of identical timed processes. In [Parosh Aziz Abdulla and Bengt Jonsson. Model checking of systems with many identical timed processes. Theoretical Computer Science, 290(1):241-264, 2003] it was shown that checking safety properties is decidable in the case where each timed process is equipped with a single real-valued clock. In [P. Abdulla, J. Deneux, and P. Mahata. Multi-clock timed networks. In Proc. LICS' 04, pages 345-354. IEEE Computer Society Press, 2004], we showed that this is no longer possible if each timed process is equipped with at least two real-valued clocks. In this paper, we study two subclasses of timed networks: closed and open timed networks. In closed timed networks, all clock constraints are non-strict, while in open timed networks, all clock constraints are strict (thus corresponds to syntactic removal of equality testing). We show that the problem becomes decidable for closed timed network, while it remains undecidable for open timed networks. We also consider robust semantics of timed networks by introducing timing fuzziness through semantic removal of equality testing. We show that the problem is undecidable both for closed and open timed networks under the robust semantics.