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)


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


  1. 1.
    Antimirov, V.M.: Partial derivatives of regular expressions and finite automaton constructions. Theor. Comput. Sci. 155(2), 291–319 (1996). 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). 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). 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). 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). Scholar
  6. 6.
    Finkbeiner, B., Sipma, H.: Checking finite traces using alternating automata. Form. Methods Syst. Des. 24(2), 101–127 (2004). 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). 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). 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). 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). 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).
  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). 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).
  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). 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). 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). 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). 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). 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). Scholar
  21. 21.
    Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1/2), 72–99 (1983). Scholar
  22. 22.
    Wolper, P.: The tableau method for temporal logic: an overview. Log. Anal. 28(110–111), 119–136 (1985). 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).

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