PDL with Negation of Atomic Programs

Carsten Lutz, Dirk Walther
PDL with Negation of Atomic Programs
Technical Report, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, volume LTCS-03-04, 2003. LTCS-Report

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, it is long-known that 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.
Bemerkung: Note: See http://lat.inf.tu-dresden.de/research/reports.html.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@techreport{ LuWa-LTCS-03-04,
  address = {Germany},
  author = {C. {Lutz} and D. {Walther}},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-03-04},
  title = {PDL with Negation of Atomic Programs},
  type = {LTCS-Report},
  year = {2003},
}

PDL with Negation of Atomic Programs

PDL with Negation of Atomic Programs

Carsten LutzCarsten Lutz, Dirk WaltherDirk Walther