Is your Model Checker on Time?
On the Complexity of Model Checking for Timed Modal Logics

Luca Aceto
François Laroussinie

October 1999


This paper studies the structural complexity of model checking for (variations on) the specification formalisms used in the tools CMC and UPPAAL, and fragments of a timed alternation-free $\mu$-calculus. For each of the logics we study, we characterize the computational complexity of model checking, as well as its specification and program complexity, using timed automata as our system model

Available as PostScript, PDF.


Last modified: 2003-06-08 by webmaster.