Abstract:
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 
-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
-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 modelAvailable as PostScript, PDF.