On the Complexity of Modal Logic Variants and their Fragments
-
- Taschenbuch
- eBook ausgewählt
-
Form:Einzelkauf Download
-
Sprache:Englisch
17,05 €
inkl. gesetzl. MwSt.Beschreibung
Produktdetails
Format
Kopierschutz
Nein
Family Sharing
Ja
Text-to-Speech
Nein
Erscheinungsdatum
15.11.2011
Verlag
Cuvillier Verlag eBooksSeitenzahl
148 (Printausgabe)
Dateigröße
912 KB
Sprache
Englisch
EAN
9783736939295
The automatic verification of computer programs is an important step in software engineering. In this regard temporal logics have been invented as an extension of modal logic which itself is an extension of propositional logic. Therefore, one may call them \emph{modal logic variants}.
The first part of this thesis will investigate the two temporal logics CTL and CTL* with respect to their model-checking and satisfiability problem. We will analyze the complexity of fragments of these problems by means of operator and Boolean function restrictions. There we will see for the satisfiability problem, how the operator fragments form a trichotomy and the Boolean fragments form a quartering. The model-checking problem for CTL is divided into three types: monotone, atomic negation, and positive fragments. Surprisingly, we will see that these three fragments are computationally equivalent. Furthermore, several prominent extensions of CTL will be visited and classified with respect to their Boolean and operator fragments.
In the second part we will concentrate on description logics which are modal logic extensions settled in the area of semantic web, databases, and artificial intelligence. These types of logics are used to express, and work on, large sets of data. Besides the usual satisfiability problems, we will work with some special kind of implication problem, which is called subsumption. We will see that these logics combine two very strong Boolean concepts, namely implication and conjunction, such that restricting large sets of Boolean functions do not reduce the complexity of the problems significantly.
The first part of this thesis will investigate the two temporal logics CTL and CTL* with respect to their model-checking and satisfiability problem. We will analyze the complexity of fragments of these problems by means of operator and Boolean function restrictions. There we will see for the satisfiability problem, how the operator fragments form a trichotomy and the Boolean fragments form a quartering. The model-checking problem for CTL is divided into three types: monotone, atomic negation, and positive fragments. Surprisingly, we will see that these three fragments are computationally equivalent. Furthermore, several prominent extensions of CTL will be visited and classified with respect to their Boolean and operator fragments.
In the second part we will concentrate on description logics which are modal logic extensions settled in the area of semantic web, databases, and artificial intelligence. These types of logics are used to express, and work on, large sets of data. Besides the usual satisfiability problems, we will work with some special kind of implication problem, which is called subsumption. We will see that these logics combine two very strong Boolean concepts, namely implication and conjunction, such that restricting large sets of Boolean functions do not reduce the complexity of the problems significantly.
Noch keine Bewertungen vorhanden
Verfassen Sie die erste Bewertung zu diesem Artikel
Helfen Sie anderen Kundinnen und Kunden durch Ihre Meinung.
Kurze Frage zu unserer Seite
Vielen Dank für dein Feedback
Wir nutzen dein Feedback, um unsere Produktseiten zu verbessern. Bitte habe Verständnis, dass wir dir keine Rückmeldung geben können. Falls du Kontakt mit uns aufnehmen möchtest, kannst du dich aber gerne an unseren Kund*innenservice wenden.
zum Kundenservice