Quantitative model-checking of controlled discrete-time Markov processes

DOI10.1016/J.IC.2016.11.006MaRDI QIDQ515573zbMATH OpenOpenAlexFDO

Authors Ilya Tkachev, Alexandru Mereacre, Joost-Pieter Katoen, Alessandro Abate

Publication date 16 March 2017

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1407.5449

Mathematics Subject Classification ID

Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• Optimal control of probabilistic discrete event systems on Markov decision processes
• scientific article; zbMATH DE number 1507207
• Model checking probabilistic systems
• Markov decision processes and regular events
• Formal Modeling and Analysis of Timed Systems

Cites work

• scientific article; zbMATH DE number 3128787 (Why is no real title available?)
• scientific article; zbMATH DE number 3844615 (Why is no real title available?)
• scientific article; zbMATH DE number 49674 (Why is no real title available?)
• scientific article; zbMATH DE number 1324455 (Why is no real title available?)
• scientific article; zbMATH DE number 1325008 (Why is no real title available?)
• scientific article; zbMATH DE number 700091 (Why is no real title available?)
• scientific article; zbMATH DE number 1166155 (Why is no real title available?)
• scientific article; zbMATH DE number 2102704 (Why is no real title available?)
• scientific article; zbMATH DE number 794262 (Why is no real title available?)
• scientific article; zbMATH DE number 893883 (Why is no real title available?)
• scientific article; zbMATH DE number 2206109 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 3216771 (Why is no real title available?)
• scientific article; zbMATH DE number 3245885 (Why is no real title available?)
• A Borel measurable version of König's lemma for random paths
• Adaptive Markov control processes
• Approximation of Markov decision processes with general state space
• Characterization and computation of infinite-horizon specifications over Markov processes
• Control Techniques for Complex Networks
• Control design for specifications on stochastic hybrid systems
• Controlled Markov Processes with Arbitrary Numerical Criteria
• Decision Problems with Expected Utility Critera, I: Upper and Lower Convergent Utility
• Decision Problems with Expected Utility Criteria, II: Stationarity
• Defining liveness
• Discrete-Time Controlled Markov Processes with Average Cost Criterion: A Survey
• Error bounds for rolling horizon policies in discrete-time Markov control processes
• Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems
• Foundations of Modern Probability
• Gambling Problems with a Limit Inferior Payoff
• Handbook of Markov decision processes. Methods and applications
• Harmonic analysis of the de Rham complex on the sphere.
• Language-guided controller synthesis for discrete-time linear systems
• Markov chains and stochastic stability
• Markov decision processes and regular events
• Maximizing the probability of attaining a target prior to extinction
• Negative Dynamic Programming
• On the Existence of Good Markov Strategies
• On the Existence of Good Stationary Strategies
• Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems
• Quantitative automata model checking of autonomous stochastic hybrid systems
• Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems
• Reasoning about infinite computations
• Sequential Decision Problems with Expected Utility Criteria. III: Upper and Lower Transience
• Specification-guided controller synthesis for linear systems and safe linear-time temporal logic
• Stochastic optimal control. The discrete time case
• The stochastic processes of Borel gambling and dynamic programming
• The theory of dynamic programming
• Universally Measurable Policies in Dynamic Programming
• Verification and Control of Hybrid Systems
• Verification of discrete time stochastic hybrid systems: a stochastic reach-avoid decision problem

Cited in

(9)

• Robustly complete finite-state abstractions for verification of stochastic systems
• Qualitative controller synthesis for consumption Markov decision processes
• Discrete-time hybrid control in Borel spaces: average cost optimality criterion
• Optimal schedulers vs optimal bases: an approach for efficient exact solving of Markov decision processes
• Automated verification and synthesis of stochastic hybrid systems: a survey
• Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives
• Certified reinforcement learning with logic guidance
• Characterization and computation of infinite-horizon specifications over Markov processes
• Symbolic control for stochastic systems via finite parity games

This page was built for publication: Quantitative model-checking of controlled discrete-time Markov processes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q515573)