zbMATH — the first resource for mathematics

Reasoning about the past with two-way automata. (English) Zbl 0909.03019
Larsen, Kim G. (ed.) et al., Automata, languages and programming. 25th international colloquium, ICALP ’98. Aalborg, Denmark, July 13–17, 1998. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1443, 628-641 (1998).
An exponential time upper bound for the satisfiability problem of the \(\mu\)-calculus with both forward and backward modalities is proved. To get this result an automata-theoretic approach is employed. It is shown that even though the full \(\mu\)-calculus does not have the finite-model property, it does have the tree-model property. This property asserts that if a formula is satisfiable then it is satisfiable by a bounded-degree infinite tree structure. It is shown how a formula \(\varphi\) can be translated to an automaton \(A_\varphi\) on infinite trees that accepts precisely the tree models of \(\varphi\). To check whether \(\varphi\) is satisfiable it suffices then to solve the emptiness problem for \(A_\varphi\). To deal with backward modalities two-way alternating automata (they are based on an analogous notion of two-way automata) on finite trees are introduced. Alternating tree automata (both one-way and two-way) can be viewed as infinite games. A fact that the winning player has a memoryless strategy (under certain conditions) is used to show that two-way alternating tree automata can be translated to equivalent one-way nondeterministic tree automata with an exponential blowup. The emptiness problem can then be solved by using known algorithms for emptiness of nondeterministic tree automata.
For the entire collection see [Zbl 0893.00039].

03B45 Modal logic (including the logic of norms)
03D05 Automata and formal grammars in connection with logical questions
03B70 Logic in computer science