Cited By
View all- Basin DKlaedtke FZălinescu E(2019)Runtime Verification over Out-of-order StreamsACM Transactions on Computational Logic10.1145/335560921:1(1-43)Online publication date: 4-Oct-2019
LTL generalized model checking revisited
Pages 571 - 584
Abstract
Given a 3-valued abstraction of a program (possibly generated using static program analysis and predicate abstraction) and a temporal logic formula, generalized model checking (GMC) checks whether there exists a concretization of that abstraction that satisfies the formula. In this paper, we revisit generalized model checking for linear time (LTL) properties. First, we show that LTL GMC is 2EXPTIME-complete in the size of the formula and polynomial in the model, where the degree of the polynomial depends on the formula, instead of EXPTIME-complete and quadratic as previously believed. The standard definition of GMC depends on a definition of concretization which is tailored for branching-time model checking. We then study a simpler linear completeness preorder for relating program abstractions. We show that LTL GMC with this weaker preorder is only EXPSPACE-complete in the size of the formula, and can be solved in linear time and logarithmic space in the size of the model. Finally, we identify classes of formulas for which the model complexity of standard GMC is reduced.
References
[1]
Antonik, A., Huth, M., Larsen, K., Nyman, U., Wasowski, A.: 20 years of mixed and modal specifications. Bulletin of the European Association for Theoretical Computer Science (2008)
[2]
Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: IFAC Symp. on System Structure and Control, pp. 469---474. Elsevier, Amsterdam (1998)
[3]
Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: 11th Computer Aided Verification, pp. 274---287 (1999)
[4]
Bruns, G., Godefroid, P.: Generalized model checking: Reasoning about partial state spaces. In: 11th Concurrency Theory. Lecture Notes in Computer Science, vol. 1877, pp. 168---182 (2000)
[5]
Ball, T., Rajamani, S.: The SLAM Toolkit. In: 13th Computer Aided Verification. Lecture Notes in Computer Science, vol. 2102, pp. 260---264, Springer, Paris (2001)
[6]
Gurfinkel, A., Chechik, M.: How thorough is thorough enough? In: 13th Correct Hardware Design and Verification Methods (2005)
[7]
Godefroid, P., Huth, M.: Model checking vs. generalized model checking: semantic minimizations for temporal logics. In: 20th Logic in Computer Science, pp. 158---167, Chicago, June (2005)
[8]
Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: 12th Concurrency Theory. Lecture Notes in Computer Science, vol. 2154, pp. 426---440. Springer, Aalborg (2001)
[9]
Godefroid, P., Jagadeesan, R.: Automatic abstraction using generalized model checking. In: 14th Computer Aided Verification. Lecture Notes in Computer Science, vol. 2404, pp. 137---150. Springer, Berlin (2002)
[10]
Godefroid, P., Jagadeesan, R.: On the Expressiveness of 3-valued models. In: 4th Verification, Model Checking and Abstract Interpretation. Lecture Notes in Computer Science, vol. 2575, pp. 206---222. Springer, New York (2003)
[11]
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: 9th Computer Aided Verification. Lecture Notes in Computer Science, vol. 1254, pp. 72---83. Springer, Haifa (1997)
[12]
Grädel, E., Thomas, W., Wilke, T.: Automata, Logics, and Infinite Games. Lecture Notes in Computer Science, vol. 2500. Springer, Berlin (2002)
[13]
Gurfinkel, A., Wei, O., Chechik, M.: Systematic construction of abstractions for model-checking. In: 7th Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 3855, pp. 381---397. Springer, Berlin (2006)
[14]
Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: 29th Principles of Programming Languages, pp. 58---70 (2002)
[15]
Huth, M., Jagadeesan, R., Schmidt, D.: Modal transition systems: a foundation for three-valued program analysis. In: 10th European Symp. on Programming. Lecture Notes in Computer Science, vol. 2028. Springer, Berlin (2001)
[16]
Jurdziński, M.: Small progress measures for solving parity games. In: 17th Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 1770, pp. 290---301. Springer, Berlin (2000)
[17]
Kleene S.C.: Introduction to Metamathematics. North Holland, Amsterdam (1987)
[18]
Kupferman, O., Morgenstern, G., Murano, A.: Typeness for ?-regular automata. In: 2nd Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 3299, pp. 324---338. Springer, Berlin (2004)
[19]
Kesten, Y., Piterman, N., Pnueli, A.: Bridging the gap between fair simulation and trace containment. In: 15th Computer Aided Verification. Lecture Notes in Computer Science, vol. 2725, pp. 381---393. Springer, Berlin (2003)
[20]
Kupferman O., Vardi M.Y., Wolper P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312---360 (2000)
[21]
Larsen, K.G., Thomsen, B.: A modal process logic. In: 3rd Logic in Computer Science, pp. 203---210 (1988)
[22]
Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: 9th Symposium on Principles of Distributed Computing, pp. 377---410. ACM, New York (1990)
[23]
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Berlin (1992)
[24]
Piterman N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. Logical Methods Comput. Sci. 3(3), 5 (2007)
[25]
Piterman, N., Pnueli, A., Saar, Y.: Synthesis of reactive(1) designs. In: 7th Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 3855, pp. 364---380. Springer, Berlin (2006)
[26]
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: 16th Principles of Programming Languages, pp. 179---190 (1989)
[27]
Ramadge P.J.G., Wonham W.M.: The control of discrete event systems. IEEE Trans. Control Theory 77, 81---98 (1989)
[28]
Safra, S.: On the complexity of ?-automata. In: 29th Foundations of Computer Science, pp. 319---327, White Plains, October (1988)
[29]
Sistla A.P., Vardi M.Y., Wolper P.: The complementation problem for Büchi automata with applications to temporal logic. Theor. Comput. Sci. 49, 217---237 (1987)
[30]
van Emde Boas, P.: The convenience of tilings. In: Complexity, Logic and Recursion Theory. Lecture Notes in Pure and Applied Mathetaics, vol. 187, pp. 331---363 (1997)
[31]
Vardi M.Y., Wolper P.: Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci. 32(2), 182---221 (1986)
[32]
Vardi M.Y., Wolper P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1---37 (1994)
- LTL generalized model checking revisited
Recommendations
LTL Generalized Model Checking Revisited
VMCAI '09: Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract InterpretationGiven a 3-valued abstraction of a program (possibly generated using static program analysis and predicate abstraction) and a temporal logic formula, generalized model checking (GMC) checks whether there exists a concretization of that abstraction that ...
Bounded model checking of high-integrity software
HILT '13: Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technologyModel checking [5] is an automated algorithmic technique for exhaustive verification of systems, described as finite state machines, against temporal logic [9] specifications. It has been used successfully to verify hardware at an industrial scale [6]. ...
Another Look at LTL Model Checking
We show how LTL model checking can be reduced to CTL model checking with fairness constraints. Using this reduction, we also describe how to construct a {\em symbolic} LTL model checker that appears to be quite efficient in practice. In particular, we ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Copyright © 2011 Springer-Verlag.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 01 November 2011
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 24 Sep 2024
Other Metrics
Citations
Cited By
View all- Basin DKlaedtke FZălinescu E(2019)Runtime Verification over Out-of-order StreamsACM Transactions on Computational Logic10.1145/335560921:1(1-43)Online publication date: 4-Oct-2019
View Options
View options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in