CSL model checking algorithms for QBDs

DOI10.1016/J.TCS.2007.05.007MaRDI QIDQ995462zbMATH OpenOpenAlexFDO

Authors Anne Remke, B. 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

transient analysismodel checkingcontinuous-time Markov chainsuniformizationCSLinfinite-statequasi-birth death processes

Mathematics Subject Classification ID

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

Recommendations

• Theory and Applications of Satisfiability Testing
• \(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers
• Automata-based CSL model checking
• Model Checking Quantified Computation Tree Logic
• CTL Model-Checking with Graded Quantifiers
• Quantified CTL: expressiveness and model checking (extended abstract)
• Compositional and quantitative model checking (extended abstract)
• Efficient CSL model checking using stratification
• scientific article; zbMATH DE number 2163033

Cites work

• scientific article; zbMATH DE number 1670870 (Why is no real title available?)
• scientific article; zbMATH DE number 3736680 (Why is no real title available?)
• scientific article; zbMATH DE number 1956509 (Why is no real title available?)
• scientific article; zbMATH DE number 2038771 (Why is no real title available?)
• scientific article; zbMATH DE number 956814 (Why is no real title available?)
• A logarithmic reduction algorithm for quasi-birth-death processes
• Approximated Transient Queue Length and Waiting Time Distributions via Steady State Analysis
• CONCUR 2004 - Concurrency Theory
• Model-checking continuous-time Markov chains
• Model-checking large structured Markov chains.
• STACS 2005
• STACS 2005
• Symbolic model checking with rich assertional languages
• The Randomization Technique as a Modeling Tool and Solution Procedure for Transient Markov Processes
• Tools and Algorithms for the Construction and Analysis of Systems
• Transient analysis of quasi-birth-death processes

Cited in

(5)

• An analytical model for end-to-end communication channel over PLCN based on QBDs
• CSL Model Checking Algorithms for Infinite-State Structured Markov Chains
• Tools and Algorithms for the Construction and Analysis of Systems
• A Uniformization-Based Algorithm for Model Checking the CSL Until Operator on Labeled Queueing Networks
• Performance analysis for (X,S)-bottleneck cell in large-scale wireless networks

Describes a project that uses

Uses Software

• MRMC
• PRISM

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

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