Partial orders and verification of real-time systems

We show in this paper how the verification method of timed graphs ([1], [6]) can be substantially improved by the use of a partial-order technique. In [5] and [4] is presented an efficient model-checking algorithm for concurrent systems that avoids most of the state explosion due to the modeling of concurrency by interleaving. We adapt this work to timed graphs, by defining a dependency relation on transitions and an equivalence on executions, taking into account quantitative aspects of time. We then propose a selective search algorithm that computes a reduced accessibility graph, in the framework of deadlock detection.