Improved upper and lower bounds for modal logics of programs
Moshe Y. Vardi, Larry Stockmeyer · 1985
We describe novel techniques for establishing improved upper and lower bounds for modal logics of programs: 1) We introduce hybrid tree automata. These automata seems to be doubly exponential more powerful than Rabin tree automata but their emptiness problem is only exponentially harder (nondeterministic exponential time vs. nondeterministic polynomial time). The satisfiability problem for several logics is reducible to the emptiness problem for hybrid tree automata. Using this reduction we show that the satisfiability problems for Streett's delta-PDL. Kozen's μ-calculus and Parikh's game logic are solvable in nondeterministic exponential time, and the satisfiability problem for Emerson and Halpern's CTL and Vardi and Wolper's process logic (YAPL) are solvable in nondeterministic doubly exponential time. 2) We encode Turing machine computations by Kripke structures where every state in the structure represents a single tape cell. This yields a deterministic doubly exponential time lower bound for CTL and YAPL. 3) For variants of CTL and YAPL that deal only with finite computations we prove completeness for deterministic doubly exponential time.