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

DOI10.3233/FI-2009-145MaRDI QIDQ3400550zbMATH OpenOpenAlexFDO

Authors 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

zbMATH Keywords

Markov chains, model checking, truncation, uniformization

Mathematics Subject Classification ID

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

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

Cited in

(9)

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

Describes a project that uses

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)