Characterization and computation of infinite-horizon specifications over Markov processes

DOI10.1016/J.TCS.2013.09.032zbMATH Open1293.68194arXiv1211.4346OpenAlexW1980146067MaRDI QIDQ386604FDOQ386604

Authors: Ilya Tkachev, Alessandro Abate 

Publication date: 10 December 2013

Published in: Theoretical Computer Science (Search for Journal in Brave)

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.

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

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

zbMATH Keywords

absorbing setsBellman equationsdiscrete-time Markov processesinfinite-horizon propertiesPCTL model checking

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?)
• Title not available (Why is that?)
• Foundations of Modern Probability
• Markov chains and stochastic stability
• Stochastic stability and control
• General Irreducible Markov Chains and Non-Negative Operators
• Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems
• Title not available (Why is that?)
• Stochastic optimal control. The discrete time case
• Title not available (Why is that?)
• Verification and Control of Hybrid Systems
• Title not available (Why is that?)
• Metrics for labelled Markov processes
• Adaptive Markov control processes
• Control Techniques for Complex Networks
• Verification of discrete time stochastic hybrid systems: a stochastic reach-avoid decision problem
• Error bounds for rolling horizon policies in discrete-time Markov control processes
• On finite-state approximants for probabilistic computation tree logic
• Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes
• On the connections between PCTL and dynamic programming
• Quantitative automata model checking of autonomous stochastic hybrid systems
• Regularization of bellman equations for infinite-horizon probabilistic properties
• Three-Valued Abstractions of Markov Chains: Completeness for a Sizeable Fragment of PCTL
• Markov Chains with Continuous Components
• Model Checking Software
• Approximate model checking of stochastic hybrid systems

Cited In (7)

• Robustly complete finite-state abstractions for verification of stochastic systems
• Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations
• Discrete-time hybrid control in Borel spaces: average cost optimality criterion
• Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions
• Automated verification and synthesis of stochastic hybrid systems: a survey
• Quantitative model-checking of controlled discrete-time Markov processes
• Formal controller synthesis for Markov jump linear systems with uncertain dynamics

Uses Software

• PRISM
• MRMC

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)