Quantitative model-checking of controlled discrete-time Markov processes

DOI10.1016/J.IC.2016.11.006zbMATH Open1359.68199arXiv1407.5449OpenAlexW2963907727MaRDI QIDQ515573FDOQ515573

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

Publication date: 16 March 2017

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

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.

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

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

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)

Cites Work

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

Cited In (7)

• 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
• 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
• 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)