Propositional dynamic logic of looping and converse is elementarily decidable

Propositional dynamic logic is a formal system for reasoning about the before—after behavior of regular program schemes. An extension of propositional dynamic logic which includes both an infinite looping construct and a converse or backtracking construct is considered and it is proved that the satisfiability problem for this logic is elementarily decidable. In order to establish this result, deterministic two-way automata on infinite trees are defined, and it is shown how they can be simulated by nondeterministic one-way automata. The satisfiability problem for propositional dynamic logic of looping and converse is then reduced to the emptiness problem for these two-way automata