Approximate Verification of the Symbolic Dynamics of Markov Chains

DOI10.1145/2629417zbMath1321.68367OpenAlexW2021112905MaRDI QIDQ5501948

S. Akshay, P. S. Thiagarajan, Blaise Genest, Manindra Agrawal

Publication date: 14 August 2015

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-00920793/file/AAGT15.pdf

zbMATH Keywords

discretizationMarkov chainsapproximate model checkingLTL logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items

What's decidable about discrete linear dynamical systems? ⋮ Reachability problems for Markov chains ⋮ Unnamed Item ⋮ Complexity of Restricted Variants of Skolem and Related Problems ⋮ Algebraic model checking for discrete linear dynamical systems ⋮ Constrained Markov order surrogates

Uses Software

• PRISM

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Constraint Markov chains
• Markov chains and stochastic stability
• Wielandt's proof of the exponent inequality for primitive nonnegative matrices
• Discrete time Markov chains with interval probabilities
• A theory of timed automata
• A logic for reasoning about time and reliability
• Interval-valued finite Markov chains
• The theory of interval-probability as a unifying concept for uncertainty
• Non-negative matrices and Markov chains.
• Unzerlegbare, nicht negative Matrizen
• Approximate Verification of the Symbolic Dynamics of Markov Chains
• Decision Problems for Interval Markov Chains
• Markov Chains
• Symbolic model checking for probabilistic processes
• An Introduction to Symbolic Dynamics and Coding
• Decision Problems for Linear Recurrence Sequences
• Performance Analysis of Communications Networks and Systems
• LTL Model Checking of Interval Markov Chains
• Model-Checking ω-Regular Properties of Interval Markov Chains
• On stochastic languages
• Symbolic Dynamics
• CONCUR 2003 - Concurrency Theory