Quantitative model-checking of controlled discrete-time Markov processes

2014/07/21 by Tkachev, Ilya, Mereacre, Alexandru, Katoen, Joost-Pieter +1 · 1 citation
#FOS: Computer and information sciences #FOS: Electrical engineering #FOS: Mathematics #Formal Languages and Automata Theory (cs.FL) #Optimization and Control (math.OC) #Probability (math.PR) #Systems and Control (eess.SY) #electronic engineering #information engineering

paper · doi:10.48550/arxiv.1407.5449

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

Cited by

• Correct-by-Design Control Synthesis of Stochastic Multi-agent Systems: a Robust Tensor-based Solution

Related

• Optimal Continuous Time Markov Decisions
• On reachability of Markov decision processes: a novel state-classification-based PI approach
• Faster Statistical Model Checking for Unbounded Temporal Properties
• Beyond Decisiveness of Infinite Markov Chains
• Efficient Probabilistic Model Checking for Relational Reachability (Extended Version)