Automata-theoretic techniques for modal logics of programs (Q1090675): Difference between revisions

The authors introduce a new type of automata, called subtree automata, in order to simplify \textit{M. O. Rabin}'s [Math. Logic Found. Set Theory, Proc. Int. Colloq., Jerusalem 1968, 1-23 (1970; Zbl 0214.022)] reduction of the satisfiability problem for logics to the emptiness problem for special automata, which the authors prefer to call Büchi automata in honor of \textit{J. R. Büchi} [Logic, Method. Philos. Sci., Proc. 1960 Int. Congr., 1-11 (1962; Zbl 0147.251)]. The emptiness of subtree automata can be checked in polynomial time and the reduction establishes the desired exponential upper bound for satisfiability. This unifying technique is applied to the following three logics: (1) ADPDL (deterministic PDL of flowcharts), (2) the extension of ADPDL with the loop construct, (3) the extension of ADPDL with the converse construct.