Model-Checking ω-Regular Properties of Interval Markov Chains

DOI10.1007/978-3-540-78499-9_22zbMath1138.68441OpenAlexW1822323017MaRDI QIDQ5458367

Krishnendu Chatterjee, Koushik Sen, Thomas A. Henzinger

Publication date: 11 April 2008

Published in: Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-78499-9_22

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (18)

Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities ⋮ Interval iteration algorithm for MDPs and IMDPs ⋮ Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination ⋮ Quantitative analysis of interval Markov chains ⋮ Consistency and refinement for interval Markov chains ⋮ Three-valued abstraction for probabilistic systems ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Maximizing entropy over Markov processes ⋮ Unnamed Item ⋮ Are Parametric Markov Chains Monotonic? ⋮ Opacity for linear constraint Markov chains ⋮ Approximate Verification of the Symbolic Dynamics of Markov Chains ⋮ Constraint Markov chains ⋮ Reachability in parametric interval Markov chains using constraints ⋮ Unnamed Item ⋮ An active-set strategy to solve Markov decision processes with good-deal risk measure ⋮ Comparison of algorithms for simple stochastic games

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A logic for reasoning about time and reliability
• Interval-valued finite Markov chains
• Measures of uncertainty in expert systems
• Model checking of probabilistic and nondeterministic systems
• The complexity of probabilistic verification
• Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems
• Model Checking Software

This page was built for publication: Model-Checking ω-Regular Properties of Interval Markov Chains