IscasMc: A web-based probabilistic model checker

Ernst Moritz Hahn; Yi Li; Sven Schewe; Andrea Turrini; Lijun Zhang

doi:10.1007/978-3-319-06410-9_22

IscasMc: A web-based probabilistic model checker

Ernst Moritz Hahn, Yi Li, Sven Schewe, Andrea Turrini, Lijun Zhang^*

^*Corresponding author for this work

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

57 Citations (Scopus)

Abstract

We introduce the web-based model checker iscasMc for probabilistic systems (see http://iscasmc.ios.ac.cn/IscasMC). This Java application offers an easy-to-use web interface for the evaluation of Markov chains and decision processes against PCTL and PCTL specifications. Compared to PRISM or MRMC, iscasMc is particularly efficient in evaluating the probabilities of LTL properties.

Original language	English
Title of host publication	FM 2014: Formal Methods
Subtitle of host publication	19th International Symposium, Singapore, May 12-16, 2014. Proceedings
Editors	Cliff Jones, Pekka Pihlajasaari, Jun Sun
Place of Publication	Cham
Publisher	Springer
Pages	312-317
Number of pages	6
ISBN (Electronic)	978-3-319-06410-9
ISBN (Print)	978-3-319-06409-3
DOIs	https://doi.org/10.1007/978-3-319-06410-9_22
Publication status	Published - 2014
Externally published	Yes
Event	19th International Symposium on Formal Methods, FM 2014 - Singapore, Singapore Duration: 12 May 2014 → 16 May 2014 Conference number: 19

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	8442
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	19th International Symposium on Formal Methods, FM 2014
Abbreviated title	FM
Country/Territory	Singapore
City	Singapore
Period	12/05/14 → 16/05/14

Keywords

Model checker
Markov decision process (MDP)
Reachability problem
Work thread
Probabilistic model checker

Access to Document

10.1007/978-3-319-06410-9_22

Cite this

Hahn, E. M., Li, Y., Schewe, S., Turrini, A., & Zhang, L. (2014). IscasMc: A web-based probabilistic model checker. In C. Jones, P. Pihlajasaari, & J. Sun (Eds.), FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12-16, 2014. Proceedings (pp. 312-317). (Lecture Notes in Computer Science; Vol. 8442). Springer. https://doi.org/10.1007/978-3-319-06410-9_22

@inproceedings{5a809a07bb2a48a7a26d9d1db4938ac5,

title = "IscasMc: A web-based probabilistic model checker",

abstract = "We introduce the web-based model checker iscasMc for probabilistic systems (see http://iscasmc.ios.ac.cn/IscasMC). This Java application offers an easy-to-use web interface for the evaluation of Markov chains and decision processes against PCTL and PCTL specifications. Compared to PRISM or MRMC, iscasMc is particularly efficient in evaluating the probabilities of LTL properties.",

keywords = "Model checker, Markov decision process (MDP), Reachability problem, Work thread, Probabilistic model checker",

author = "Hahn, {Ernst Moritz} and Yi Li and Sven Schewe and Andrea Turrini and Lijun Zhang",

year = "2014",

doi = "10.1007/978-3-319-06410-9_22",

language = "English",

isbn = "978-3-319-06409-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "312--317",

editor = "Cliff Jones and Pekka Pihlajasaari and Jun Sun",

booktitle = "FM 2014: Formal Methods",

address = "Netherlands",

note = "19th International Symposium on Formal Methods, FM 2014, FM ; Conference date: 12-05-2014 Through 16-05-2014",

}

Hahn, EM, Li, Y, Schewe, S, Turrini, A & Zhang, L 2014, IscasMc: A web-based probabilistic model checker. in C Jones, P Pihlajasaari & J Sun (eds), FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12-16, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8442, Springer, Cham, pp. 312-317, 19th International Symposium on Formal Methods, FM 2014, Singapore, Singapore, 12/05/14. https://doi.org/10.1007/978-3-319-06410-9_22

IscasMc : A web-based probabilistic model checker. / Hahn, Ernst Moritz; Li, Yi; Schewe, Sven; Turrini, Andrea; Zhang, Lijun.

FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12-16, 2014. Proceedings. ed. / Cliff Jones; Pekka Pihlajasaari; Jun Sun. Cham : Springer, 2014. p. 312-317 (Lecture Notes in Computer Science; Vol. 8442).

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

TY - GEN

T1 - IscasMc

T2 - 19th International Symposium on Formal Methods, FM 2014

AU - Hahn, Ernst Moritz

AU - Li, Yi

AU - Schewe, Sven

AU - Turrini, Andrea

AU - Zhang, Lijun

N1 - Conference code: 19

PY - 2014

Y1 - 2014

N2 - We introduce the web-based model checker iscasMc for probabilistic systems (see http://iscasmc.ios.ac.cn/IscasMC). This Java application offers an easy-to-use web interface for the evaluation of Markov chains and decision processes against PCTL and PCTL specifications. Compared to PRISM or MRMC, iscasMc is particularly efficient in evaluating the probabilities of LTL properties.

AB - We introduce the web-based model checker iscasMc for probabilistic systems (see http://iscasmc.ios.ac.cn/IscasMC). This Java application offers an easy-to-use web interface for the evaluation of Markov chains and decision processes against PCTL and PCTL specifications. Compared to PRISM or MRMC, iscasMc is particularly efficient in evaluating the probabilities of LTL properties.

KW - Model checker

KW - Markov decision process (MDP)

KW - Reachability problem

KW - Work thread

KW - Probabilistic model checker

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

U2 - 10.1007/978-3-319-06410-9_22

DO - 10.1007/978-3-319-06410-9_22

M3 - Conference contribution

SN - 978-3-319-06409-3

T3 - Lecture Notes in Computer Science

SP - 312

EP - 317

BT - FM 2014: Formal Methods

A2 - Jones, Cliff

A2 - Pihlajasaari, Pekka

A2 - Sun, Jun

PB - Springer

CY - Cham

Y2 - 12 May 2014 through 16 May 2014

ER -

IscasMc: A web-based probabilistic model checker

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this