CCMC: A conditional CSL model checker for continuous-time Markov chains

Yang Gao; Ernst Moritz Hahn; Naijun Zhan; Lijun Zhang

doi:10.1007/978-3-319-02444-8_36

CCMC: A conditional CSL model checker for continuous-time Markov chains

Yang Gao, Ernst Moritz Hahn, Naijun Zhan, Lijun Zhang

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

1 Citation (Scopus)

Abstract

We present CCMC (Conditional CSL Model Checker), a model checker for continuous-time Markov chains (CTMCs) with respect to properties specified in continuous-time stochastic logic (CSL). Existing CTMC model checkers such as PRISM or MRMC handle only binary CSL until path formulas. CCMC is the first tool that supports algorithms for analyzing multiple until path formulas. Moreover, CCMC supports a recent extension of CSL - conditional CSL - which makes it possible to verify a larger class of properties on CTMC models. Our tool is based on our recent algorithmic advances for CSL, that construct a stratified CTMC before performing transient probability analyses. The stratified CTMC is a product obtained from the original CTMC and an automaton extracted from a given formula, aiming to filter out the irrelevant paths and make the computation more efficient.

Original language	English
Title of host publication	Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Proceedings
Pages	464-468
Number of pages	5
DOIs	https://doi.org/10.1007/978-3-319-02444-8_36
Publication status	Published - 2013
Externally published	Yes
Event	11th International Symposium on Automated Technology for Verification and Analysis - Hanoi, Viet Nam Duration: 15 Oct 2013 → 18 Oct 2013 Conference number: 11

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	8172 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	11th International Symposium on Automated Technology for Verification and Analysis
Abbreviated title	ATVA 2013
Country	Viet Nam
City	Hanoi
Period	15/10/13 → 18/10/13

Access to Document

10.1007/978-3-319-02444-8_36

Link to publication in Scopus

Fingerprint Dive into the research topics of 'CCMC: A conditional CSL model checker for continuous-time Markov chains'. Together they form a unique fingerprint.

Cite this

Gao, Y., Hahn, E. M., Zhan, N., & Zhang, L. (2013). CCMC: A conditional CSL model checker for continuous-time Markov chains. In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Proceedings (pp. 464-468). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8172 LNAI). https://doi.org/10.1007/978-3-319-02444-8_36

Gao, Yang ; Hahn, Ernst Moritz ; Zhan, Naijun ; Zhang, Lijun. / CCMC : A conditional CSL model checker for continuous-time Markov chains. Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Proceedings. 2013. pp. 464-468 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{7049d06fdd614ae1a58b606962aa93bc,

title = "CCMC: A conditional CSL model checker for continuous-time Markov chains",

abstract = "We present CCMC (Conditional CSL Model Checker), a model checker for continuous-time Markov chains (CTMCs) with respect to properties specified in continuous-time stochastic logic (CSL). Existing CTMC model checkers such as PRISM or MRMC handle only binary CSL until path formulas. CCMC is the first tool that supports algorithms for analyzing multiple until path formulas. Moreover, CCMC supports a recent extension of CSL - conditional CSL - which makes it possible to verify a larger class of properties on CTMC models. Our tool is based on our recent algorithmic advances for CSL, that construct a stratified CTMC before performing transient probability analyses. The stratified CTMC is a product obtained from the original CTMC and an automaton extracted from a given formula, aiming to filter out the irrelevant paths and make the computation more efficient.",

author = "Yang Gao and Hahn, {Ernst Moritz} and Naijun Zhan and Lijun Zhang",

year = "2013",

doi = "10.1007/978-3-319-02444-8_36",

language = "English",

isbn = "9783319024431",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "464--468",

booktitle = "Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Proceedings",

note = "11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013 ; Conference date: 15-10-2013 Through 18-10-2013",

}

Gao, Y, Hahn, EM, Zhan, N & Zhang, L 2013, CCMC: A conditional CSL model checker for continuous-time Markov chains. in Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8172 LNAI, pp. 464-468, 11th International Symposium on Automated Technology for Verification and Analysis, Hanoi, Viet Nam, 15/10/13. https://doi.org/10.1007/978-3-319-02444-8_36

CCMC : A conditional CSL model checker for continuous-time Markov chains. / Gao, Yang; Hahn, Ernst Moritz; Zhan, Naijun; Zhang, Lijun.

Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Proceedings. 2013. p. 464-468 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8172 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - CCMC

T2 - 11th International Symposium on Automated Technology for Verification and Analysis

AU - Gao, Yang

AU - Hahn, Ernst Moritz

AU - Zhan, Naijun

AU - Zhang, Lijun

N1 - Conference code: 11

PY - 2013

Y1 - 2013

N2 - We present CCMC (Conditional CSL Model Checker), a model checker for continuous-time Markov chains (CTMCs) with respect to properties specified in continuous-time stochastic logic (CSL). Existing CTMC model checkers such as PRISM or MRMC handle only binary CSL until path formulas. CCMC is the first tool that supports algorithms for analyzing multiple until path formulas. Moreover, CCMC supports a recent extension of CSL - conditional CSL - which makes it possible to verify a larger class of properties on CTMC models. Our tool is based on our recent algorithmic advances for CSL, that construct a stratified CTMC before performing transient probability analyses. The stratified CTMC is a product obtained from the original CTMC and an automaton extracted from a given formula, aiming to filter out the irrelevant paths and make the computation more efficient.

AB - We present CCMC (Conditional CSL Model Checker), a model checker for continuous-time Markov chains (CTMCs) with respect to properties specified in continuous-time stochastic logic (CSL). Existing CTMC model checkers such as PRISM or MRMC handle only binary CSL until path formulas. CCMC is the first tool that supports algorithms for analyzing multiple until path formulas. Moreover, CCMC supports a recent extension of CSL - conditional CSL - which makes it possible to verify a larger class of properties on CTMC models. Our tool is based on our recent algorithmic advances for CSL, that construct a stratified CTMC before performing transient probability analyses. The stratified CTMC is a product obtained from the original CTMC and an automaton extracted from a given formula, aiming to filter out the irrelevant paths and make the computation more efficient.

UR - http://www.scopus.com/inward/record.url?scp=84887498001&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-02444-8_36

DO - 10.1007/978-3-319-02444-8_36

M3 - Conference contribution

AN - SCOPUS:84887498001

SN - 9783319024431

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 464

EP - 468

BT - Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Proceedings

Y2 - 15 October 2013 through 18 October 2013

ER -

Gao Y, Hahn EM, Zhan N, Zhang L. CCMC: A conditional CSL model checker for continuous-time Markov chains. In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Proceedings. 2013. p. 464-468. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-02444-8_36