LtlNfBa: Making LTL Translation More Practical

1. Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundation of Computer Science, pp. 46–57 (1977)

   Google Scholar 

2. Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994)

   Article  MathSciNet  MATH  Google Scholar 

3. Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: Proceedings of the 24th IEEE Symposium on Foundations of Computer Science, Tucson, pp. 185–194 (1983)

   Google Scholar 

4. Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembiski, P., Sredniawa, M. (eds.) Protocol Specification, Testing, and Verification, pp. 3–18. Chapman & Hall, London (1995)

   Google Scholar 

5. Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 415–427. Springer, Heidelberg (1994)

   Chapter  Google Scholar 

6. 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)

   Chapter  Google Scholar 

7. Vardi, M.Y.: Automata-theoretic model checking revisited. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 137–150. Springer, Heidelberg (2007)

   Chapter  Google Scholar 

8. Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999)

   Chapter  Google Scholar 

9. Etessami, K., Holzmann, G.J.: Optimizing Büchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 153–167. Springer, Heidelberg (2000)

   Chapter  Google Scholar 

10. Fritz, C.: Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata. In: Ibarra, O.H., Dang, Z. (eds.) CIAA 2003. LNCS, vol. 2759, pp. 35–48. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

11. Fritz, C.: Concepts of automata construction from LTL. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 728–742. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

12. 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)

    Chapter  Google Scholar 

13. Thirioux, X.: Simple and efficient translation from LTL formulas to Büchi automata. Electr. Notes Theor. Comput. Sci. 66(2), 145–159 (2002)

    Article  Google Scholar 

14. Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica 45(1), 43–78 (2008)

    Article  MathSciNet  MATH  Google Scholar 

15. Emerson, A.E.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Methods and Semantics, vol. B, pp. 995–1072 (1990)

    Google Scholar 

16. Duan, Z.: An extended interval temporal logic and a framing technique for temporal logic programming. Ph.D. thesis, University of Newcastle Upon Tyne, May 1996

    Google Scholar 

17. Katoen, J.-P.: Concepts, Algorithms, and Tools for Model Checking. Lecture Notes of the Course Mechanised Validation of Parrel Systems (1999)

    Google Scholar 

18. Gastin, P., Oddoux, D.: Fast LTL to Büchi Automata Translation. In CAV , LNCS 2102, pp. 53–65, Springer-Verlag, 2001. (2001)

    Google Scholar 

19. 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)

    Chapter  Google Scholar 

20. Babiak, T., Kretinsky, M., Rehak, V., Strejcek, J.: LTL to Büchi Automata Translation: Fast and More Deterministic. CoRR, abs/1201.0682 (2012)

    Google Scholar 

21. Duret-Lutz, A., Poitrenaud, D.: SPOT: an extensible model checking library using transition-based generalized Büchi automata. In: MASCOTS 2004, pp. 76–83 (2004)

    Google Scholar 

22. Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Wing, J.M., Woodcock, J. (eds.) FM 1999. LNCS, vol. 1708, p. 253. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

23. Tian, C., Duan, Z.: A note on stutter-invariant PLTL. Inf. Process. Lett. 109(13), 663–667 (2009)

    Article  MathSciNet  MATH  Google Scholar 

24. Cichon, J., Czubak, A., Jasinski, A.: Minimal Büchi automata for certain classes of LTL formulas. In: DEPCOS-RELCOMEX 2009, pp. 17–24. IEEE (2009)

    Google Scholar 

Download references