Model Checking Interactive Markov Chains

DOI10.1007/978-3-642-12002-2_5MaRDI QIDQ3557065zbMATH OpenOpenAlexFDO

Authors Martin Neuhäußer, Lijun Zhang

Publication date 27 April 2010

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-12002-2_5

Mathematics Subject Classification ID

Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Model checking interactive Markov chains
• Model-checking continuous-time Markov chains
• Model checking of open interval Markov chains
• scientific article; zbMATH DE number 1538048
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification of open interactive Markov chains
• Model-checking large structured Markov chains.

Cited in

(22)

• Efficient approximation of optimal control for continuous-time Markov games
• Model checking hyperproperties for Markov decision processes
• The how and why of interactive Markov chains
• Model checking for performability
• Interactive Markov chains. And the quest for quantified quality
• A semantics for every GSPN
• Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games
• Applying Formal Methods: Testing, Performance, and M/E-Commerce
• Compositional verification and optimization of interactive Markov chains
• A Tutorial on Interactive Markov Chains
• Improving time bounded reachability computations in interactive Markov chains
• Quantitative information flow for scheduler-dependent systems
• MeGARA: menu-based game abstraction and abstraction refinement of Markov automata
• Model checking interactive Markov chains
• Verification of open interactive Markov chains
• Model checking compositional Markov systems.
• The linear time-branching time spectrum of equivalences for stochastic systems with non-determinism
• scientific article; zbMATH DE number 1397300 (Why is no real title available?)
• Confluence reduction for Markov automata
• Revisiting interactive Markov chains
• PAC statistical model checking of mean payoff in discrete- and continuous-time MDP
• Model Checking Software

This page was built for publication: Model Checking Interactive Markov Chains

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