Abstract
It is known that Linear Temporal Logic (LTL) has the same expressive power as alternating 1-weak automata (A1W automata, also called alternating linear automata or very weak alternating automata). A translation of LTL formulae into a language equivalent A1W automata has been introduced in [1]. The inverse translation has been developed independently in [2] and [3]. In the first part of the paper we show that the latter translation wastes temporal operators and we propose some improvements of this translation. The second part of the paper draws a direct connection between fragments of the Until-Release hierarchy [4] and alternation depth of nonaccepting and accepting states in A1W automata. We also indicate some corollaries and applications of these results.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
Rohde, S.: Alternating automata and the temporal logic of ordinals. PhD thesis, University of Illinois at Urbana-Champaign (1997)
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)
Č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)
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)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115, 1–37 (1994)
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)
Wolper, P.: Temporal logic can be more expressive. Information and Control 56, 72–99 (1983)
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)
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)
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)
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)
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)
Kučera, A., Strejček, J.: The stuttering principle revisited. Acta Informatica (to appear, 2005)
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)
Perrin, D., Pin, J.E.: Infinite words. Pure and Applied Mathematics, vol. 141. Elsevier, Amsterdam (2004)
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)
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)
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/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pelánek, R., Strejček, J. (2006). Deeper Connections Between LTL and Alternating Automata. In: Farré, J., Litovsky, I., Schmitz, S. (eds) Implementation and Application of Automata. CIAA 2005. Lecture Notes in Computer Science, vol 3845. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11605157_20
Download citation
DOI: https://doi.org/10.1007/11605157_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31023-5
Online ISBN: 978-3-540-33097-4
eBook Packages: Computer ScienceComputer Science (R0)