CSL model checking algorithms for QBDs

DOI10.1016/J.TCS.2007.05.007zbMath1159.68481OpenAlexW2107737377MaRDI QIDQ995462

Anne Remke, Boudewijn R. Haverkort, Lucia Cloth

Publication date: 3 September 2007

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2007.05.007

zbMATH Keywords

uniformizationmodel checkingcontinuous-time Markov chainstransient analysisCSLinfinite-statequasi-birth death processes

Mathematics Subject Classification ID

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

Related Items (2)

Performance analysis for \((X,S)\)-bottleneck cell in large-scale wireless networks ⋮ An analytical model for end-to-end communication channel over PLCN based on QBDs

Uses Software

• PRISM
• MRMC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model-checking large structured Markov chains.
• The Randomization Technique as a Modeling Tool and Solution Procedure for Transient Markov Processes
• Transient analysis of quasi-birth-death processes
• A logarithmic reduction algorithm for quasi-birth-death processes
• CONCUR 2004 - Concurrency Theory
• Approximated Transient Queue Length and Waiting Time Distributions via Steady State Analysis
• Tools and Algorithms for the Construction and Analysis of Systems
• STACS 2005
• STACS 2005
• Model-checking continuous-time Markov chains
• Symbolic model checking with rich assertional languages

This page was built for publication: CSL model checking algorithms for QBDs