|
Compositional Model Checking of Real Time Systems
François Laroussinie March 1995 |
Abstract:A major problem in applying model checking to finite-state systems is the potential combinatorial explosion of the state space arising from parallel composition. Solutions of this problem have been attempted for practical applications using a variety of techniques. Recent work by Andersen (Partial Model Checking. To appear in Proceedings of LICS '95) proposes a very promising compositional model checking technique, which has experimentally been shown to improve results obtained using Binary Decision Diagrams. In this paper we make Andersen's technique applicable to systems described by networks of timed automata. We present a quotient construction, which allows timed automata components to be gradually moved from the network expression into the specification. The intermediate specifications are kept small using minimization heuristics suggested by Andersen. The potential of the combined technique is demonstrated using a prototype implemented in CAML. Available as PostScript, PDF, DVI. |