Verification of Open Interactive Markov Chains

DOI10.4230/LIPIcs.FSTTCS.2012.474zbMath1354.68170OpenAlexW2243362255MaRDI QIDQ2957522

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

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) Specification and verification (program logics, model checking, etc.) (68Q60) Applications of continuous-time Markov processes on discrete state spaces (60J28) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (5)

Expected reachability-time games ⋮ Model Checking Probabilistic Systems ⋮ A Tutorial on Interactive Markov Chains ⋮ Compositional Design of Stochastic Timed Automata ⋮ The linear time-branching time spectrum of equivalences for stochastic systems with non-determinism

This page was built for publication: Verification of Open Interactive Markov Chains