Model-Checking ω-Regular Properties of Interval Markov Chains

DOI10.1007/978-3-540-78499-9_22zbMATH Open1138.68441OpenAlexW1822323017MaRDI QIDQ5458367FDOQ5458367

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

Recommendations

• Tools and Algorithms for the Construction and Analysis of Systems
• On the complexity of model checking interval-valued discrete time Markov chains
• LTL model checking of interval Markov chains
• Model checking of open interval Markov chains
• Quantitative analysis of interval Markov chains

Mathematics Subject Classification ID

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

Cites Work

• Measures of uncertainty in expert systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• The complexity of probabilistic verification
• A logic for reasoning about time and reliability
• Model checking of probabilistic and nondeterministic systems
• Interval-valued finite Markov chains
• Title not available (Why is that?)
• Title not available (Why is that?)
• Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems
• Model Checking Software

Cited In (21)

• Three-valued abstraction for probabilistic systems
• Comparison of algorithms for simple stochastic games
• An active-set strategy to solve Markov decision processes with good-deal risk measure
• Interval Markov decision processes with multiple objectives: from robust strategies to Pareto curves
• Constraint Markov chains
• Approximate Verification of the Symbolic Dynamics of Markov Chains
• Quantitative analysis of interval Markov chains
• Consistency and refinement for interval Markov chains
• Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination
• Interval iteration algorithm for MDPs and IMDPs
• Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities
• Maximizing entropy over Markov processes
• Title not available (Why is that?)
• Stochastic games with lexicographic objectives
• Title not available (Why is that?)
• Entropic risk for turn-based stochastic games
• Opacity for linear constraint Markov chains
• Are Parametric Markov Chains Monotonic?
• Title not available (Why is that?)
• Reachability in parametric interval Markov chains using constraints
• Title not available (Why is that?)

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5458367)