{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T04:32:40Z","timestamp":1768278760684,"version":"3.49.0"},"publisher-location":"Cham","reference-count":11,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319064093","type":"print"},{"value":"9783319064109","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06410-9_22","type":"book-chapter","created":{"date-parts":[[2014,4,18]],"date-time":"2014-04-18T21:03:01Z","timestamp":1397854981000},"page":"312-317","source":"Crossref","is-referenced-by-count":65,"title":["iscasMc: A Web-Based Probabilistic Model Checker"],"prefix":"10.1007","author":[{"given":"Ernst Moritz","family":"Hahn","sequence":"first","affiliation":[]},{"given":"Yi","family":"Li","sequence":"additional","affiliation":[]},{"given":"Sven","family":"Schewe","sequence":"additional","affiliation":[]},{"given":"Andrea","family":"Turrini","sequence":"additional","affiliation":[]},{"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A. Bianco","year":"1995","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabalistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol.\u00a01026, pp. 499\u2013513. Springer, Heidelberg (1995)"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Ciesinski, F., Baier, C.: LiQuor: A tool for qualitative and quantitative linear time analysis of reactive systems. In: QEST, pp. 131\u2013132 (2006)","DOI":"10.1109\/QEST.2006.25"},{"issue":"4","key":"22_CR4","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. JACM\u00a042(4), 857\u2013907 (1995)","journal-title":"JACM"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A.: LTL translation improvements in SPOT. In: VECoS, pp. 72\u201383. BCS (2011)","DOI":"10.14236\/ewic\/VECOS2011.8"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: FMSP, pp. 7\u201315 (1998)","DOI":"10.1145\/298595.298598"},{"key":"22_CR7","unstructured":"Hahn, E.M., Li, G., Schewe, S., Zhang, L.: Lazy determinisation for quantitative model checking, arXiv:1311.2928 (2013)"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Katoen, J.P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: QEST, pp. 243\u2013244 (2005)","DOI":"10.1109\/QEST.2005.2"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-540-73368-3_37","volume-title":"Computer Aided Verification","author":"J.-P. Katoen","year":"2007","unstructured":"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.\u00a04590, pp. 311\u2013324. Springer, Heidelberg (2007)"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"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.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-642-33386-6_5","volume-title":"Automated Technology for Verification and Analysis","author":"S. Schewe","year":"2012","unstructured":"Schewe, S., Varghese, T.: Tight bounds for the determinisation and complementation of generalised B\u00fcchi automata. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol.\u00a07561, pp. 42\u201356. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","FM 2014: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06410-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T12:33:57Z","timestamp":1746189237000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06410-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319064093","9783319064109"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06410-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}