On the Deterministic Horn Fragment of Test-free PDL
Linh Anh Nguyen · Advances in Modal Logic · 2006
We study the deterministic Horn fragment of test-free proposi- tional dynamic logic (PDL(0)). This fragment adopts the restriction that, in bodies of program clauses and goals, special universal modal operators which are a kind of combination of ! and are used instead of ! . The fragment contains deterministic positive logic programs and deterministic negative clauses, whose negations form serial positive formulae. A least Kripke model for a deterministic positive logic program in PDL (0) may not exist, because PDL(0) is a non-serial modal logic. In this work, we present an algorithm that, given a deterministic positive logic program P in PDL (0) , constructs a least pseudo-model of P. A pseudo-model is similar to a Kripke model except that it contains two sets of accessibility relations, one for dealing with existential modal operators and the other for dealing with universal modal operators. A least pseudo-model M of P has the property that, for every serial positive formula ! , P |= ! i! M |= ! . Fur- thermore, checking whether M |= ! is solvable in polynomial time in the sizes of M and ! . Our algorithm runs in exponential time and returns a pseudo-model with size 2 O(n 2 ) . We give a deterministic positive logic pro- gram in PDL(0) such that every pseudo-model characterizing it must have size 2 ! (n) .