Compositional Model Checking of Real Time Systems

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
[And95] 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.