In and Out of WQOs - Model Checking of Parameterized Time Systems

Parosh Aziz Abdulla
Department of Infornation Technology, Uppsala University, Sweden
Tuesday, 24 February, 2004 (All day)

We show applications and limitations of the theory of well quasi-ordered programs, by analyzing different classes of parameterized timed systems.

We consider verification of safety properties for timed networks: systems consisting of an arbitrary set of identical timed processes. First, we show that checking safety properties is decidable in the case where each timed process is equipped with a single real-valued clock. Then, we consider multi-clock timed networks. We prove that the problem becomes undecidable when each process has two clocks. On the other hand, we show that the problem is decidable when clocks range over a discrete time domain. This decidability result holds when processes have any finite number of clocks.