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)

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

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)