Propositional Dynamic Logic with Quantification over Regular Computation Sequences

Abstrakt

We extend test-free regular propositional dynamic logic with operators expressing combinations of existential and universal quantifiers quantifying over computation sequences represented by a given regular expression and states accessible via these computation sequences. This extended language is able to express that there is a computation sequence represented by a given regular expression that leads only to states where a given formula is satisfied, or that for all computation sequences represented by a given regular expression there is a state accessible via the computation sequence where a given formula is satisfied. Such quantifier combinations are essential in expressing, for instance, that a given non-deterministic finite automaton accepts all words of a given regular language or that there is a specific sequence of actions instantiating a plan expressed by a regular expression that is guaranteed to accomplish a certain goal. The existential-universal quantifier combination is modelled by neighborhood functions. We prove that a rich fragment of our logic is decidable and EXPTIME -complete by embedding the fragment into deterministic propositional dynamic logic.