Model-Checking ω-Regular Properties of Interval Markov Chains

DOI10.1007/978-3-540-78499-9_22MaRDI QIDQ5458367zbMATH OpenOpenAlexFDO

Authors 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)

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

Cites work

• scientific article; zbMATH DE number 5542185 (Why is no real title available?)
• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 3543391 (Why is no real title available?)
• A logic for reasoning about time and reliability
• Interval-valued finite Markov chains
• Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems
• Measures of uncertainty in expert systems
• Model Checking Software
• Model checking of probabilistic and nondeterministic systems
• Quantitative stochastic parity games
• The complexity of probabilistic verification

Cited in

(25)

• Approximate verification of the symbolic dynamics of Markov chains
• Maximizing entropy over Markov processes
• Interval Markov decision processes with multiple objectives: from robust strategies to Pareto curves
• Model checking of open interval Markov chains
• Constraint Markov chains
• Quantitative analysis of interval Markov chains
• An active-set strategy to solve Markov decision processes with good-deal risk measure
• Are parametric Markov chains monotonic?
• Opacity for linear constraint Markov chains
• Entropic risk for turn-based stochastic games
• Efficient probabilistic model checking of systems with ranged probabilities
• LTL model checking of interval Markov chains
• Probabilistic disclosure: maximisation vs. minimisation
• Consistency and refinement for interval Markov chains
• Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination
• Three-valued abstraction for probabilistic systems
• Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination
• Probabilistic timed automata with one clock and initialised clock-dependent probabilities
• Probabilistic timed automata with one clock and initialised clock-dependent probabilities
• Tools and Algorithms for the Construction and Analysis of Systems
• On the complexity of model checking interval-valued discrete time Markov chains
• Comparison of algorithms for simple stochastic games
• Comparison of algorithms for simple stochastic games
• Stochastic games with lexicographic objectives
• Interval iteration algorithm for MDPs and IMDPs

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)