Compositional Model Checking of Real Time Systems

Francois Laroussinie, Kim G. Larsen


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.

Full Text:


This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.

ISSN: 0909-0878 

Hosted by the Royal Danish Library and Aarhus University Library