Monotonicity in Markov models

Spel, Jip Josephine; Petrov, Tatjana; Katoen, Joost-Pieter

doi:HT030626337

Monotonicity in Markov models

Spel, Jip Josephine^RWTH*

2023 & 2024

Verantwortlichkeitsangabevorgelegt von Jip Spel, M.Sc.

ImpressumAachen : RWTH Aachen University 2023

Umfang1 Online-Ressource : Illustrationen

Dissertation, RWTH Aachen University, 2023

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2024

Genehmigende Fakultät
Fak01

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

Tag der mündlichen Prüfung/Habilitation
2023-07-07

Online
DOI: 10.18154/RWTH-2023-11664
URL: https://publications.rwth-aachen.de/record/974903/files/974903.pdf

Einrichtungen

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
In vielen Systemen treten Formen von Wahrscheinlichkeiten auf, unter anderem in Kommunikationsprotokollen, Zufallsprotokollen und biologischen Systemen vor. Solche Systeme können wir als Markow-Modelle modellieren, und anhand einer Spezifikation in (einer probabilistischen Erweiterung der) lineare temporalen Logik (LTL) oder baumbasierten temporalen Logik (CTL) verifizieren. Das Ziel ist die Berechnung der Wahrscheinlichkeit oder der erwarteten Gesamtkosten für das Erreichen eines der Teilzuständen. Die Wahrscheinlichkeiten in einem Markow-Modell werden oft als ein exakter Wert angegeben. In der Praxis sind diese Wahrscheinlichkeiten jedoch nicht genau bekannt, sondern liegen in einem Intervall. Außerdem können diese Wahrscheinlichkeiten von anderen Wahrscheinlichkeiten abhängen. Deshalb konzentrieren wir uns auf parametrische Markow-Modelle, in denen die Wahrscheinlichkeiten symbolisch durch Parameter in rationalen Funktionen dargestellt werden. In dieser Arbeit konzentrieren wir uns auf parametrische Markow-Ketten (pMCs) und parametrische Markow-Entscheidungsprozesse (pMDPs). Beide Arten von Markow-Modellen haben eine endliche Menge von Zuständen, von denen einer den Ausgangszustand darstellt, und einer oder mehrere Zielzustände sind. Die Übergänge zwischen den Zuständen werden mit einer parametrischen Wahrscheinlichkeitsfunktion gekennzeichnet. Bei pMCs ist diese Funktion für alle Zustände deterministisch; bei pMDPs kann diese Funktion auch für einige Zustände nicht-deterministisch sein. Eines der Probleme, das wir in dieser Arbeit analysieren, ist das sogenannte

Many systems exhibit probabilistic behavior, such as randomized protocols, communication protocols, or biological systems. Probabilistic model checking is a common way to analyze these type of systems. We often model these systems as Markov models and check them against a specification typically given in a probabilistic extension of LTL or CTL. One of the main goals is to analyze the probability to reach or the expected total reward upon reaching a set of target states. When checking for these properties, we assume probabilities to be fixed constants. In practice, however, these probabilities are often not fixed but bounded to a given interval. Moreover, these probabilities can be dependent on other probabilities. Therefore, we consider parametric Markov models, in which the probabilities are given symbolically by rational functions over parameters. We focus on parametric Markov chains (pMCs) and parametric Markov decision processes (pMDPs). Both models have a finite set of states, of which one is the initial state, and one or more are the target states. The transitions are given by a parametric transition function. PMCs have a deterministic transition function, whereas for pMDPs the transition function might be non-deterministic. One problem addressed when analyzing parametric Markov models is the almost- optimal synthesis problem, i.e., finding a parameter instantiation such that the expected total reward is

OpenAccess:
PDF
(additional files)