Abstract
Over the last decades the theory of finite automata on infinite objects has been an important source of tools for the specification and the verification of computer programs. Trees are more suitable than words to model nondeterminism and thus concurrency. In the literature, there are several examples of acceptance conditions that have been proposed for automata on infinite words and then have been fruitfully extended to infinite trees (Büchi, Rabin, and Muller conditions). The type of acceptance condition can influence both the succinctness of the corresponding class of automata and the complexity of the related decision problems. Here we consider, for automata on infinite trees, two acceptance conditions that are obtained by a relaxation of the Muller acceptance condition: the Landweber and the Muller-Superset conditions. We prove that Muller-Superset tree automata accept the same class of languages as Büchi tree automata, but using more succinct automata. Landweber tree automata, instead, define a class of languages which is not comparable with the one defined by Büchi tree automata. We prove that, for this class of automata, the emptiness problem is decidable in polynomial time, and thus we expand the class of automata with a tractable emptiness problem.
This research was partially supported by the NSF award CCR99-70925, NSF grant CCR-9988322, SRC award 99-TJ-688, DARPA ITO Mobies award F33615-00-C- 1707, NSF ITR award, and the MURST in the framework of project “Metodi Formali per la Sicurezza” (MEFISTO)
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
J.R. Büchi. Weak second-order arithmetic and finite automata. Z. Math Logik Grundlag. Math., 6:66–92, 1960.
J.R. Büchi. On a decision method in restricted second-order arithmetic. In Proc. of the International Congress on Logic, Methodology, and Philosophy of Science 1960, pages 1–12. Stanford University Press, 1962.
E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. of Workshop on Logic of Programs, LNCS 131, pages 52–71. Springer-Verlag, 1981.
E.A. Emerson and J.Y. Halpern. Sometimes and not never revisited: On branching versus linear time. Journal of the ACM, 33(1):151–178, 1986.
E.A. Emerson and C.S. Jutla. The complexity of tree automata and logics of programs. In Proc. of the 29th IEEE-CS Symposium on Foundations of Computer Science, pages 328–337, 1988.
R. Hossley. Finite tree Automata and ω-Automata. PhD thesis, MIT, Cambridge, Massachussets, 1970.
R.P. Kurshan. Computer-aided Verification of Coordinating Processes: the automata-theoretic approach. Princeton University Press, 1994.
L. H. Landweber. Decision problems for ω-automata. Mathematical System Theory, 3:376–384, 1969.
S. La Torre and M. Napoli. Finite automata on timed ω-trees. Theoretical Computer Science, To appear.
S. La Torre and M. Napoli. Timed tree automata with an application to temporal logic. Acta Informatica, 38(2):89–116, 2001.
R. McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9:521–530, 1966.
M.O. Rabin. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc., 141:1–35, 1969.
M.O. Rabin. Weakly definable relations and special automata. Mathematical Logic and Foundations of Set theory, 1970.
M.O. Rabin. Automata on Infinite Objects and Church’s Problem. Amer. Mathematical Soc., 1972.
M.Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Sciences, 32:182–211, 1986.
M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115:1–37, 1994.
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
La Torre, S., Murano, A., Napoli, M. (2002). Weak Muller Acceptance Conditions for Tree Automata. In: Cortesi, A. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2002. Lecture Notes in Computer Science, vol 2294. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47813-2_17
Download citation
DOI: https://doi.org/10.1007/3-540-47813-2_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43631-7
Online ISBN: 978-3-540-47813-3
eBook Packages: Springer Book Archive