Deeper Connections Between LTL and Alternating Automata

1. 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 the 3rd IEEE Symposium on Logic in Computer Science (LICS 1988), pp. 422–427. IEEE Computer Society Press, Los Alamitos (1988)

   Google Scholar 

2. Rohde, S.: Alternating automata and the temporal logic of ordinals. PhD thesis, University of Illinois at Urbana-Champaign (1997)

   Google Scholar 

3. Löding, C., Thomas, W.: Alternating automata and logics over infinite words (extended abstract). In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, pp. 521–535. Springer, Heidelberg (2000)

   Chapter  Google Scholar 

4. Černá, I., Pelánek, R.: Relating hierarchy of temporal properties to model checking. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, Springer, Heidelberg (2003)

   Google Scholar 

5. Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths (extended abstract). In: 24th Annual Symposium on Foundations of Computer Science, pp. 185–194. IEEE, Los Alamitos (1983)

   Google Scholar 

6. Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115, 1–37 (1994)

   Article  MathSciNet  MATH  Google Scholar 

7. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the First Symposium on Logic in Computer Science, Cambridge, pp. 322–331 (1986)

   Google Scholar 

8. Wolper, P.: Temporal logic can be more expressive. Information and Control 56, 72–99 (1983)

   Article  MathSciNet  MATH  Google Scholar 

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

   Chapter  Google Scholar 

10. Tauriainen, H.: On translating linear temporal logic into alternating and nondeterministic automata. Research Report A83, Helsinki University of Technology, Laboratory for Theoretical Computer Science (2003)

    Google Scholar 

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

    Chapter  Google Scholar 

12. Thérien, D., Wilke, T.: Temporal logic and semidirect products: An effective characterization of the until hierarchy. In: 37th Annual Symposium on Foundations of Computer Science (FOCS 1996), pp. 256–263. IEEE, Los Alamitos (1996)

    Google Scholar 

13. Etessami, K., Wilke, T.: An until hierarchy and other applications of an Ehrenfeucht-Fraïssé game for temporal logic. Information and Computation 160, 88–108 (2000)

    Article  MathSciNet  MATH  Google Scholar 

14. Kučera, A., Strejček, J.: The stuttering principle revisited. Acta Informatica (to appear, 2005)

    Google Scholar 

15. Kučera, A., Strejček, J.: Characteristic patterns for LTL. In: Vojtáš, P., Bieliková, M., Charron-Bost, B., Sýkora, O. (eds.) SOFSEM 2005. LNCS, vol. 3381, pp. 239–249. Springer, Heidelberg (2005)

    Google Scholar 

16. Perrin, D., Pin, J.E.: Infinite words. Pure and Applied Mathematics, vol. 141. Elsevier, Amsterdam (2004)

    MATH  Google Scholar 

17. Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Proc. ACM Symposium on Principles of Distributed Computing, pp. 377–410. ACM Press, New York (1990)

    Chapter  Google Scholar 

18. Chang, E., Manna, Z., Pnueli, A.: Characterization of temporal property classes. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 474–486. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

19. Pelánek, R., Strejček, J.: Deeper connections between ltl and alternating automata. Technical Report FIMU-RS-2004-08, Faculty of Informatics, Masaryk University in Brno (2004), available at http://www.fi.muni.cz/reports/

Download references