TagsArticle Source
Probabilistic Reachability for MDPs
- Gethin Norman (University of Glasgow)
- Theoretical Foundations of Computer Systems Boot Camp
Abstract
In this talk I will outline automated techniques for the verification and control of partially observable probabilistic systems for both discrete and dense models of time. For the discrete-time case, we formally model these systems using partially observable Markov decision processes; for dense time, we propose an extension of probabilistic timed automata in which local states are partially visible to an observer or controller. Quantitative properties of interest, relate to the probability of an event’s occurrence or the expected value of some reward measure. I will present techniques to either verify that such a property holds or to synthesise a controller for the model which makes it true. The approach is based on an integer discretisation of the model’s dense-time behaviour and a grid-based abstraction of the uncountable belief space induced by partial observability. The latter is necessarily approximate since the underlying problem is undecidable, however both lower and upper bounds on numerical results can be generated.