On model checking durational Kripke structures

F. Laroussinie and N. Markey and Ph. Schnoebelen

To appear at Foundations of Software Science and Computation Structures (FOSSACS02), Grenoble, France, 6-14 April, 2002


We consider quantitative model checking in durational Kripke structures (Kripke structures where transitions have integer durations) with timed temporal logics where subscripts put quantitative constraints on the time it takes before a property is satisfied. We investigate the conditions that allow polynomial-time model checking algorithms for timed versions of CTL and exhibit an important gap between logics where subscripts of the form ``=c'' (exact duration) are allowed, and simpler logics that only allow subscripts of the form ``<=c'' or ``>=c'' (bounded duration). A surprising outcome of this study is that it provides the second example of a Delta_2^p-complete model checking problem.

Server START Conference Manager
Update Time 14 Dec 2001 at 14:02:38
Maintainer fossacs02@brics.dk.
Start Conference Manager
Conference Systems