Is your model checker on time? On the complexity of model checking for timed modal logics

This paper studies the structural complexity of model checking for several timed modal logics presented in the literature. More precisely, we consider (variations on) the specification formalisms used in the tools CMC and UPPAAL, and fragments of a timed mu-calculus. For each of the logics, we characterize the computational complexity of model checking, as well as its specification and program complexity, using (parallel compositions of) timed automata as our system model. In particular, we show that the complexity of model checking for a timed mu-calculus interpreted over (networks of) timed automata is EXPTIME-complete, no matter whether the complexity is measured with respect to the size of the specification, of the model or of both. All the flavours of model checking for timed versions of Hennessy-Milner logic, and the restricted fragments of the timed mu-calculus studied in the literature on CMC and UPPAAL, are shown to be PSPACE-complete or EXPTIME-complete. Amongst the complexity result, offered in the paper is a theorem to the effect that the model checking problem for the sublanguage L-s of the timed mu-calculus, proposed by Larsen, Pettersson and Yi, is PSPACE-complete. This result is accompanied by an array of statements showing that any extension of L-s has an EXPTIME-complete model checking problem. We also argue that the model checking problem for the timed propositional mu-calculus T-mu is EXPTIME-complete, thus improving upon results by Henzinger, Nicollin, Sifakis and Yovine, (C) 2002 Elsevier Science Inc. All rights reserved.