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.
Supported by the National Natural Science Foundation of China (NSFC) under grant No. 61361136002, 61350110518, 61202069, the Chinese Academy of Sciences Fellowship for International Young Scientists (Grant No. 2013Y1GB0006), Research Fund for the Doctoral Program of Higher Education of China (Grant No. 20120001120103), and Engineering and Physical Science Research Council (EPSRC) through the grant EP/H046623/1.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)
Bianco, A., de Alfaro, L.: Model checking of probabalistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)
Ciesinski, F., Baier, C.: LiQuor: A tool for qualitative and quantitative linear time analysis of reactive systems. In: QEST, pp. 131–132 (2006)
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. JACM 42(4), 857–907 (1995)
Duret-Lutz, A.: LTL translation improvements in SPOT. In: VECoS, pp. 72–83. BCS (2011)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: FMSP, pp. 7–15 (1998)
Hahn, E.M., Li, G., Schewe, S., Zhang, L.: Lazy determinisation for quantitative model checking, arXiv:1311.2928 (2013)
Katoen, J.P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: QEST, pp. 243–244 (2005)
Katoen, J.-P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for continuous-time Markov chains. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 311–324. Springer, Heidelberg (2007)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)
Schewe, S., Varghese, T.: Tight bounds for the determinisation and complementation of generalised Büchi automata. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 42–56. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L. (2014). iscasMc: A Web-Based Probabilistic Model Checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds) FM 2014: Formal Methods. FM 2014. Lecture Notes in Computer Science, vol 8442. Springer, Cham. https://doi.org/10.1007/978-3-319-06410-9_22
Download citation
DOI: https://doi.org/10.1007/978-3-319-06410-9_22
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06409-3
Online ISBN: 978-3-319-06410-9
eBook Packages: Computer ScienceComputer Science (R0)