Model checking conditional CSL for continuous-time Markov chains

Publication: Research - peer-reviewJournal article – Annual report year: 2013

Documents

DOI

View graph of relations

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
Publication date2013
Volume113
Issue1-2
Pages44-50
ISSN0020-0190
DOIs
StatePublished
CitationsWeb of Science® Times Cited: 1

Keywords

  • Formal methods, Probabilistic systems, Continuous-time Markov chains, Continuous stochastic logic, Conditional logic
Download as:
Download as PDF
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
Word

Download statistics

No data available

ID: 51174793