Abstract
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 Δp 2-complete model checking problem.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2–34, 1993.
R. Alur, T. Feder, and T. A. Henzinger. The benefits of relaxing punctuality. Journal of the ACM, 43(1):116–146, 1996.
R. Alur and T. A. Henzinger. Logics and models of real time: A survey. In Real-Time: Theory in Practice, Proc. REX Workshop, Mook, NL, June 1991, volume 600 of Lecture Notes in Computer Science, pages 74–106. Springer, 1992.
R. Alur and T. A. Henzinger. Real-time logics: Complexity and expressiveness. Information and Computation, 104(1):35–77, 1993.
R. Alur and T. A. Henzinger. A really temporal logic. Journal of the ACM, 41(1):181–203, 1994.
L. Aceto and F. Laroussinie. Is your model checker on time? In Proc. 24th Int. Symp. Math. Found. Comp. Sci. (MFCS’99), Szklarska Poreba, Poland, Sep. 1999, volume 1672 of Lecture Notes in Computer Science, pages 125–136. Springer, 1999.
R. Alur. Techniques for Automatic Verification of Real-Time Systems. PhD thesis, Stanford Univ., August 1991. Available as Tech. Report STAN-CS-91-1378.
E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.
T. H. Cormen, C. E. Leiserson, and R. L. Rivest. Introduction to algorithms. MIT Press, 1990.
C. Courcoubetis and M. Yannakakis. Minimum and maximum delay problems in real-time systems. Formal Methods in System Design, 1(4):385–415, 1992.
E. A. Emerson and Chin-Laung Lei. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming, 8(3):275–306, 1987.
E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, vol. B, chapter 16, pages 995–1072. Elsevier Science, 1990.
E. A. Emerson, A. K. Mok, A. P. Sistla, and J. Srinivasan. Quantitative temporal reasoning. Real-Time Systems, 4(4):331–352, 1992.
E. A. Emerson and R. J. Trefler. Generalized quantitative temporal reasoning: An automata-theoretic approach. In Proc. 7th Int. Joint Conf. Theory and Practice of Software Development (TAPSOFT’97), Lille, France, Apr. 1997, volume 1214 of Lecture Notes in Computer Science, pages 189–200. Springer, 1997.
E. A. Emerson and R. J. Trefler. Parametric quantitative temporal reasoning. In Proc. 14th IEEE Symp. Logic in Computer Science (LICS’99), Trento, Italy, July 1999, pages 336–343. IEEE Comp. Soc. Press, 1999.
M. R. Garey and D. S. Johnson. Computers and Intractability. A Guide to the Theory of NP-Completeness. Freeman, 1979.
T. A. Henzinger. It’s about time: real-time logics reviewed. In Proc. 9th Int. Conf. Concurrency Theory (CONCUR’98), Nice, France, Sep. 1998, volume 1466 of Lecture Notes in Computer Science, pages 439–454. Springer, 1998.
M. W. Krentel. The complexity of optimization problems. Journal of Computer and System Sciences, 36(3):490–509, 1988.
H. R. Lewis. A logic of concrete time intervals (extended abstract). In Proc. 5th IEEE Symp. Logic in Computer Science (LICS’90), Philadelphia, PA, USA, June 1990, pages 380–389. IEEE Comp. Soc. Press, 1990.
F. Laroussinie, N. Markey, and Ph. Schnoebelen. Model checking CTL+ and FCTL is hard. In Proc. 4th Int. Conf. Foundations of Software Science and Computation Structures (FOSSACS’2001), Genova, Italy, Apr. 2001, volume 2030 of Lecture Notes in Computer Science, pages 318–331. Springer, 2001.
F. Laroussinie, Ph. Schnoebelen, and M. Turuani. On the expressivity and complexity of quantitative branching-time temporal logics. In Proc. 4th Latin American Symposium on Theoretical Informatics (LATIN’2000), Punta del Este, Uruguay, Apr. 2000, volume 1776 of Lecture Notes in Computer Science, pages 437–446. Springer, 2000.
J. S. Ostroff. Deciding properties of timed transition models. IEEE Transactions on Parallel and Distributed Systems, 1(2):170–183, 1990.
C. H. Papadimitriou. On the complexity of unique solutions. Journal of the ACM, 31(2):392–400, 1984.
C. H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.
L. J. Stockmeyer. The polynomial-time hierarchy. Theoretical Computer Science, 3(1):1–22, 1976.
K. W. Wagner. More complicated questions about maxima and minima, and some closures of NP. Theoretical Computer Science, 51(1–2):53–80, 1987.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Laroussinie, F., Markey, N., Schnoebelen, P. (2002). On Model Checking Durational Kripke Structures. In: Nielsen, M., Engberg, U. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2002. Lecture Notes in Computer Science, vol 2303. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45931-6_19
Download citation
DOI: https://doi.org/10.1007/3-540-45931-6_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43366-8
Online ISBN: 978-3-540-45931-6
eBook Packages: Springer Book Archive