# Quantitative model-checking of controlled discrete-time Markov processes

arXiv: https://arxiv.org/abs/1407.5449 · HTML: https://mlsanity.com/paper/1407.5449/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 21 Jul 2014.

## Built on by (most cited first, 1 of 1)

- [Learning Task Automata for Reinforcement Learning using Hidden Markov Models](https://mlsanity.com/paper/2208.11838/) (2022)

## Abstract (arXiv)

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 ω-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.