- Titel
- PDL with Negation of Atomic Programs
- Zitierfähige Url:
- https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-790555
- Schriftenreihe
- LTCS-Report
- Bandnummer
- 03-04
- Erstveröffentlichung
- 2003
- DOI
- https://doi.org/10.25368/2022.129
- Abstract (EN)
- Propositional dynamic logic (PDL) is one of the most succesful 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 Büchi tree automata.
- Freie Schlagwörter (DE)
- Dynamische Logik, PDL, Büchi Automat, Beschreibungslogik, EXPTIME-komplett
- Freie Schlagwörter (EN)
- propositional dynamic logic, PDL, Büchi tree automata, description logic, EXPTIME-complete
- Klassifikation (DDC)
- 004
- Klassifikation (RVK)
- ST 136
- Publizierende Institution
- Technische Universität Dresden, Dresden
- Version / Begutachtungsstatus
- angenommene Version / Postprint / Autorenversion
- URN Qucosa
- urn:nbn:de:bsz:14-qucosa2-790555
- Veröffentlichungsdatum Qucosa
- 30.05.2022
- Dokumenttyp
- Bericht
- Sprache des Dokumentes
- Englisch
- Lizenz / Rechtehinweis
CC BY 4.0