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].

For the entire collection see [Zbl 0893.00039].

Reviewer: D.Gruska (Bratislava)

##### MSC:

03B45 | Modal logic (including the logic of norms) |

03D05 | Automata and formal grammars in connection with logical questions |

03B70 | Logic in computer science |