Abstraction and refinement of probabilistic automata using modal stochastic games

Sher, Falak; Zhang, Lijun; Katoen, Joost-Pieter

doi:HT018628064

Abstraction and refinement of probabilistic automata using modal stochastic games = Abstraktion und Verfeinerung von probabilistischen Automaten mit modalen stochastischen Spielen

Sher, Falak

2015

VerantwortlichkeitsangabeFalak Sher

ImpressumAachen : Fachgruppe Informatik, RWTH Aachen University 2015

UmfangVIII, 105 S. : graph. Darst.

ReiheAachener Informatik-Berichte ; 2015,10

Dissertation, RWTH Aachen University, 2015

Auch veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor)^RWTH* ; Zhang, Lijun (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2015-04-24

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

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Abstraction (frei) ; Alternating Simulation (frei) ; Informatik (frei) ; Probabilistic Automata (frei) ; Probabilistic Game Automata (frei) ; Refinement (frei) ; Stochastic Games (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Formale Methoden sind mathematische Techniken, die in der Entwicklung zuvelässiger Systeme angewandt werden. Ihre Anwendung garantiert korrekte Spezifikationen und fehlerfreie Implementierungen von Systemen dadurch, dass Garantien für funktionale Anforderungen und probabilistisches Verhaltengegeben werden, zum Beispiel bezüglich Performanz, Zuverlässigkeit usw. Model Checking is einesolche Technik die systematisch und vollständig alle möglichen Systemkonfigurationen eine Systemmodels untersucht um bestimmte Eigenschaften zu verifizieren. Eine der Herausforderungen für diesen Ansatz ist es, effiziente Algorithmen zu entwerfen um alle möglichen Systemkonfigurationen zu untersuchen. Die Anzahl an Zuständen für realistische Systeme ist im Allgemeinen extrem hoch und manchmal sogar unendlich - dies ist bekannt als die Explosion des Zustandsraumes. Dieses Problem schränkt die Anwendbarkeit von Model Checking ein.Abstraktion ist eine Reduzierungstechnik welche Informationen aus dem Systemmodell entfernt, welcheirrelevant für die untersuchte Eigenschaft sind; konsequenterweise wird zuätzliches Verhalten hinzugefügt. Das abstrakte Modell über- und/oder unterapproximiert das Verhalten konkreter Modelle. Zum Beispiel, existentielle abstrakte Modelle wie Segalas probabilistische Automaten (PA) überapproximieren das Verhalten konkreter Modelle während modale abstrakt Modelle es über- und unterapproximieren. Spielbasierte Modelle, wie zum Beispiel Condon’s stochastische Spiele (SGs), unterscheiden sich dadurch dass sie das Verhalten abstrakter Prozesse (kontrolliert durch Spieler 2) von dem konkreten Verhalten (kontrolliert durch Spieler 1) getrennt wird. Sowohl modale und spielbasierte Abstraktionsmodelle ermöglichen es, Erreichbarkeitswahrscheinlichkeiten in konkreten Modellen von unten und oben zubeschränken. Tatsächlich konstruieren Abstraktionsverfeinerungsalgorithmen initial gröbere abstrakteModelle und verfeinern diese dann schrittweise bis die Grenzen für Erreichbarkeitswahrscheinlichkeiten ausreichend genau sind. Wir kombinieren die Techniken modaler und spielbasierter Abstraktion in orthogonaler Art und Weise. Dies ergibt modale stochastische Spiele wo Spieler 2 vollständig das Verhalten kontrolliert, welchesdurch Abstraktion entsteht, während Spieler 1 Verhalten kontrolliert, welches durch Abstraktion unddurch das konkrete Modell entsteht. Durch dieses zusätzliche nichtdeterministische Verhalten in Spieler1-Zuständen sind Grenzen für Errreichbarkeitswahrscheinlihkeiten in modalen stochastischen Spielenmindestens so genau wie in stochastischen Spielen, während modale Spiele vergleichsweise kleiner sind. Zudem ist unsere modale spielbasierte Abstraction kompositionell in dem Sinne, dass einzelne Komponenten auch einzeln abstrahiert und dann zusammengefügt werden können, was ein Gesamtmodell des Systems ergibt. Vorhandene Abstraktionstechniken aus der Literatur sind zustandsbasiert. Das heißt, abstrakte Modelleleiten ihre Transitionen von denen konkreter Zustände ab und simulieren daher schrittweise konkreteModelle. Wir nutzen aus, dass probabilistische Systeme nicht nur stochastische Prozesse sind sondernauch Wahrscheinlichkeitstransformer und behandeln Verteilungen über Zuständen (anstatt Zuständen) als Bürger erster Klasse und heben das Konzept der Abstraktion von Zuständen auf Verteilungen überZuständen. Außerdem definieren wir (alternierende) Simulationsrelationen zwischen konkreten und abstrakten Modellen. Wir zeigen, dass spielbasierte Abstraktion nicht die optimale Strategie ist um extreme Erreichbarkeitswahrscheinlichkeiten zu erhalten. Darüber hinaus zeigen wir, dass unsere verteilungsbasierte Abstraktion präzisere und prägnantere Modelle erzeugen kann als zustandsbasierte Abstraktion. Schlußendlich stellen wir ein zustandsbasiertes und ein verteilungsbasiertes Abstraktionsverfeinerungs-Rahmenwerk für PAs vor. Es verfeinert ein modales stochastisches Spiel in zwei geschachtelten Schleifen. Die innere Schleife verfeinert schrittweise Spieler 1-Zustände solange bis nichtdeterministisches Verhalten induziert durch den Abstraktionsprozess keinen Einfluss mehr auf Erreichbarkeitswahrscheinlichkeiten von Spieler 2-Zuständen hat. Die aüßere Schleife verfeinert Spieler 2-Zustände bis ihre Erreichbarkeitswahrscheinlichkeit die von zugehörigen Zuständen innerhalb eines bestimmten Bereiches beschränkt. Dies ergibt die kleinste mögliche modale Abstraktion für eine gegebene Zustandspartitionierung, welche Erreichbarkeitswahrscheinlichkeiten innerhalb eines bestimmten Bereiches beschränkt.

Formal methods are mathematical techniques used in the development of trustworthy ICT systems. Their application ensures correct specifications and error-free implementations of systems providing guarantees on their functional requirements and probabilistic behaviours, e.g., performance, reliability, etc. Model checking is one of such techniques that systematically and exhaustively explores all possible configurations of systems' models to verify certain properties. One of the challenges faced by this approach is to design efficient algorithms for exploring all configurations of systems' model. The number of states for realistic systems is usually extremely high and sometimes even infinitely-many - known as the state space explosion problem. This problem restricts the applicability of model checking algorithms. Abstraction is a reduction technique that removes information from system models irrelevant to the property of interest; and consequently induces additional behaviour. The abstract models over- and/or under-approximate the behaviour of concrete models. For example, existential abstract models like Segala's probabilistic automata (PA) over-approximate while modal abstract models over- and under-approximate the behaviour of concrete models. The game-based abstract models, such as Condon's stochastic games (SGs), are different in a sense that they keep the behaviour from the abstraction process (handled by, say, player-two) separate from the concrete behaviour (handled by, say, player-one). Both modal and game-based abstract models allow for bounding the reachability probabilities in concrete models from below and from above. In fact, abstraction-refinement algorithms initially construct coarser abstract models and then gradually refine them until the bounds on the reachability probabilities of concrete models are sufficiently tight. We orthogonally combine the techniques of modal and game-based abstractions. This yields modal stochastic games in which player-two completely handles behaviour induced by abstraction whereas player-one handles behaviour induced by abstraction and from concrete models. Due to this additional non-deterministic behaviour in player-one states, bounds on reachability probabilities in modal stochastic games are at most as tight as in stochastic games, but modal games are comparatively smaller in size. Moreover, our modal game-based abstraction is compositional in a sense that individual components can be abstracted separately and then plugged together constituting an overall model of a system. Existing abstraction techniques in the literature are state-based. That is to say, abstract models derive their transitions from that of the concrete states and, thus, simulate concrete models in a step-wise manner. Exploiting the fact that probabilistic systems are not just stochastic processes but transformers of probabilities as well, we treat distributions over states (rather than states) as first-class citizens and lift the notion of abstraction from states to distributions over states. We also define (alternating) simulation relations between concrete and abstract models. We show that game-based abstraction is not the optimal abstraction preserving extremal reachability probabilities. Furthermore, we illustrate that our distribution-based abstraction may induce more precise and concise models than state-based abstraction. Finally, we propose a state-based and a distribution-based abstraction-refinement framework for PA. It refines a modal stochastic game in two nested loops. The inner-loop iteratively refines player-one states until the effect of non-deterministic behaviour induced in them by the abstraction process has no impact anymore on the reachability probabilities of player-two states. The outer-loop refines player-two states until their reachability probabilities bound that of their corresponding concrete states within a certain given range. This yields the smallest possible modal abstraction for a given state-space partitioning, that bounds the reachability probabilities of concrete model within a given range.

OpenAccess:
PDF PDF (PDFA)
(additional files)