arXiv · 1407.5449
Quantitative model-checking of controlled discrete-time Markov processes
Abstract
This paper focuses on optimizing probabilities of events of interest defined over general controlled discrete-time Markov processes. It is shown that the optimization over a wide class of $\omega$-regular properties can be reduced to the solution of one of two fundamental problems: reachability and repeated reachability. We provide a comprehensive study of the former problem and an initial characterisation of the (much more involved) latter problem. A case study elucidates concepts and techniques.
Explore related subjects
Keep this discovery
Ilya Tkachev, Alexandru Mereacre, Joost-Pieter Katoen, Alessandro Abate. 2014-07-21. Quantitative model-checking of controlled discrete-time Markov processes. https://arxiv.org/abs/1407.5449
Cite the original work for its findings. Save a collection to share your selection of sources.