Quantitative model-checking of controlled discrete-time Markov processes

DOI10.1016/j.ic.2016.11.006zbMath1359.68199arXiv1407.5449OpenAlexW2963907727MaRDI QIDQ515573

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

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) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (5)

Symbolic control for stochastic systems via finite parity games ⋮ Certified reinforcement learning with logic guidance ⋮ Discrete-time hybrid control in Borel spaces: average cost optimality criterion ⋮ Automated verification and synthesis of stochastic hybrid systems: a survey ⋮ Robustly complete finite-state abstractions for verification of stochastic systems

Cites Work

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

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