zbMATH — the first resource for mathematics

On model checking durational Kripke structures. (English) Zbl 1077.68691
Nielsen, Mogens (ed.) et al., Foundations of software science and computation structures. 5th international conference, FOSSACS 2002, held as part of the joint European conferences on theory and practice of software, ETAPS 2002, Grenoble, France, April 8–12, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43366-X). Lect. Notes Comput. Sci. 2303, 264-279 (2002).
Summary: 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 “\(\leq c\)” or “\(\geq c\)” (bounded duration).
A surprising outcome of this study is that it provides the second example of a \(\Delta^p_2\)-complete model checking problem.
For the entire collection see [Zbl 0989.00051].

68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: Link