Prochain Exposé

Mardi 23 avril, 14h00 en salle Aurigny

Nathalie Bertrand (SUMO)

Long-run satisfaction of path properties

We introduce the concepts of long-run frequency of properties for paths in Kripke structures, and their generalization to long-run probabilities for schedulers in Markov decision processes. The natural associated optimization problem is to compute the optimal values of these measures, when ranging over all paths or all schedulers. For (repeated) reachability and other simple properties, optimal long-run probabilities and corresponding optimal memoryless schedulers are computable in polynomial time. When it comes to constrained reachability properties, memoryless schedulers are no longer sufficient, even in the non-probabilistic setting. Nevertheless, optimal long-run probabilities for constrained reachability are computable in pseudo-polynomial time in the probabilistic setting and in polynomial time for Kripke structures. Finally for co-safety properties expressed by NFA, we give an exponential-time algorithm to compute the optimal long-run frequency, and prove the PSPACE-completeness of the corresponding decision problem.

Joint work with Christel Baier, Jakob Piribauer and Ocan Sankur