An initial semantics for the \(\mu\)-calculus on trees and Rabin’s complementation lemma. (English) Zbl 0873.68157

Arnold, André

Theor. Comput. Sci. 148, No. 1, 121-132 (1995).

Summary: We show that the function associated with any closed or nonclosed term of the \(\mu\)-calculus on trees can be represented by a recognizable set of trees whose nodes are labeled by letters and by sets of variables. Rabin’s complementation lemma is an immediate consequence of this result.

MSC:

68R10	Graph theory (including graph drawing) in computer science
68Q45	Formal languages and automata

Keywords:

tree automaton

References:

[1]	Arnold, A.; Niwiński, D., Fixed point characterization of weak monadic logic definable sets of trees, (), 159-188 · Zbl 0794.03054
[2]	Emerson, E.A.; Jutla, C.S., Tree automata, μ-calculus and determinacy, (), 368-377
[3]	Gurevich, Y.; Harrington, L., Trees, automata, and games, (), 60-65
[4]	Kozen, D., Results on the prepositional μ-calculus, Theor. comput. sci., 27, 333-354, (1983) · Zbl 0553.03007
[5]	Muchnik, A.A., Games on infinite trees and automata with dead-ends: a new proof for the decidability of the monadic second order theory of two successors, Bull. EATCS, 48, 220-267, (1992), (translation of a Russian paper of 1984) · Zbl 1030.03513
[6]	D.E. Muller and P.E. Schupp, Alternating automata on infinite trees. Theoret. Comput. Sci.{\bf54} 267-276. · Zbl 0636.68108
[7]	Niwiński, D., On fixed point clones, (), 464-473
[8]	Niwiński, D., Fixed points vs. infinite generation, (), 402-409
[9]	Pratt, V., A decidable mu-calculus, (), 421-427
[10]	Rabin, M.O., Decidability of second-order theories and automata on infinite trees, Trans. amer. soc., 141, 1-35, (1969) · Zbl 0221.02031
[11]	Thomas, W., Automata on infinite objects, (), 133-191 · Zbl 0900.68316
[12]	Thomas, W., Infinite trees and automaton definable relations over ω-words, Theoret. comput. sci., 103, 143-159, (1992) · Zbl 0760.68043