{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T23:41:02Z","timestamp":1778715662213,"version":"3.51.4"},"reference-count":89,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2013,7,8]],"date-time":"2013-07-08T00:00:00Z","timestamp":1373241600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2013,8]]},"abstract":"<jats:p>This paper gives a bird's-eye view of the various ingredients that make up a modern, model-checking-based approach to performability evaluation: Markov reward models, temporal logics and continuous stochastic logic, model-checking algorithms, bisimulation and the handling of non-determinism. A short historical account as well as a large case study complete this picture. In this way, we show convincingly that the smart combination of performability evaluation with stochastic model-checking techniques, developed over the last decade, provides a powerful and unified method of performability evaluation, thereby combining the advantages of earlier approaches.<\/jats:p>","DOI":"10.1017\/s0960129512000254","type":"journal-article","created":{"date-parts":[[2013,7,8]],"date-time":"2013-07-08T11:28:01Z","timestamp":1373282881000},"page":"751-795","source":"Crossref","is-referenced-by-count":20,"title":["Model checking for performability"],"prefix":"10.1017","volume":"23","author":[{"given":"C.","family":"BAIER","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"E. M.","family":"HAHN","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"B. R.","family":"HAVERKORT","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H.","family":"HERMANNS","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.-P.","family":"KATOEN","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2013,7,8]]},"reference":[{"key":"S0960129512000254_ref64","first-page":"334","volume-title":"Proceedings of the 1st International Performance and Dependability Symposium","author":"Meyer","year":"1995"},{"key":"S0960129512000254_ref61","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1980.1675654"},{"key":"S0960129512000254_ref53","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2010.04.001"},{"key":"S0960129512000254_ref49","volume-title":"Dynamic Probabilistic Systems; Volume II: Semi-Markov and decision processes","author":"Howard","year":"1971"},{"key":"S0960129512000254_ref35","doi-asserted-by":"publisher","DOI":"10.1109\/2.56852"},{"key":"S0960129512000254_ref43","doi-asserted-by":"publisher","DOI":"10.1016\/0166-5316(94)00038-7"},{"key":"S0960129512000254_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.05.006"},{"key":"S0960129512000254_ref29","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2007.26"},{"key":"S0960129512000254_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/7531.7536"},{"key":"S0960129512000254_ref24","first-page":"136","volume-title":"Proceedings of the 1st International Workshop on Timed Petri Nets","author":"Chiola","year":"1985"},{"key":"S0960129512000254_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44804-7_9"},{"key":"S0960129512000254_ref54","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9_17"},{"key":"S0960129512000254_ref18","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1978.1675145"},{"key":"S0960129512000254_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.03.001"},{"key":"S0960129512000254_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_14"},{"key":"S0960129512000254_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/1810891.1810912"},{"key":"S0960129512000254_ref11","first-page":"53","volume-title":"Logic and Automata","author":"Baier","year":"2008"},{"key":"S0960129512000254_ref48","volume-title":"Dynamic Probabilistic Systems; Volume I: Markov models","author":"Howard","year":"1971"},{"key":"S0960129512000254_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45022-X_65"},{"key":"S0960129512000254_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_19"},{"key":"S0960129512000254_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343402"},{"key":"S0960129512000254_ref1","first-page":"83","volume-title":"Hybrid Systems: Computation and Control (HSCC)","author":"Abate","year":"2011"},{"key":"S0960129512000254_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2008.03.027"},{"key":"S0960129512000254_ref57","doi-asserted-by":"publisher","DOI":"10.1145\/1530873.1530882"},{"key":"S0960129512000254_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.07.022"},{"key":"S0960129512000254_ref38","doi-asserted-by":"publisher","DOI":"10.1109\/12.75148"},{"key":"S0960129512000254_ref51","first-page":"266","volume-title":"6th IEEE Symposium on Logic in Computer Science (LICS)","author":"Jonsson","year":"1991"},{"key":"S0960129512000254_ref62","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1982.1676062"},{"key":"S0960129512000254_ref34","first-page":"51","volume-title":"Proceedings of the 9th Fault-Tolerant Computer Systems Systems (FTCS)","author":"Gay","year":"1979"},{"key":"S0960129512000254_ref80","volume-title":"Quantitative Evaluation of Systems (QEST)","author":"Sanders","year":"2010"},{"key":"S0960129512000254_ref59","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.09.021"},{"key":"S0960129512000254_ref63","doi-asserted-by":"publisher","DOI":"10.1016\/0166-5316(92)90002-X"},{"key":"S0960129512000254_ref33","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1984.1676479"},{"key":"S0960129512000254_ref28","first-page":"145","volume-title":"Quantitative Evaluation of Systems (QEST)","author":"Cloth","year":"2005"},{"key":"S0960129512000254_ref30","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(02)00068-1"},{"key":"S0960129512000254_ref40","doi-asserted-by":"publisher","DOI":"10.1109\/24.3744"},{"key":"#cr-split#-S0960129512000254_ref42.1","unstructured":"Haverkort B. R. (2006) Can we quantitatively assess security? In: Workshop on Emperical Evaluation of Dependability and Security"},{"key":"#cr-split#-S0960129512000254_ref42.2","unstructured":"Supplement Proceedings DSN 2006 (online) 125-128."},{"key":"S0960129512000254_ref45","article-title":"Interactive Markov Chains: The Quest for Quantitative Quality.","volume":"2428","author":"Hermanns","year":"2002","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129512000254_ref52","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_37"},{"key":"S0960129512000254_ref66","doi-asserted-by":"publisher","DOI":"10.1137\/0306020"},{"key":"S0960129512000254_ref65","volume-title":"Performability Modelling","author":"Meyer","year":"2001"},{"key":"S0960129512000254_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"S0960129512000254_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/190.191"},{"key":"S0960129512000254_ref81","first-page":"250","article-title":"Probabilistic simulations for probabilistic processes.","volume":"2","author":"Segala","year":"1995","journal-title":"Nordic Journal of Computing"},{"key":"S0960129512000254_ref47","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(02)00066-8"},{"key":"S0960129512000254_ref41","doi-asserted-by":"publisher","DOI":"10.1287\/opre.32.2.343"},{"key":"S0960129512000254_ref32","doi-asserted-by":"publisher","DOI":"10.1109\/TR.1987.5222291"},{"key":"S0960129512000254_ref46","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17071-3_16"},{"key":"S0960129512000254_ref56","volume-title":"Queueing Systems; Volume 2: Computer Applications","author":"Kleinrock","year":"1976"},{"key":"S0960129512000254_ref55","volume-title":"Queueing Systems; Volume 1: Theory","author":"Kleinrock","year":"1975"},{"key":"S0960129512000254_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48320-9_12"},{"key":"S0960129512000254_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0088-7"},{"key":"S0960129512000254_ref23","first-page":"123","volume-title":"Quantitative Evaluation of Systems (QEST)","author":"Caillaud","year":"2010"},{"key":"S0960129512000254_ref10","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"S0960129512000254_ref60","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1976.1674657"},{"key":"S0960129512000254_ref67","first-page":"481","volume-title":"Proceedings of the 2nd International Joint Conference on Artificial Intelligence","author":"Milner","year":"1971"},{"key":"S0960129512000254_ref86","doi-asserted-by":"publisher","DOI":"10.1016\/0166-5316(92)90001-W"},{"key":"S0960129512000254_ref68","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3"},{"key":"S0960129512000254_ref70","first-page":"215","volume-title":"IEEE Real-Time Systems Symposium","author":"Movaghar","year":"1984"},{"key":"S0960129512000254_ref71","first-page":"209","volume-title":"Quantitative Evaluation of Systems (QEST)","author":"Neuh\u00e4u\u00dfer","year":"2010"},{"key":"S0960129512000254_ref73","doi-asserted-by":"publisher","DOI":"10.1016\/0166-5316(94)90061-2"},{"key":"S0960129512000254_ref74","doi-asserted-by":"publisher","DOI":"10.1016\/0166-5316(94)90061-2"},{"key":"S0960129512000254_ref75","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-011-0140-0"},{"key":"S0960129512000254_ref76","doi-asserted-by":"publisher","DOI":"10.1016\/0305-0548(88)90026-3"},{"key":"S0960129512000254_ref77","doi-asserted-by":"publisher","DOI":"10.1080\/15326348908807130"},{"key":"S0960129512000254_ref82","doi-asserted-by":"publisher","DOI":"10.1080\/15326340008807601"},{"key":"S0960129512000254_ref83","doi-asserted-by":"publisher","DOI":"10.1109\/12.2184"},{"key":"S0960129512000254_ref84","doi-asserted-by":"publisher","DOI":"10.1016\/0166-5316(92)90003-Y"},{"key":"S0960129512000254_ref85","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6377(00)00023-7"},{"key":"S0960129512000254_ref87","volume-title":"Quantitative Evaluation of Systems (QEST)","author":"Wachter","year":"2007"},{"key":"S0960129512000254_ref88","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_5"},{"key":"S0960129512000254_ref50","first-page":"87","article-title":"Markov chains as an aid in the study of Markov processes.","volume":"36","author":"Jensen","year":"1953","journal-title":"Skandinavisk Aktuarietidsskrift"},{"key":"S0960129512000254_ref69","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1982.1676110"},{"key":"S0960129512000254_ref72","doi-asserted-by":"publisher","DOI":"10.1109\/12.210174"},{"key":"S0960129512000254_ref39","first-page":"7","article-title":"Evaluation of performability for degradable computer systems.","volume":"36","author":"Goyal","year":"1987","journal-title":"IEEE Transactions on Computers"},{"key":"S0960129512000254_ref19","first-page":"311","volume-title":"Quantitative Evaluation of Systems (QEST)","author":"Berendsen","year":"2006"},{"key":"S0960129512000254_ref21","first-page":"61","article-title":"Continuous-time stochastic games with time-bounded reachability. In: FSTTCS","volume":"4","author":"Br\u00e1zdil","year":"2009","journal-title":"LIPIcs"},{"key":"S0960129512000254_ref5","doi-asserted-by":"publisher","DOI":"10.1109\/T-C.1973.223703"},{"key":"S0960129512000254_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/1328690.1328697"},{"key":"S0960129512000254_ref58","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"S0960129512000254_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/BF02187098"},{"key":"S0960129512000254_ref44","volume-title":"Performability Modelling: Techniques and Tools","author":"Haverkort","year":"2001"},{"key":"S0960129512000254_ref15","volume-title":"Principles of Model Checking","author":"Baier","year":"2008"},{"key":"S0960129512000254_ref78","first-page":"111","volume-title":"Proceedings of the 2nd International Workshop on Petri Nets and Performance Models","author":"Sanders","year":"1987"},{"key":"S0960129512000254_ref36","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1145\/945445.945450","volume-title":"ACM Symposium on Operating Systems Principles (SOSP)","author":"Ghemawat","year":"2003"},{"key":"S0960129512000254_ref6","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2004.2"},{"key":"S0960129512000254_ref79","doi-asserted-by":"publisher","DOI":"10.1109\/49.64901"},{"key":"S0960129512000254_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45232-4_6"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129512000254","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T20:43:07Z","timestamp":1556052187000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129512000254\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7,8]]},"references-count":89,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,8]]}},"alternative-id":["S0960129512000254"],"URL":"https:\/\/doi.org\/10.1017\/s0960129512000254","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,7,8]]}}}