206
2 March 2017 - 16h45
Verification of infinite probabilistic systems
by Paulin Fournier from LABRI, Bordeaux
Abstract: In a first part, I'll give an overview of my phd thesis results on parameterized verification of networks composed of many identical processes. In those networks the number of processes is a parameter, and the processes are modeled by finite probabilistic state machines which interact with messages.
In particular I'll present, with more details, the decidability of the parameterized reachability problem in selective networks, where the messages only reach a subset of the components. This result is obtained thanks to a reduction to a new model of distributed two-player games for which we prove decidability in coNP of the game problem.
In second part, I'll give a brief overview of my current work with Hugo Gimbert on the satisfiability problem for PCTL*.
