Abstract
A graph extension of two-way alternating automata on trees is considered. The following problem: “does a given automaton accept any finite graph?” is proven EXPTIME complete. Using this result, the decidability of the finite model problem for the modal μ-calculus with backward modalities is shown.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Mikolaj Bojańczyk. The finite graph problem for two-way alternating automata. In FOSSACS 2001, volume 2030 of LNCS, pages 88–103, 2001.
A. Saoudi D. E. Muller and P. E. Shupp. Weak alternating automata give a simple explanation why most temporal and dynamic logics are decidable in exponential time. In Proceedings 3rd IEEE Symposium on Logic in Computer Science, pages 422–427, 1988.
E. A. Emerson and C. Jutla. Tree automata, mu-calculus and determinacy. In Proc. 32th IEEE Symposium on Foundations of Computer Science, pages 368–377, 1991.
E. Grädel. On the restraining power of guards. Journal of Symbolic Logic, 1999.
E. Grädel and I. Walukiewicz. Guarded fixed point logic. In Proceedings 14th IEEE Symp. on Logic in Computer Science, pages 45–54, 1999.
Y. Gurevich and L. Harrington. Automata, trees and games. In Proc. 14th. Ann. ACM Symp. on the Theory of Computing, pages 60–65, 1982.
J. van Benthem H. Andreka and I. Nemeti. Modal logics and bounded fragments of predicate logic. Journal of Philosophical Logic, pages 217–274, 1998.
I. Hodkinson. Loosely guarded fragment has finite model property. J. Symbolic Logic, to appear.
D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333–354, 1983.
R. Ladner M. Fischer. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18:194–211, 1979.
A. Mostowski. Games with forbidden positions. Technical report, University of Gdańsk, 1991.
D.E. Muller and P.E. Schupp. Alternating automata on infinite trees. Theoretical Computer Science, 54:267–276, 1987.
M. O. Rabin. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc., 141, 1969.
G. Slutzki. Alternating tree automata. Theoretical Computer Science, 41:305–318, 1985.
Wolfgang Thomas. Languages, automata, and logic. In Handbook of Formal Language Theory, III, pages 389–455. Springer, 1997.
M. Vardi. Reasoning about the past with two-way automata. In vol. 1443 LNCS, pages 628–641, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bojarńczyk, M. (2002). Two-Way Alternating Automata and Finite Models. In: Widmayer, P., Eidenbenz, S., Triguero, F., Morales, R., Conejo, R., Hennessy, M. (eds) Automata, Languages and Programming. ICALP 2002. Lecture Notes in Computer Science, vol 2380. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45465-9_71
Download citation
DOI: https://doi.org/10.1007/3-540-45465-9_71
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43864-9
Online ISBN: 978-3-540-45465-6
eBook Packages: Springer Book Archive