Verifying omega-regular properties of probabilistic systems, and simple processes on probabilistic automata

Date: Thursday, October 14, 2010
Speaker: Mathieu Tracol
Venue: TU Wien

Given a probabilistic system M, i.e. a model withprobabilistic transitions, one may be interested to knowwhether execution paths on M satisfy a given propertyphi. When the model is totally observable and phi isomega-regular, the question can be answered using LinearProgramming or Iteration methods.

We focus on the context of partially observed models, theextreme casebeing the model of Probabilistic Automata: the observerhas no feedback on the current state of an executionpath. Most interesting problems become undecidable, thisis the case for instance for the positive Buchi problem:

Given a probabilistic Automata, is there an input wordsuch that with positive probability the associated pathssatisfy a given Buchi condition?

After an preliminary introduction of the probabilisticmodels of Markov Decision Processes and ProbabilisticAutomata, and an overview of the decidability resultsknown so far, we will present the notion of “simpleprocesses”, which allows the definition of probabilisticmodels on which the verification of general omega-regularproperties is decidable. The notion of simple process isinspired by works on the structure of the tail sigma fieldof a non homogeneous Markov chain, and a DecompositionSeparation theorem which generalizes the partition of thestate space of a finite homogeneous Markov chain intoirreducible and transient components, to the context offinite non homogeneous Markov chains.

Posted in RiSE Seminar