Verification of open interactive Markov chains

DOI10.4230/LIPICS.FSTTCS.2012.474MaRDI QIDQ2957522zbMATH OpenOpenAlexFDO

Authors Tomáš Brázdil, Holger Hermanns, Jan Krčál, Jan Křetínský, Vojtěch Řehák

Publication date 26 January 2017

Full work available at URL https://drops.dagstuhl.de/opus/volltexte/2012/3882/pdf/43.pdf/

zbMATH Keywords

discretizationsynthesiscompositional verificationIMCtime-bounded reachability

Mathematics Subject Classification ID

Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Applications of continuous-time Markov processes on discrete state spaces (60J28) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Compositional verification and optimization of interactive Markov chains
• Model Checking Interactive Markov Chains
• The how and why of interactive Markov chains
• scientific article; zbMATH DE number 1397300
• A Tutorial on Interactive Markov Chains

Cited in

(11)

• Compositional design of stochastic timed automata
• Expected reachability-time games
• Model checking probabilistic systems
• Compositional verification and optimization of interactive Markov chains
• A Tutorial on Interactive Markov Chains
• Improving time bounded reachability computations in interactive Markov chains
• Verification of linear duration properties over continuous-time markov chains
• Model checking interactive Markov chains
• The linear time-branching time spectrum of equivalences for stochastic systems with non-determinism
• Model Checking Interactive Markov Chains
• A modest Markov automata tutorial

This page was built for publication: Verification of open interactive Markov chains

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