Advertisement

LTL Semantic Tableaux and Alternating \(\omega \)-automata via Linear Factors

  • Martin Sulzmann
  • Peter Thiemann
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11187)

Abstract

Linear Temporal Logic (LTL) is a widely used specification framework for linear time properties of systems. The standard approach for verifying such properties is by transforming LTL formulae to suitable \(\omega \)-automata and then applying model checking. We revisit Vardi’s transformation of an LTL formula to an alternating \(\omega \)-automaton and Wolper’s LTL tableau method for satisfiability checking. We observe that both constructions effectively rely on a decomposition of formulae into linear factors. Linear factors have been introduced previously by Antimirov in the context of regular expressions. We establish the notion of linear factors for LTL and verify essential properties such as expansion and finiteness. Our results shed new insights on the connection between the construction of alternating \(\omega \)-automata and semantic tableaux.

Supplementary material

References

  1. 1.
    Antimirov, V.M.: Partial derivatives of regular expressions and finite automaton constructions. Theor. Comput. Sci. 155(2), 291–319 (1996).  https://doi.org/10.1016/0304-3975(95)00182-4MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    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).  https://doi.org/10.1007/978-3-642-28756-5_8CrossRefzbMATHGoogle Scholar
  3. 3.
    Broda, S., Machiavelo, A., Moreira, N., Reis, R.: Partial derivative automaton for regular expressions with shuffle. In: Shallit, J., Okhotin, A. (eds.) DCFS 2015. LNCS, vol. 9118, pp. 21–32. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-19225-3_2CrossRefGoogle Scholar
  4. 4.
    Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 253–271. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48119-2_16CrossRefGoogle Scholar
  5. 5.
    Esparza, J., Křetínský, J., Sickert, S.: From LTL to deterministic automata: a safraless compositional approach. Form. Methods Syst. Des. 49(3), 219–271 (2016).  https://doi.org/10.1007/s10703-016-0259-2CrossRefzbMATHGoogle Scholar
  6. 6.
    Finkbeiner, B., Sipma, H.: Checking finite traces using alternating automata. Form. Methods Syst. Des. 24(2), 101–127 (2004).  https://doi.org/10.1023/b:form.0000017718.28096.48CrossRefzbMATHGoogle Scholar
  7. 7.
    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).  https://doi.org/10.1007/3-540-44585-4_6CrossRefGoogle Scholar
  8. 8.
    Geldenhuys, J., Valmari, A.: More efficient on-the-fly LTL verification with Tarjan’s algorithm. Theor. Comput. Sci. 345(1), 60–82 (2005).  https://doi.org/10.1016/j.tcs.2005.07.004MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembinski, P., Sredniawa, M. (eds.) PSTV 1995. IFIPAICT, pp. 3–18. Springer, Boston (1996).  https://doi.org/10.1007/978-0-387-34892-6_1CrossRefGoogle Scholar
  10. 10.
    Loding, C., Thomas, W.: Alternating automata and logics over infinite words. In: van Leeuwen, J., Watanabe, O., Hagiya, M., Mosses, P.D., Ito, T. (eds.) TCS 2000. LNCS, vol. 1872, pp. 521–535. Springer, Heidelberg (2000).  https://doi.org/10.1007/3-540-44929-9_36CrossRefGoogle Scholar
  11. 11.
    Muller, D.E., Saoudi, A., Schupp, P.E.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: Proceedings of 3rd Annual Symposium on Logic in Computer Science, LICS 1999, Edinburgh, July 1988, pp. 422–427. IEEE CS Press (1988).  https://doi.org/10.1109/lics.1988.5139
  12. 12.
    Pelánek, R., Strejček, J.: Deeper connections between LTL and alternating automata. In: Farré, J., Litovsky, I., Schmitz, S. (eds.) CIAA 2005. LNCS, vol. 3845, pp. 238–249. Springer, Heidelberg (2006).  https://doi.org/10.1007/11605157_20CrossRefzbMATHGoogle Scholar
  13. 13.
    Pnueli, A.: The temporal logic of programs. In: Proceedings of 18th Annual Symposium on Foundations of Computer Science, FOCS 1977, Providence, RI, October–November 1977, pp. 46–57. IEEE CS Press (1977).  https://doi.org/10.1109/sfcs.1977.32
  14. 14.
    Reynolds, M.: A new rule for LTL tableaux. In: Cantone, D., Delzanno, G. (eds.) Proceedings of 7th International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016 (Catania, September 2016). Electronic Proceedings in Theoretical Computer Science, vol. 226, pp. 287–301. Open Public Association, Sydney (2016).  https://doi.org/10.4204/eptcs.226.20MathSciNetCrossRefGoogle Scholar
  15. 15.
    Schwendimann, S.: A new one-pass tableau calculus for PLTL. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 277–291. Springer, Heidelberg (1998).  https://doi.org/10.1007/3-540-69778-0_28CrossRefGoogle Scholar
  16. 16.
    Thiemann, P., Sulzmann, M.: From \(\omega \)-regular expressions to Büchi automata via partial derivatives. In: Dediu, A.-H., Formenti, E., Martín-Vide, C., Truthe, B. (eds.) LATA 2015. LNCS, vol. 8977, pp. 287–298. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-15579-1_22CrossRefzbMATHGoogle Scholar
  17. 17.
    Vardi, M.Y.: Nontraditional applications of automata theory. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 575–597. Springer, Heidelberg (1994).  https://doi.org/10.1007/3-540-57887-0_116CrossRefGoogle Scholar
  18. 18.
    Vardi, M.Y.: Alternating automata: unifying truth and validity checking for temporal logics. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 191–206. Springer, Heidelberg (1997).  https://doi.org/10.1007/3-540-63104-6_19CrossRefGoogle Scholar
  19. 19.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of 1st Symposium on Logic in Computer Science, LICS 1986, Cambridge, MA, June 1986, pp. 332–344. IEEE CS Press (1986)Google Scholar
  20. 20.
    Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994).  https://doi.org/10.1006/inco.1994.1092MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1/2), 72–99 (1983).  https://doi.org/10.1016/s0019-9958(83)80051-5MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Wolper, P.: The tableau method for temporal logic: an overview. Log. Anal. 28(110–111), 119–136 (1985). https://www.jstor.org/stable/44084125MathSciNetzbMATHGoogle Scholar
  23. 23.
    Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths (extended abstract). In: Proceedings of 24th Annual Symposium on Foundations of Computer Science, FOCS 1983, Tucson, AZ, November 1983, pp. 185–194. IEEE CS Press (1983).  https://doi.org/10.1109/sfcs.1983.51

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Faculty of Computer Science and Business Information SystemsKarlsruhe University of Applied SciencesKarlsruheGermany
  2. 2.Faculty of EngineeringUniversity of FreiburgFreiburgGermany

Personalised recommendations