Positivity-Hardness and Saturation Points in Markov Decision Processes
Aus International Center for Computational Logic
Positivity-Hardness and Saturation Points in Markov Decision Processes
Vortrag von Jakob Piribauer
- Veranstaltungsort: online
- Beginn: 5. November 2020 um 13:00
- Ende: 5. November 2020 um 14:30
- Event series: Research Seminar Logic and AI
- iCal
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: