Please use this identifier to cite or link to this item: doi:10.22028/D291-26690
Title: Finite horizon analysis of Markov automata
Author(s): Hatefi Ardakani, Hassan
Language: English
Year of Publication: 2016
SWD key words: Markov-Modell
Markov-Prozess
Stochastischer Automat
Fehleranalyse
Volterra-Integralgleichung
Free key words: Markov automata
quantitative system analysis
formal methods
stochastic process
Markov process
DDC notations: 004 Computer science, internet
Publikation type: Dissertation
Abstract: Markov automata constitute an expressive continuous-time compositional modelling formalism, featuring stochastic timing and nondeterministic as well as probabilistic branching, all supported in one model. They span as special cases, the models of discrete and continuous-time Markov chains, as well as interactive Markov chains and probabilistic automata. Moreover, they might be equipped with reward and resource structures in order to be used for analysing quantitative aspects of systems, like performance metrics, energy consumption, repair and maintenance costs. Due to their expressive nature, they serve as semantic backbones of engineering frameworks, control applications and safety critical systems. The Architecture Analysis and Design Language (AADL), Dynamic Fault Trees (DFT) and Generalised Stochastic Petri Nets (GSPN) are just some examples. Their expressiveness thus far prevents them from efficient analysis by stochastic solvers and probabilistic model checkers. A major problem context of this thesis lies in their analysis under some budget constraints, i.e. when only a finite budget of resources can be spent by the model. We study mathematical foundations of Markov automata since these are essential for the analysis addressed in this thesis. This includes, in particular, understanding their measurability and establishing their probability measure. Furthermore, we address the analysis of Markov automata in the presence of both reward acquisition and resource consumption within a finite budget of resources. More specifically, we put the problem of computing the optimal expected resource-bounded reward in our focus. In our general setting, we support transient, instantaneous and final reward collection as well as transient resource consumption. Our general formulation of the problem encompasses in particular the optimal time-bound reward and reachability as well as resource-bounded reachability. We develop a sound theory together with a stable approximation scheme with a strict error bound to solve the problem in an efficient way. We report on an implementation of our approach in a supporting tool and also demonstrate its effectiveness and usability over an extensive collection of industrial and academic case studies.
Markov-Automaten bilden einen mächtigen Formalismus zur kompositionellen Modellierung mit kontinuierlicher stochastischer Zeit und nichtdeterministischer sowie probabilistischer Verzweigung, welche alle in einem Modell unterstützt werden. Sie enthalten als Spezialfälle die Modelle diskreter und kontinuierlicher Markov-Ketten sowie interaktive Markov-Ketten und probabilistischer Automaten. Darüber hinaus können sie mit Belohnungs- und Ressourcenstrukturen ausgestattet werden, um quantitative Aspekte von Systemen wie Leistungsfähigkeit, Energieverbrauch, Reparatur- und Wartungskosten zu analysieren. Sie dienen aufgrund ihrer Ausdruckskraft als semantisches Rückgrat von Engineering Frameworks, Steuerungsanwendungen und sicherheitskritischen Systemen. Die Architekturanalyse und Designsprache (AADL), Dynamic Fault Trees (DFT) und Generalized Stochastic Petri Nets (GSPN) sind nur einige Beispiele dafür. Ihre Aussagekraft verhindert jedoch bisher eine effiziente Analyse durch stochastische Löser und probabilistische Modellprüfer. Ein wichtiger Problemzusammenhang dieser Arbeit liegt in ihrer Analyse unter Budgetbeschränkungen, das heisst wenn nur ein begrenztes Budget an Ressourcen vom Modell aufgewendet werden kann. Wir studieren mathematische Grundlagen von Markov-Automaten, da diese für die in dieser Arbeit angesprochene Analyse von wesentlicher Bedeutung sind. Dazu gehört insbesondere das Verständnis ihrer Messbarkeit und die Festlegung ihrer Wahrscheinlichkeitsmaßes. Darüber hinaus befassen wir uns mit der Analyse von Markov-Automaten in Bezug auf Belohnungserwerb sowie Ressourcenverbrauch innerhalb eines begrenzten Ressourcenbudgets. Genauer gesagt stellen wir das Problem der Berechnung der optimalen erwarteten Ressourcen-begrenzte Belohnung in unserem Fokus. Dieser Fokus umfasst transiente, sofortige und endgültige Belohnungssammlung sowie transienten Ressourcenverbrauch. Unsere allgemeine Formulierung des Problems beinhalet insbesondere die optimale zeitgebundene Belohnung und Erreichbarkeit sowie ressourcenbeschränkte Erreichbarkeit. Wir entwickeln die grundlegende Theorie dazu. Zur effizienten Lösung des Problems entwerfen wir ein stabilen Approximationsschema mit einer strikten Fehlerschranke. Wir berichten über eine Umsetzung unseres Ansatzes in einem Software-Werkzeug und zeigen seine Wirksamkeit und Verwendbarkeit anhand einer umfangreichen Sammlung von industriellen und akademischen Fallstudien.
Link to this record: urn:nbn:de:bsz:291-scidok-67438
hdl:20.500.11880/26746
http://dx.doi.org/10.22028/D291-26690
Advisor: Hermanns, Holger
Date of oral examination: 20-Dec-2016
Date of registration: 11-Jan-2017
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
thesis.pdf1,11 MBAdobe PDFView/Open


Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.