Time-bounded model checking of infinite-state continuous-time Markov chains

DOI10.3233/FI-2009-145zbMATH Open1214.68213OpenAlexW2622039200MaRDI QIDQ3400550FDOQ3400550

Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, Lijun 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

Recommendations

• scientific article; zbMATH DE number 2090708
• scientific article; zbMATH DE number 1008397
• scientific article; zbMATH DE number 1864588
• Model-checking continuous-time Markov chains
• scientific article; zbMATH DE number 1670788

zbMATH Keywords

Markov chains, model checking, truncation, uniformization

Mathematics Subject Classification ID

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

Cited In (8)

• Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
• Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games
• CONCUR 2003 - Concurrency Theory
• Quantitative Analysis of Communication Scenarios
• Analysis of timed and long-run objectives for Markov automata
• Time-Bounded Verification of CTMCs against Real-Time Specifications
• Precisely deciding CSL formulas through approximate model checking for CTMCs
• Probabilistic model checking of biological systems with uncertain kinetic rates

Uses Software

• PRISM
• SPIN
• MRMC
• CEGAR

This page was built for publication: Time-bounded model checking of infinite-state continuous-time Markov chains

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