New results on probabilistic verification : automata, logic and satisfiability

Chakraborty, Souymodip; Zhang, Lijun; Katoen, Joost-Pieter

doi:HT020111378

New results on probabilistic verification : automata, logic and satisfiability

Chakraborty, Souymodip^RWTH*

2019

Verantwortlichkeitsangabevorgelegt von Souymodip Chakraborty

ImpressumAachen 2019

Umfang1 Online-Ressource (172 Seiten) : Illustrationen

Dissertation, RWTH Aachen University, 2019

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

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

Tag der mündlichen Prüfung/Habilitation
2019-05-27

Online
DOI: 10.18154/RWTH-2019-05211
URL: http://publications.rwth-aachen.de/record/761892/files/761892.pdf

Einrichtungen

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Neue Resultate in Probabilistischer Verifikation: Automaten, Logik und Erfüllbarkeit. Probabilistische (oder quantitative) Verifikation ist ein Teilgebiet der Formalen Methoden, das sich mit stochastischen Modellen und Logiken beschäftigt. Probabilistische Modelle beschreiben das Verhalten randomisierter Algorithmen und anderer physikalischer Systeme, die einer gewissen Unsicherheit unterworfen sind, während probabilistische Logikquantitative Maße über dem Wahrscheinlichkeitsraum eines solchen Modells spezifiziert. In den allermeisten Fällen sind die formalen Techniken, die zur Analyse des Verhaltens probabilistischer Modelle und Logiken eingesetzt werden, mehr als einfache Erweiterungen ihrer nicht-quantitativen Varianten. Vielmehr weisen die resultierenden mathematischen Strukturen eine überraschende Komplexität auf. Das Ziel dieser Arbeit besteht darin, das Verständnis dieser Strukturen grundlegend zu verbessern. Wir beginnen mit der Vorstellung einiger interessanter formaler Darstellungen diskreter stochastischer Modelle. Insbesondere werden wir uns dem Problem der Parametersynthese für parametrische Linearzeit-Temporallogik sowie des Model Checking für konvexe Markov-Entscheidungsprozesse mit offenen Intervallen widmen. Der Schwerpunkt der Arbeit liegt auf dem Erfüllbarkeits- und Gültigkeitsproblem für verschiedene probabilistische Logiken. Letztere umfassen ein beschränktes Fragment der probabilistischen Logik sowie eine einfache quantitative (probabilistische) Erweiterung des mu-Kalküls. Wir entwickeln Entscheidungsprozeduren für die zugehörigen Erfüllbarkeitsprobleme und führen eine detaillierte Komplexitätsanalysedurch. Automaten haben sich als ein äußerst effektives Hilfsmittel für das Verständnis von Logiken erwiesen. Wir führen das neue Konzept derp-Automaten ein, welche eine probabilistische Erweiterung alternierender Baumautomaten darstellen. Wie sich zeigen wird, weist probabilistische Logik sowohl nichtdeterministisches als auch stochastisches Verhalten auf. Daher wird die Semantik von p-Automaten um die Behandlung von Nichtdeterminismus erweitert, so dass auch Markov-Entscheidungsprozesse modelliert werden können.

Probabilistic (or quantitative) verification is a branch of formal methods dealing with stochastic models and logic. Probabilistic models capture the behavior of randomized algorithms and other physical systems with certain uncertainty, whereas probabilistic logic expresses the quantitative measure on the probabilistic space defined by the models. Most often, the formal techniques used in studying the behavior of these models and logic are not just mundane extension of its non-probabilistic counterparts. The complexity of these mathematical structures is surprisingly different. The thesis is an effort at improving our continued under- standing of these models and logic. We will begin by looking at few interesting formal representations of discrete stochastic models. Namely, we will address the parameter synthesis problem for parametric linear time temporal logic and model checking of convex Markov decision processes with open intervals. The primary focus of the thesis is however on the satisfiability (or validity) problem of different probabilistic logics. This includes a bounded fragment of probabilistic logic and a simple quantitative (probabilistic) extension of mu-calculus. Decision procedures for the satisfiability problems are developed and a detailed complexity analysis of these problems is provided. The study of automata has been very effective in understanding logic. We will look at the newly conceived notion of p-automata, which are a probabilistic extension of alternating tree automata. As we will see, probabilistic logic exhibits both non-deterministic and stochastic behavior. The semantics of p-automata are extended to capture non-determinism and hence model Markov decision processes.

OpenAccess:
PDF
(additional files)