Model checking nondeterministic and randomly timed systems

Neuhäußer, Martin R.; Katoen, Joost-Pieter

doi:HT016251507

Model checking nondeterministic and randomly timed systems = Modellüberprüfung für nichtdeterministische Systeme mit zufallsgesteuertem Zeitverhalten

Neuhäußer, Martin R. (Author)

2010

Verantwortlichkeitsangabevorgelegt von Marin R. Neuhäußer

ImpressumEnschede : Univ. Twente 2010

UmfangOnline-Ressource

ISBN978-90-365-2975-4

ReiheIPA dissertation series ; 2010-02

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

Zsfassung in engl. und dt. Sprache. - Weitere Reihe: CTIT Ph. D. thesis series ; 09-165

Genehmigende Fakultät
Fak01

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

Tag der mündlichen Prüfung/Habilitation
2010-01-25

Online
URN: urn:nbn:de:hbz:82-opus-31369
URL: https://publications.rwth-aachen.de/record/51599/files/Neuhaeusser_Martin.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Markov-Kette (Genormte SW) ; Maßtheorie (Genormte SW) ; Model Checking (Genormte SW) ; continuous-time Markov chain (frei) ; continuous-time Markov decision process (frei) ; exponentially distributed delay (frei) ; measure theory (frei) ; model checking (frei) ; nondeterminism (frei) ; Nichtdeterminismus (frei) ; stochastische Optimierung (frei) ; Informatik (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Quantitatives Model Checking ist zu einem weit verbreiteten Werkzeug für die Analyse von Leistungs- und Verlässlichkeitscharakteristiken geworden. Die bisher bekannten Model Checking Verfahren unterstützen jedoch keine Modelle, die stochastisches Zeitverhalten und Nichtdeterminismus verbinden. Das ist überraschend, da Nichtdeterminismus der Schlüssel für kompositionelle Modellierungstechniken ist und in verteilten Systemen häufig vorkommt. Die vorliegende Arbeit untersucht zeitkontinuierliche Markov-Entscheidungsprozesse, die eine Modellklasse bilden, die stochastisches Zeitverhalten und Nichtdeterminismus verbindet. Unser Hauptbeitrag ist ein Diskretisierungsverfahren, das es erlaubt, die maximalen und minimalen Wahrscheinlichkeiten für das Erreichen einer Zielzustandsmenge innerhalb einer CTMDP zu berechnen.

Quantitative model checking has become an indispensable tool to analyze performance and dependability characteristics such as the expected round trip time in a packet switched network or the failure probability of a safety-critical system. So far, the existing model checking techniques lack support for models which combine stochastic timing and nondeterminism. This is surprising, as nondeterminism is the key for compositional modeling and occurs naturally in distributed systems. In this thesis, we overcome this limitation. More precisely, we consider continuous-time Markov decision processes (CTMDPs), a model which closely entangles stochasticity and nondeterminism. Our main contribution is a discretization which allows to compute the maximum and minimum probability to enter a set of goal states in a CTMDP within a given time-bound. By applying value iteration techniques to the induced discrete-time model, we compute the desired probabilities up to an a priori specified precision. This result provides the basis for model checking important performance and dependability characteristics and has been extended to a variety of other nondeterministic and randomly timed system models. We demonstrate the applicability of our techniques by a number of case studies which also show that nondeterministic modeling makes an essential difference in the area of performance and dependability evaluation.

Fulltext:
PDF