Model checking conditional CSL for continuous-time Markov chains

DOI10.1016/J.IPL.2012.09.009MaRDI QIDQ1941693zbMATH OpenOpenAlexFDO

Authors Yang Gao, Ming Xu, Naijun Zhan, Lijun Zhang

Publication date 21 March 2013

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://backend.orbit.dtu.dk/ws/files/51174796/653F8d01.pdf

zbMATH Keywords

continuous-time Markov chainsformal methodsprobabilistic systemsconditional logiccontinuous stochastic logic

Mathematics Subject Classification ID

Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Probability and inductive logic (03B48) Continuous-time Markov processes on discrete state spaces (60J27) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• CCMC: a conditional CSL model checker for continuous-time Markov chains
• scientific article; zbMATH DE number 1361121
• Efficient CSL model checking using stratification
• Model-checking continuous-time Markov chains
• Automata-based CSL model checking

Cited in

(16)

• Conditional Probabilities over Probabilistic and Nondeterministic Systems
• Multiphase until formulas over Markov reward models: an algebraic approach
• Efficient CSL model checking using stratification
• Probabilistic model checking for energy-utility analysis
• scientific article; zbMATH DE number 1884412 (Why is no real title available?)
• Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
• scientific article; zbMATH DE number 1670788 (Why is no real title available?)
• Automata-based CSL model checking
• An algebraic method to fidelity-based model checking over quantum Markov chains
• Model-checking continuous-time Markov chains
• Energy-utility analysis for resilient systems using probabilistic model checking
• Model checking expected time and expected reward formulae with random time bounds
• Precisely deciding CSL formulas through approximate model checking for CTMCs
• scientific article; zbMATH DE number 2090708 (Why is no real title available?)
• A probabilistic logic for verifying continuous-time Markov chains
• CCMC: a conditional CSL model checker for continuous-time Markov chains

Describes a project that uses

Uses Software

• WSAT

This page was built for publication: Model checking conditional CSL for continuous-time Markov chains

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