CSL model checking algorithms for QBDs

DOI10.1016/J.TCS.2007.05.007zbMATH Open1159.68481OpenAlexW2107737377MaRDI QIDQ995462FDOQ995462

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

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

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)

Cites Work

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

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

Uses Software

• PRISM
• MRMC

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)