Distributed Interval Automata: A Subclass of Timed Automata.

Deepak D'Souza and P. S. Thiagarajan

Report TCS-98-3, Chennai Mathematical Institute, Chennai, INDIA.

We identify a subclass of timed automata and develop its theory. These automata, called distributed interval automata, consist of a network of timed agents. The key restriction is that there is just one clock for each agent and the way the clocks are read and reset is determined by the distribution of shared actions across the agents. We show that the resulting automata admit a clean theory in both logical and language theoretic terms. We also establish decidability of the timed language inclusion and reachability problems for a related class of hybrid systems. It turns out that the study of distributed interval automata can exploit the rich theory of partial orders known as Mazurkiewicz traces. A likely consequence is that the partial order reduction techniques available in the untimed case can be applied to the verification tasks associated with our automata. Indeed this is the case with the recently proposed technique due to Bengtsson et. al. [BJLW98].