Positivity-Hardness and Saturation Points in Markov Decision Processes

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Positivity-Hardness and Saturation Points in Markov Decision Processes

Vortrag von Jakob Piribauer
The Positivity problem for linear recurrence sequences is a number-theoretic decision problem whose decidability has been open for many decades. We show that this Positivity problem can be encoded into several optimization problems on Markov decision processes, a standard model combining non-deterministic and probabilistic behavior. This reduction demonstrates the inherent mathematical difficulty of various problems in the formal verification of probabilistic systems.

For naturally restricted versions of most of these problems, we can nevertheless establish decidability. The key ingredient is the existence of so-called saturation points which can be seen as bounds on the memory required for an optimal strategy in the Markov decision process.


The talk will be approximately 45 minutes long and takes place online. To access the talk use the following links:

If you have a ZIH-login:

https://selfservice.zih.tu-dresden.de/l/link.php?meeting_id=42224&pin=4c120949


If you do not have a ZIH-login:

https://selfservice.zih.tu-dresden.de/link.php?meeting_id=42224&pin=d3219e91