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 Δp2 -complete model checking problem.
CITATION STYLE
Laroussinie, F., Markey, N., & Schnoebelen, P. (2002). On model checking durational kripke structures. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2303, pp. 264–279). Springer Verlag. https://doi.org/10.1007/3-540-45931-6_19
Mendeley helps you to discover research relevant for your work.