Consistency and refinement for interval Markov chains

DOI10.1016/j.jlap.2011.10.003zbMath1247.68195OpenAlexW1972539585MaRDI QIDQ444461

Axel Legay, Mikkel L. Pedersen, Benoît Delahaye, Andrzej Wąsowski, Kim Guldstrand Larsen

Publication date: 14 August 2012

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2011.10.003

zbMATH Keywords

complexitydeterminismMarkov chainrefinementabstraction

Mathematics Subject Classification ID

Markov chains (discrete-time Markov processes on discrete state spaces) (60J10) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items

Unnamed Item, Quantitative analysis of interval Markov chains, Compositionality for quantitative specifications, Consistency in parametric interval probabilistic timed automata

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Markov set-chains
• A logic for reasoning about time and reliability
• Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete
• Counterexample-guided abstraction refinement for symbolic model checking
• Markov Set-Chains as Abstractions of Stochastic Hybrid Systems
• Modal and mixed specifications: key decision problems and their complexities
• Compositional Abstraction for Stochastic Systems
• Validation of Stochastic Systems
• Three-Valued Abstraction for Continuous-Time Markov Chains
• Model-Checking ω-Regular Properties of Interval Markov Chains
• Probabilistic automata
• Model Checking Software
• Tools and Algorithms for the Construction and Analysis of Systems