Please use this identifier to cite or link to this item: doi:10.22028/D291-26295
Title: Incremental decision procedures for modal logics with nominals and eventualities
Other Titles: Inkrementelle Entscheidungsverfahren für Modallogiken mit Nominalen und Eventualities
Author(s): Kaminski, Mark
Language: English
Year of Publication: 2012
SWD key words: Entscheidungsverfahren
Tableau <Logik>
Dynamische Aussagenlogik
Computational logic
Modallogik
Automatisches Beweisverfahren
Free key words: Hybridlogik
Nominale
Temporallogik
decision procedures
automated reasoning
tableau systems
propositional dynamic logic
modal logic
hybrid logic
DDC notations: 004 Computer science, internet
Publikation type: Dissertation
Abstract: This thesis contributes to the study of incremental decision procedures for modal logics with nominals and eventualities. Eventualities are constructs that allow to reason about the reflexive-transitive closure of relations. Eventualities are an essential feature of temporal logics and propositional dynamic logic (PDL). Nominals extend modal logics with the possibility to reason about state equality. Modal logics with nominals are often called hybrid logics. Incremental procedures are procedures that can potentially solve a problem by performing only the reasoning steps needed for the problem in the underlying calculus. We begin by introducing a class of syntactic models called demos and showing how demos can be used for obtaining nonincremental but worst-case optimal decision procedures for extensions of PDL with nominals, converse and difference modalities. We show that in the absence of nominals, such nonincremental procedures can be refined into incremental demo search procedures, obtaining a worst-case optimal decision procedure for modal logic with eventualities. We then develop the first incremental decision procedure for basic hybrid logic with eventualities, which we eventually extend to deal with hybrid PDL. The approach in the thesis suggests a new principled design of modular, incremental decision procedures for expressive modal logics. In particular, it yields the first incremental procedures for modal logics containing both nominals and eventualities.
Diese Dissertation untersucht inkrementelle Entscheidungsverfahren für Modallogiken mit Nominalen und Eventualities. Eventualities sind Konstrukte, die erlauben, über den reflexiv-transitiven Abschluss von Relationen zu sprechen. Sie sind ein Schlüsselmerkmal von Temporallogiken und dynamischer Aussagenlogik (PDL). Nominale erweitern Modallogik um die Möglichkeit, über Gleichheit von Zuständen zu sprechen. Modallogik mit Nominalen nennt man Hybridlogik. Inkrementell ist ein Verfahren dann, wenn es ein Problem so lösen kann, dass für die Lösung nur solche Schritte in dem zugrundeliegenden Kalkül gemacht werden, die für das Problem relevant sind. Wir führen zunächst eine Klasse syntaktischer Modelle ein, die wir Demos nennen. Wir nutzen Demos um nichtinkrementelle aber laufzeitoptimale Entscheidungsverfahren für Erweiterungen von PDL zu konstruieren. Wir zeigen, dass im Fall ohne Nominale solche Verfahren durch algorithmische Verfeinerung zu inkrementellen Verfahren ausgebaut werden können. Insbesondere erhalten wir so ein optimales Verfahren für Modallogik mit Eventualities. Anschließend entwickeln wir das erste inkrementelle Verfahren für Hybridlogik mit Eventualities, welches wir schließlich auf hybrides PDL erweitern. Die Dissertation vermittelt einen neuen Ansatz zur Konstruktion modularer, inkrementeller Entscheidungsverfahren für expressive Modallogiken. Insbesondere liefert der Ansatz die ersten inkrementellen Verfahren für Modallogiken mit Nominalen und Eventualities.
Link to this record: urn:nbn:de:bsz:291-scidok-46765
hdl:20.500.11880/26351
http://dx.doi.org/10.22028/D291-26295
Advisor: Smolka, Gert
Date of oral examination: 24-Jan-2012
Date of registration: 8-Feb-2012
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
thesis_print.pdf1,32 MBAdobe PDFView/Open


Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.