Probabilistic PCTL*: The deductive way
- Day - Time: 03 October 2016, h.10:00
- Place: Area della Ricerca CNR di Pisa - Room: C-29
Speakers
- Luis Ferrer Fioriti (Dependable Systems and Software group, Saarland University, Saarbreucken, Germany)
Referent
Abstract
Complex probabilistic temporal behaviours need to be guaranteed in robotics and various other control domains, as well as in the context of families of randomized protocols. At its core, this entails checking infinite-state probabilistic systems with respect to quantitative properties specified in probabilistic temporal logics. Model checking methods are not directly applicable to infinite-state systems, and techniques for infinite-state probabilistic systems are limited in terms of the specifications they can handle.
We present a deductive approach to the verification of countable-state systems against properties specified in probabilistic CTL*, on models featuring both nondeterministic and probabilistic choices. The deductive proof system we propose lifts the classical proof system by Kesten and Pnueli to the probabilistic setting. However, the soundness arguments are completely distinct and go via the theory of martingales. Completeness results for the weakly finite case illustrate the theoretical effectiveness of our approach.
This is joint work with Rayna Dimitrova, Holger Hermanns and Rupak Majumdar.