Deterministic process logic is elementary

Process Logic (PL) is a language for reasoning about the behavior of a program during a computation, while Propositional Dynamic Logic (PDL) can only reason about the input-output states of a program. Nevertheless, we show that to each PL model M there corresponds in a natural way a PDL, model Mt such that every path in M is represented by a state in Mt. Moreover, to every PL formula p there corresponds a PDL formula pt, whose length is linear in that of p, such that p is true of a path in M iff pt is true of the state which represents that path in Mt. We then show that p is satisfiable iff pt is satisfiable in a finite PDL model with special properties which we call a pseudomodel. The size of the pseudomodel is in general nonelementary, and depends on the depth of nesting of the suf operator in PL. However, for PDL, a deterministic version of PL, the pseudomodel has size 2|p|2, giving us a decision procedure for PDL which runs in deterministic time O(2cn2). These results suggest that it is the interaction between nondeterministic programs and thc suf operator that makes the general decision problem for PL so difficult.