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

(27)

• 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
• Comparison of algorithms for simple stochastic games
• Constraint Markov chains
• Interval Markov decision processes with multiple objectives: from robust strategies to Pareto curves
• Efficient probabilistic model checking of systems with ranged probabilities
• Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination
• Quantitative analysis 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
• LTL model checking of interval Markov chains
• Model checking of open interval Markov chains
• Interval iteration algorithm for MDPs and IMDPs
• Are parametric Markov chains monotonic?
• Comparing labelled Markov decision processes
• Maximizing entropy over Markov processes
• Stochastic games with lexicographic objectives
• On the complexity of model checking interval-valued discrete time Markov chains
• Entropic risk for turn-based stochastic games
• Opacity for linear constraint Markov chains
• Scalable control synthesis for stochastic systems via structural imdp abstractions
• Approximate verification of the symbolic dynamics of Markov chains
• Tools and Algorithms for the Construction and Analysis of Systems
• Probabilistic timed automata with one clock and initialised clock-dependent probabilities
• Probabilistic timed automata with one clock and initialised clock-dependent probabilities

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)