Efficient CSL model checking using stratification

DOI10.2168/LMCS-8(2:17)2012MaRDI QIDQ2904612zbMATH OpenWikidataFDO

Authors David N. Jansen, Flemming Nielson, Holger Hermanns, Lijun Zhang

Publication date 15 August 2012

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2168/LMCS-8(2:17)2012

zbMATH Keywords

approximation algorithmcontinuous stochastic logiccontinuous-time Markov chainsmodel checkingstratification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Approximation algorithms (68W25)

Recommendations

• Automata-based CSL model checking
• Precisely deciding CSL formulas through approximate model checking for CTMCs
• CCMC: a conditional CSL model checker for continuous-time Markov chains
• Model checking conditional CSL for continuous-time Markov chains
• scientific article; zbMATH DE number 1670788

Cited in

(9)

• Model checking conditional CSL for continuous-time Markov chains
• Time-bounded termination analysis for probabilistic programs with delays
• Statistical verification of PCTL using antithetic and stratified samples
• Precisely deciding CSL formulas through approximate model checking for CTMCs
• Automata-based CSL model checking
• CCMC: a conditional CSL model checker for continuous-time Markov chains
• Checking continuous stochastic logic against quantum continuous-time Markov chains
• Multiphase until formulas over Markov reward models: an algebraic approach
• CSL model checking algorithms for QBDs

Describes a project that uses

Uses Software

• MRMC

This page was built for publication: Efficient CSL model checking using stratification

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