# 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

# Exposés des semaines suivantes

Vos propositions sont les bienvenues !

Mardi 28 mai, 14h00 en salle Minquiers

Niki Vazou

Typing, Proofs and Refinements

TBA

Jeudi 6 juin, 14h00 en salle Minquiers

Loic Garoche (ONERA)

TBA

TBA