Characterization and computation of infinite-horizon specifications over Markov processes
From MaRDI portal
(Redirected from Publication:386604)
absorbing setsBellman equationsdiscrete-time Markov processesinfinite-horizon propertiesPCTL model checking
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 work is devoted to the formal verification of specifications over general discrete-time Markov processes, with an emphasis on infinite-horizon properties. These properties, formulated in a modal logic known as PCTL, can be expressed through value functions defined over the state space of the process. The main goal is to understand how structural features of the model (primarily the presence of absorbing sets) influence the uniqueness of the solutions of corresponding Bellman equations. Furthermore, this contribution shows that the investigation of these structural features leads to new computational techniques to calculate the specifications of interest: the emphasis is to derive approximation techniques with associated explicit convergence rates and formal error bounds.
Recommendations
- Regularization of Bellman equations for infinite-horizon probabilistic properties
- Quantitative model-checking of controlled discrete-time Markov processes
- Formal reasoning about finite-state discrete-time Markov chains in HOL
- scientific article; zbMATH DE number 1507207
- Probabilistic model checking of labelled Markov processes via finite approximate bisimulations
Cites work
- scientific article; zbMATH DE number 3858118 (Why is no real title available?)
- scientific article; zbMATH DE number 5016447 (Why is no real title available?)
- scientific article; zbMATH DE number 3539473 (Why is no real title available?)
- scientific article; zbMATH DE number 1022658 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- Adaptive Markov control processes
- Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes
- Approximate model checking of stochastic hybrid systems
- Control Techniques for Complex Networks
- Error bounds for rolling horizon policies in discrete-time Markov control processes
- Foundations of Modern Probability
- General Irreducible Markov Chains and Non-Negative Operators
- Markov Chains with Continuous Components
- Markov chains and stochastic stability
- Metrics for labelled Markov processes
- Model Checking Software
- On finite-state approximants for probabilistic computation tree logic
- On the connections between PCTL and dynamic programming
- Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems
- Quantitative automata model checking of autonomous stochastic hybrid systems
- Regularization of Bellman equations for infinite-horizon probabilistic properties
- Stochastic optimal control. The discrete time case
- Stochastic stability and control
- Three-Valued Abstractions of Markov Chains: Completeness for a Sizeable Fragment of PCTL
- Verification and Control of Hybrid Systems
- Verification of discrete time stochastic hybrid systems: a stochastic reach-avoid decision problem
Cited in
(8)- Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions
- Formal controller synthesis for Markov jump linear systems with uncertain dynamics
- Regularization of Bellman equations for infinite-horizon probabilistic properties
- Probabilistic model checking of labelled Markov processes via finite approximate bisimulations
- Robustly complete finite-state abstractions for verification of stochastic systems
- Quantitative model-checking of controlled discrete-time Markov processes
- Discrete-time hybrid control in Borel spaces: average cost optimality criterion
- Automated verification and synthesis of stochastic hybrid systems: a survey
This page was built for publication: Characterization and computation of infinite-horizon specifications over Markov processes
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q386604)
