PDL with Negation of Atomic Programs

C. LutzC. Lutz, D. WaltherD. Walther

Datei:LutzWaltherJANCL05.ps.gz

Download

C. Lutz, D. Walther
PDL with Negation of Atomic Programs
Journal of Applied Non-Classical Logic, 15(2):189--214, 2005

Details
Bibtex

KurzfassungAbstract
Propositional dynamic logic (PDL) is one of the most successful

 variants of modal logic. To make it even more useful for
 applications, many extensions of PDL have been considered in the
 literature. A very natural and useful such extension is with
 negation of programs. Unfortunately, as long known,
 reasoning with the resulting logic is undecidable.  In this paper,
 we consider the extension of PDL with negation of atomic programs,
 only. We argue that this logic is still useful, e.g. in the context
 of description logics, and prove that satisfiability is decidable
 and ExpTime-complete using an approach based on Buechi tree

automata.

Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@article{ LutzWaltherJANCL05,
  author = {C. {Lutz} and D. {Walther}},
  journal = {Journal of Applied Non-Classical Logic},
  number = {2},
  pages = {189--214},
  title = {PDL with Negation of Atomic Programs},
  volume = {15},
  year = {2005},
}