15 February 2005 Model Checking Temporal Logics Along Selected Computation Paths
Nicolas Markey and Jean-François Raskin had a very interesting paper accepted at CONCUR'04 on Model Checking Restricted Sets of Timed Paths. That paper continues the study of model checking problems for temporal logics over restricted sets of paths begun by Markey and Philippe Schnoebelen in their CONCUR 2003 paper Model Checking a Path (Preliminary Report).
The focus is now on studying the complexity of the model checking problems for four real-time logics (TPTL, MTL, MITL and TCTL) over finite or ultimately periodic sets of timed paths in timed automata. In particular, the authors consider "concrete" single paths, and symbolic paths in the region or zone graph associated with a timed automaton.
This paper studies an interesting and natural problem, viz. how the complexity of model checking problems for some standard real-time logics is affected by restricting the models to specific sets of paths of timed automata. It does so in a very thorough fashion by providing an exhaustive map of the terrain, and a wealth of instructive results with technically challenging proofs. As such, I believe that it will be an important reference for researchers interested in the theory of real-time systems and in model checking in general.
The results offered by Markey and Raskin fall naturally into two classes, viz. those with a negative and those with a positive flavour. The negative results show that some of the model checking problems studied in this work are, perhaps surprisingly, just as hard for restricted sets of timed paths as for timed automata. I found these results fascinating, and their proofs highly non-trivial. Two of those theorems show that the model checking problems for MTL and MITL over an ultimately periodic region path are undecidable and EXPSPACE-complete, respectively. Even though the proof methodology used in establishing those results is standard (viz. encoding of Turing machine computations as model checking problems), the actual details require a high degree of ingenuity, and are non-trivial. Another result I'd like to single out is a theorem to the effect that model checking TPTL formulae over a single finite concrete path is PSPACE-hard. The authors suggest that this result means that TPTL is not really usable as a specification formalism to be used in algorithmic verification of real-time systems. I agree, but, as witnessed by the relative success of the MONA verification tool, sometimes practice does not agree with structural complexity results.
Amongst the positive results presented by the authors, I was most impressed by a theorem to the effect that, in contrast to the negative results for MTL and MITL, the model checking for TCTL is in P when restricted to ultimately periodic region paths. The proof of this result uses a fairly standard labelling algorithm, but requires a very careful, and technically non-trivial, analysis of the temporal relations between regions.
As should be clear from the above discussion, I recommend this paper to my readers. I would have been extremely proud of having achieved some of the results in the paper myself.
I met Nicolas Markey for the first time during a one month stay at ENS Cachan in May 1998. I am happy to see that his career is going from strength to strength. Indeed, at least to my mind, LSV hosts now one of the strongest research groups in concurrency in Europe.
Last modified: Tuesday, 15-Feb-2005 10:14:15 CET.