Characterization and computation of infinite-horizon specifications over Markov processes

DOI10.1016/j.tcs.2013.09.032zbMath1293.68194arXiv1211.4346OpenAlexW1980146067MaRDI QIDQ386604

Alessandro Abate, Ilya Tkachev

Publication date: 10 December 2013

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

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

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

Related Items (6)

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

Uses Software

• PRISM
• MRMC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Metrics for labelled Markov processes
• Verification of discrete time stochastic hybrid systems: a stochastic reach-avoid decision problem
• Approximate model checking of stochastic hybrid systems
• Markov chains and stochastic stability
• Stochastic optimal control. The discrete time case
• Adaptive Markov control processes
• Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems
• Stochastic stability and control
• 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
• General Irreducible Markov Chains and Non-Negative Operators
• Verification and Control of Hybrid Systems
• Markov Chains with Continuous Components
• Foundations of Modern Probability
• Error bounds for rolling horizon policies in discrete-time Markov control processes
• Control Techniques for Complex Networks
• Model Checking Software

This page was built for publication: Characterization and computation of infinite-horizon specifications over Markov processes