Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains

DOI10.3233/FI-2009-145zbMath1214.68213OpenAlexW2622039200MaRDI QIDQ3400550

Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, Li-jun Zhang

Publication date: 5 February 2010

Published in: Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.3233/fi-2009-145

zbMATH Keywords

Markov chains, model checking, truncation, uniformization

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (5)

Time-Bounded Verification of CTMCs against Real-Time Specifications ⋮ Precisely deciding CSL formulas through approximate model checking for CTMCs ⋮ Quantitative Analysis of Communication Scenarios ⋮ Probabilistic model checking of biological systems with uncertain kinetic rates ⋮ Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games

Uses Software

• PRISM
• SPIN
• MRMC
• CEGAR

This page was built for publication: Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains