Model checking conditional CSL for continuous-time Markov chains

Yang Gao, Ming Xu, Naijun Zhan, Lijun Zhang

Research output: Contribution to journalJournal articleResearchpeer-review

512 Downloads (Pure)


In this paper, we consider the model-checking problem of continuous-time Markov chains (CTMCs) with respect to conditional logic. To the end, we extend Continuous Stochastic Logic introduced in Aziz et al. (2000) [1] to Conditional Continuous Stochastic Logic (CCSL) by introducing a conditional probabilistic operator. CCSL allows us to express a richer class of properties for CTMCs. Based on a parameterized product obtained from the CTMC and an automaton extracted from a given CCSL formula, we propose an approximate model checking algorithm and analyse its complexity.
Original languageEnglish
JournalInformation Processing Letters
Issue number1-2
Pages (from-to)44-50
Publication statusPublished - 2013


  • Formal methods
  • Probabilistic systems
  • Continuous-time Markov chains
  • Continuous stochastic logic
  • Conditional logic

Cite this