+**********************************************************************
*
*
* 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 di fferent. The thesis is an eff ort 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 di fferent 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 e ffective 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