Advertisement

Query Checking for Linear Temporal Logic

  • Samuel Huang
  • Rance CleavelandEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10471)

Abstract

The query-checking problem for temporal logic may be formulated as follows. Given a Kripke structure M and a temporal-logic query of form \(\phi \left[ {\texttt {var}}\right] \), which may be thought of as a temporal formula with a missing propositional subformula \({\texttt {var}}\), find the most precise propositional formula f that, when substituted for \({\texttt {var}}\) in \(\phi \left[ {\texttt {var}}\right] \), ensures M satisfies the resulting temporal property. Query checking has been used for system comprehension, specification reconstruction, and other related applications in the formal analysis of systems.

In this paper we present an automaton-based methodology for query checking over linear temporal logic (LTL). While this problem is known to be hard in the general case, we show that by exploiting several key observations about the interplay between the input model M and the query \(\phi \left[ {\texttt {var}}\right] \), we can produce results for many problems of interest. In support of this claim, we report on preliminary experimental data for an implementation of our technique.

References

  1. 1.
    Ackermann, C., Cleaveland, R., Huang, S., Ray, A., Shelton, C., Latronico, E.: Automatic requirement extraction from test cases. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 1–15. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-16612-9_1 CrossRefGoogle Scholar
  2. 2.
    Armoni, R., et al.: The ForSpec temporal logic: a new temporal property-specification language. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 296–311. Springer, Heidelberg (2002). doi: 10.1007/3-540-46002-0_21 CrossRefGoogle Scholar
  3. 3.
    Babiak, T., Křetínský, M., Řehák, V., Strejček, J.: LTL to Büchi automata translation: fast and more deterministic. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 95–109. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-28756-5_8 CrossRefGoogle Scholar
  4. 4.
    Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  5. 5.
    Bruns, G., Godefroid, P.: Temporal logic query checking. In: 16th Annual IEEE Symposium on Logic in Computer Science, pp. 409–417. IEEE, June 2001Google Scholar
  6. 6.
    Chan, W.: Temporal-logic queries. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 450–463. Springer, Heidelberg (2000). doi: 10.1007/10722167_34 CrossRefGoogle Scholar
  7. 7.
    Chockler, H., Gurfinkel, A., Strichman, O.: Variants of LTL Query Checking. In: Barner, S., Harris, I., Kroening, D., Raz, O. (eds.) HVC 2010. LNCS, vol. 6504, pp. 76–92. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-19583-9_11 CrossRefGoogle Scholar
  8. 8.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  9. 9.
    Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. MIT Press (1990)Google Scholar
  10. 10.
    Emerson, E.A., Halpern, J.Y.: “Sometimes” and “not never” revisited: On branching versus linear time temporal logic. JACM 33(1), 151–178 (1986)CrossRefzbMATHMathSciNetGoogle Scholar
  11. 11.
    Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1–3), 35–45 (2007)CrossRefzbMATHMathSciNetGoogle Scholar
  12. 12.
    Etessami, K., Holzmann, G.J.: Optimizing Büchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 153–168. Springer, Heidelberg (2000). doi: 10.1007/3-540-44618-4_13 CrossRefGoogle Scholar
  13. 13.
    Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001). doi: 10.1007/3-540-44585-4_6 CrossRefGoogle Scholar
  14. 14.
    Giannakopoulou, D., Lerda, F.: From states to transitions: improving translation of LTL formulae to Büchi automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 308–326. Springer, Heidelberg (2002). doi: 10.1007/3-540-36135-9_20 CrossRefGoogle Scholar
  15. 15.
    Gurfinkel, A., Chechik, M., Devereux, B.: Temporal logic query checking: a tool for model exploration. IEEE Trans. Soft. Eng. 29(10), 898–914 (2003)CrossRefGoogle Scholar
  16. 16.
    Lemieux, C., Park, D., Beschastnikh, I.: General LTL specification mining. In: 30th IEEE/ACM International Conference on Automated Software Engineering, pp. 81–92. IEEE, Lincoln, November 2015Google Scholar
  17. 17.
    Li, W., Forin, A., Seshia, S.A.: Scalable specification mining for verification and diagnosis. In: 47th Design Automation Conference, pp. 755–760. ACM, Anaheim, June 2010Google Scholar
  18. 18.
    Shoham, S., Yahav, E., Fink, S.J., Pistoia, M.: Static specification mining using automata-based abstractions. IEEE Trans. Soft. Eng. 34(5), 651–666 (2008)CrossRefGoogle Scholar
  19. 19.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: First Symposium on Logic in Computer Science, pp. 322–331. IEEE Computer Society, Boston, June 1986Google Scholar
  20. 20.
    Winter, K.: Model checking for abstract state machines. J. Univ. Comput. Sci. 3(5), 689–701 (1997)zbMATHGoogle Scholar
  21. 21.
    Zhang, D., Cleaveland, R.: Efficient temporal-logic query checking for Presburger systems. In: 20th IEEE/ACM International Conference on Automated Software Engineering, pp. 24–33. ACM, Long Beach, November 2005Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.University of MarylandCollege ParkUSA

Personalised recommendations