+**********************************************************************

*

*

*                          Einladung

*

*

*

*                     Informatik-Oberseminar

*

*

*

+**********************************************************************

 

Zeit:  Montag, 27. Mai 2019, 11.00 Uhr

Ort:   Informatikzentrum E3, Raum 9222, Ahornstr. 55

 

Referent:  Souymodip Chakraborty M.Sc.

                   Lehrstuhl Informatik 2

 

Thema: New Results on Probabilistic Verification: Automata, Logic and Satisfiability

 

 

Abstract:

Probabilistic (or quantitative) verification 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 defined 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 understanding 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 satisfiability (or validity) problem of different probabilistic

logics. This includes a bounded fragment of probabilistic logic and a simple quantitative (probabilistic) ex-

tension of mu-calculus. Decision procedures for the satisfiability 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.

Es laden ein: die Dozentinnen und Dozenten der Informatik