Reduction Techniques for Nondeterministic and Probabilistic Systems

Sharma, Arpit

2015 & 2015

VerantwortlichkeitsangabeArpid Sharma

ImpressumAachen : Fachgruppe Informatik, RWTH Aachen University 2015

UmfangXIV, 175 S.

ReiheAachener Informatik-Berichte ; 2015,3

Zugl.: Aachen, Techn. Hochsch., Diss., 2015

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor) ; Hermanns, Holger (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2015-01-15

Online
URN: urn:nbn:de:hbz:82-rwth-2015-005562
URL: https://publications.rwth-aachen.de/record/462319/files/462319.pdf
URL: https://publications.rwth-aachen.de/record/462319/files/462319.pdf?subformat=pdfa

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Informatik (frei) ; reduction (frei) ; model checking (frei) ; automaton (frei) ; probabilistic (frei) ; abstraction (frei) ; Markov chains (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Modelchecking ist ein automatisiertes Verfahren in der Verifikation, welches sicherstellt, dass ein mathematisches Modell eines Systems eine geforderte, formal definierte Eigenschaft besitzt. Es kann benutzt werden um sowohl qualitative als auch quantitative Eigenschaften komplexer Software- und Hardwaresysteme zu überprüfen. Beim Modelchecking stellt die Zustandsraumexplosion ein großes Problem dar. Dabei wächst die Anzahl der Zustände exponentiell mit der Anzahl der Programmvariablen, Kommunikationskanäle und Komponenten. Dem kann durch verschiedene Reduktionstechniken entgegengewirkt werden. Diese verringern den Zustandsraum, indem sie redundante Information verstecken oder irrelevante Details aus dem Model entfernen. Solange diese Manipulationen keinen Einfluss auf die Gültigkeit der zu überprüfenden Eigenschaften haben, können anschließend Analysetechniken auf dem verkleinerten Modell ausgeführt werden. Diese Arbeit beschäftigt sich mit Reduktionstechniken für ein breites Spektrum von nichtdeterministischen und probabilistischen Modellen. Die hier vorgestellten Techniken beruhen auf den Konzepten der Äquivalenzrelationen und Layering (engl. für "Schichtung"). Äquivalenzrelationen verkleinern den Zustandsraum, indem sie äquivalente Zustände zu einem einzigen zusammenfassen. Den auf dieser Weise reduzierten Zustandsraum nennt man Quotientenraum. Ein prominentes Beispiel einer Äquivalenzrelation, die zur Verkleinerung von nichtdeterministischen und probabilistischen Modellen benutzt wird, ist die Bisimulation. Auf der anderen Seite führt Layering strukturelle Transformationen auf dem gegebenen Modell durch. Das Ergebnis dieser strukturellen Transformationen ist ein kleinerer Zustandsraum als im Originalsystem. Dabei eignet sich Layering insbesondere für Systeme, die durch ein Netzwerk von Teilmodellen beschrieben werden, zum Beispiel verteilte Systeme. Der erste Teil dieser Arbeit beschäftigt sich mit der Entwicklung neuer Äquivalenzrelationen für nichtdeterministische und Markow'sche Modelle. Für jede solche Relation definieren wir ein Quotientensystem, untersuchen die Beziehung zur Bisimulationsrelation und zeigen, dass sie interessante Linearzeiteigenschaften erhält.Im zweiten Teil konzentrieren wir uns auf Zustandsraumreduktion durch Layering auf ausdrucksstärkeren Modellen, die eine schrittweise Verfeinerungsmethodik erlauben. Wir entwickeln einen Ansatz um Layering auf modale Transitionssysteme und deren probabilistische Erweiterung anzuwenden. Dieser beinhaltet einen "geschichteten" Kompositionsoperator, der Regeln für eine geschlossene Kommunikationsschicht (communication closed layer (CCL)) vorgibt und eine partielle Ordnungsäquivalenz zwischen modalen Transitionssystemen definiert. Außerdem zeigen wir, dass Zustandsraumverkleinerung mit Hilfe von Layering Erreichbarkeitseigenschaften erhält. Folglich können Erreichbarkeitseigenschaften auf dem typischerweise kleineren Modell überprüft werden. Insgesamt behandelt die vorliegende Arbeit die theoretischen Grundlagen für eine Reihe von neuen Reduktionstechniken für nichtdeterministische und probabilistische Systeme.

Model checking is an automated verification method guaranteeing that a mathematical model of a system satisfies a formally described property. It can be used to assess both qualitative and quantitative properties of complex software and hardware systems. Model checking suffers from the well-known state space explosion problem where the number of states grows exponentially in the number of program variables, channels and parallel components. Reduction techniques can be used to shrink the state space of system models by hiding redundant information and removing irrelevant details. The reduced state space can then be used for analysis provided it preserves a rich class of properties of interest. This thesis presents reduction techniques for a wide range of nondeterministic and probabilistic models. Our reduction techniques are based on the notions of equivalence relations and layering.Equivalence relations reduce the state space of system models, by aggregating equivalent states into a single state. The reduced state space obtained under an equivalence relation, is called a quotient system. An example equivalence relation that is widely used to reduce the state space of nondeterministic and probabilistic models is bisimulation. On the other hand, layering involves carrying out structural transformations for the systems that are modeled as a network of system models, e.g., distributed systems. As a result of these structural transformations, the new state space obtained is smaller than the original non-layered one. The first part of this thesis focuses on developing new equivalence relations for nondeterministic and Markovian models. For each of these relations, we define a quotient system, investigate its relationship with bisimulation and prove that it preserves interesting linear-time properties. In the second part of this thesis we focus on layering based state space reduction for more expressive specification formalisms that support a stepwise refinement methodology. We develop a framework of layering for modal transition systems and probabilistic versions thereof. This involves a layered composition operator, formulating communication closed layer (CCL) laws and defining a partial order (po) equivalence between modal transition systems. We also prove that the reduced model obtained as a result of applying layered transformation preserves reachability properties. As a result, reachability properties can be checked on the layered, typically smaller, model.To summarize, this thesis presents the theoretical underpinnings of a number of novel reduction techniques for nondeterministic and probabilistic systems.

OpenAccess:
Download fulltext PDF PDF (PDFA)
(additional files)