Advertisement

Variants of LTL Query Checking

  • Hana Chockler
  • Arie Gurfinkel
  • Ofer Strichman
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6504)

Abstract

Given a model M and a temporal logic formula ϕ[?], where ? is a placeholder, the query checking problem, as defined for the case of CTL by Chan in 2000, is to find the strongest propositional formula f such that M ⊧ ϕ[? ←f]. The motivation for solving this problem is, among other things, to get insight on the model.

We consider various objectives to the LTL query-checking problem, and study the question of whether there is a better solution than simply enumerating all possible formulas (modulo logical equivalence). It turns out that in most cases the answer is no, but there is one particular objective for which the answer – in practice – is definitely yes. The solution is based on a reduction to a Pseudo-Boolean Solving problem.

Keywords

Model Check Temporal Logic Propositional Formula Kripke Structure Temporal Logic Formula 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Aloul, F.A., Ramani, A., Markov, I.L., Saka llah, K.A.: PBS: A Backtrack-Search Psuedo-Boolean Solver and Optimizer. In: Fifth International Symposium on the Theory and Applications of Satisfiability Testing, SAT (2002)Google Scholar
  2. 2.
    Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 279–290. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  3. 3.
    Bruns, G., Godefroid, P.: Temporal logic query checking. In: LICS, pp. 409–417 (2001)Google Scholar
  4. 4.
    Chaki, S., Strichman, O.: Three optimizations for assume-guarantee reasoning with L*. J. on Formal Methods in System Design 32(3), 267–284 (2008)CrossRefzbMATHGoogle Scholar
  5. 5.
    Chan, W.: Temporal-Logic Queries. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 450–463. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  6. 6.
    Chechik, M., Gurfinkel, A., Devereux, B.: χChek: A multi-valued model-checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 505. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  7. 7.
    Clarke, E.M., Draghicescu, I.A.: Expressibility results for linear-time and branching-time logics. In: Proc. Workshop on LTBTPO LNCS, vol. 354, pp. 428–437. Springer, Heidelberg (1988)Google Scholar
  8. 8.
    Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proceedings of PSTV, pp. 3–18 (1995)Google Scholar
  9. 9.
    Gurfinkel, A., Chechik, M., Devereux, B.: Temporal logic query checking: A tool for model exploration. IEEE Trans. Software Eng. 29(10), 898–914 (2003)CrossRefGoogle Scholar
  10. 10.
    Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth first search. In: Second SPIN Workshop, pp. 23–32. AMS, Providence (1996)Google Scholar
  11. 11.
    Hornus, S., Schnoebelen, P.: On solving temporal logic queries. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 163–177. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  12. 12.
    Peled, D.: Software Reliability Methods. Springer, Heidelberg (2001)CrossRefzbMATHGoogle Scholar
  13. 13.
    Samer, M., Veith, H.: A syntactic characterization of distributive ltl queries. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1099–1110. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  14. 14.
    Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  15. 15.
    Thirioux, X.: Simple and efficient translation from LTL formulas to Buchi automata. Electronic Notes in Theoretical Computer Science 66(2), 145–159 (2002); FMICS 2002, 7th International ERCIM Workshop in Formal Methods for Industrial Critical Systems (ICALP 2002 Satellite Workshop)CrossRefGoogle Scholar
  16. 16.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. First IEEE Symp. Logic in Comp. Sci, pp. 332–344 (1986)Google Scholar
  17. 17.
    Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 110(2) (1994)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Hana Chockler
    • 1
  • Arie Gurfinkel
    • 2
  • Ofer Strichman
    • 3
  1. 1.IBM Haifa Research LabHaifaIsrael
  2. 2.Software Engineering InstitutePittsburghUSA
  3. 3.Information Systems Engineering, IETechnionHaifaIsrael

Personalised recommendations