Model composition in model checking

Felscher, Ingo; Thomas, Wolfgang

doi:urn:nbn:de:hbz:82-opus-49921

Model composition in model checking = Model Komposition im Model-Checking

Felscher, Ingo (Author)

2014

Verantwortlichkeitsangabevorgelegt von Ingo Felscher

ImpressumAachen 2014

UmfangIX, 121 S. : graph. Darst.

Aachen, Techn. Hochsch., Diss., 2014

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Thomas, Wolfgang (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2014-01-27

Online
URN: urn:nbn:de:hbz:82-opus-49921
URL: https://publications.rwth-aachen.de/record/229032/files/4992.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Mathematische Logik (Genormte SW) ; Model Checking (Genormte SW) ; Modelltheorie (Genormte SW) ; Temporale Logik (Genormte SW) ; Prädikatenlogik (Genormte SW) ; Informatik (frei) ; model composition (frei) ; model-checking (frei) ; model theory (frei) ; logic (frei) ; composed systems (frei)

Thematische Einordnung (Klassifikation)
DDC: 004
ccs: F.4.1 I.2.

Kurzfassung
Model-Checking ermöglicht das formale Überprüfen von Eigenschaften von Systemen. Diese Eigenschaften werden als Logikformeln und die Systeme als Transitionssysteme modelliert. Die Transitionssysteme sind häufig zusammengesetzt als Produkte oder Summen. Die Kompositionstechnik leitet die Gültigkeit von Formeln im zusammengesetzten System aus „Interfaceinformationen” ab: der Gültigkeit von Formeln in den Komponenten des Systems sowie Informationen darüber, in welchen Komponenten welche Formel gilt. Wir interessieren uns für Situationen, in denen die Kompositionstechnik funktioniert und analysieren wie groß in diesen Situationen die Interfaceinformationen werden können. Im ersten Teil der Arbeit erweitern wir bekannte Resultate für synchronisierte Produkte von Transitionssystemen indem wir einen Kompositionssatz für endlich synchronisierte Produkte und First-Order Logic (oder Modal Logic) erweitert mit regulärer Erreichbarkeit über einem einstelligen Alphabet zeigen. Weiter zeigen wir, dass die Kompositionstechnik für zwei Erweiterungen der Logik fehlschlägt: für reguläre Erreichbarkeit und für Propositional Dynamic Logic über einem einelementigen Alphabet. Außerdem schlägt sie für synchronisierte Produkte fehl, die nicht endlich synchronisiert sind. Ein bekannter Nachteil der Kompositionstechnik ist das Wachstum der Größe der Interfaceinformationen in Bezug zur gegebenen Formel. Göller, Jung und Lohrey haben im Allgemeinen eine nicht-elementare untere Schranke für diese Größe gezeigt. Im zweiten und dritten Teil der Arbeit betrachten wir Kombinationen von Logiken und speziellen Systemen, bei denen wir dies verhindern können. Im zweiten Teil zeigen wir einen Kompositionssatz für Linear Temporal Logic (LTL) und disjunkte geordnete Summen von Wörtern. Eine gründliche Analyse zeigt, dass die Größe der Interfaceinformationen hier exponentiell zur Größe der gegebenen Formel wächst. Im dritten Teil verallgemeinern wir diese Kompositionstechnik auf eine disjunkte geordnete Summe von Bäumen und Computation Tree Logic (CTL). Hier ist jede Komponente ein Baum und im Allgemeinen auch die Struktur die zur Verknüpfung der Komponenten dient. Wir zeigen einen Kompositionssatz, bei dem die Interfaceinformationen exponentiell in der Länge der gegebenen Formel und in der Verzweigung der Indexbaumstruktur wachsen.

Model-checking allows one to formally check properties of systems: these properties are modeled as logic formulas and the systems as structures like transition systems. These transition systems are often composed, i.e., they arise in form of products or sums. The composition technique allows us to deduce the truth of a formula in the composed system from "interface information": the truth of formulas for the component systems and information in which components which of these formulas hold. We are interested in identifying situations where the composition technique works in the context of model-checking (reachability properties, linear and branching time temporal logic) and, in these cases, how large the interface information can become. In the first main part of this thesis, we extend known results for synchronized products of transition systems by showing a composition theorem for finitely synchronized products and first-order logic (or modal logic) extended by regular reachability over a unary alphabet. We further show that the composition technique fails for two generalizations of the logic: in the general case of regular reachability and in the case of propositional dynamic logic over a unary alphabet. Furthermore, it fails for synchronized products which are not finitely synchronized. A known drawback of the composition technique is the growth of the size of the generated interface information in relation to the given formula. Göller, Jung and Lohrey have shown a non-elementary lower bound for this size in general for first-order logic (for products) and modal logic (for disjoint ordered sums). In the second and third part of this thesis, we look at combinations of logics and systems where we can avoid this. In the second part, we show a composition theorem for linear temporal logic (LTL) and disjoint ordered sums of words. A careful analysis shows that, here, the size of the interface information only grows at most exponential in the size of the given formula. In the third part, we generalize this composition technique to a disjoint ordered sum of trees and computation tree logic (CTL). Here, we deal with trees as components which are composed via a tree structure. We show a composition result for which the interface information grows exponentially in the size of the given formula and in the branching of the index tree structure.

Fulltext:
PDF