The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Probabilistic Büchi automata (PBA) are finite-state acceptors for infinite words where all choices are resolved
by fixed distributions and where the accepted language is defined by the requirement that the measure of the accepting runs is positive. In this work we describe a complementation operator for PBA and a discuss on several algorithmic problems for PBA. All interesting problems, such as checking emptiness or equivalence for PBA or checking whether a finite transition system satisfies a PBA-specification, turn out to be undecidable. An important consequence of these results are several undecidability results for stochastic games with incomplete information, modelled by partially-observable Markov decision processes (POMDP) and w-regular winning objectives.
Furthermore, we study an alternative semantics for PBA where it is required that almost all runs for an accepted word are accepting, which turns out to be less powerful, but has a decidable emptiness problem.
This is a joint work with Christel Baier and Marcus Groesser.