{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,7]],"date-time":"2023-01-07T06:26:33Z","timestamp":1673072793251},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"4","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGMETRICS Perform. Eval. Rev."],"published-print":{"date-parts":[[2005,3]]},"abstract":"\n Markov chains are one of the most popular models for the evaluation of performance and dependability of information processing systems. To obtain performance measures, typically long-run or transient state probabilities of Markov chains are determined. Sometimes the Markov chain at hand is equipped with rewards and computations involve determining long-run or instantaneous reward probabilities.This note summarises a technique to determine performance and dependability\n guarantees<\/jats:italic>\n of Markov chains. Given a precise description of the desired guarantee, all states in the Markov chain are determined that surely meet the guarantee. This is done in a fully automated way. Guarantees are described using logics. The use of logics yields an expressive framework that allows to express well-known measures, but also (new) intricate and complex performance guarantees. The power of this technique is that no matter how complex the logical guarantee, it is\n automatically<\/jats:italic>\n checked which states in the Markov chain satisfy it. Neither manual manipulations of Markov chains (or their high-level descriptions) are needed, nor the knowledge of any numerical technique to analyze them efficiently. This applies to any (time-homogeneous) Markov chain of any structure specified in any high-level formalism.\n <\/jats:p>","DOI":"10.1145\/1059816.1059819","type":"journal-article","created":{"date-parts":[[2007,1,17]],"date-time":"2007-01-17T18:32:02Z","timestamp":1169058722000},"page":"10-15","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Model checking meets performance evaluation"],"prefix":"10.1145","volume":"32","author":[{"given":"Christel","family":"Baier","sequence":"first","affiliation":[{"name":"University of Bonn, Germany"}]},{"given":"Boudewijn R.","family":"Haverkort","sequence":"additional","affiliation":[{"name":"Univ. of Twente, The Netherlands"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[{"name":"Saarland University, Germany"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}]}],"member":"320","published-online":{"date-parts":[[2005,3]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"88","article-title":"Discrete-time rewards model-checked. Formal Methods for Timed Systems","volume":"2791","author":"Andova S.","year":"2003","unstructured":"S. Andova , H. Hermanns and J.-P. Katoen . Discrete-time rewards model-checked. Formal Methods for Timed Systems , LNCS 2791 : 88 -- 104 , 2003 .]] S. Andova, H. Hermanns and J.-P. Katoen. Discrete-time rewards model-checked. Formal Methods for Timed Systems, LNCS 2791: 88--104, 2003.]]","journal-title":"LNCS"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343402"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1009382.1009786"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1999.1683"},{"key":"e_1_2_1_5_1","first-page":"780","article-title":"On the logical specification of performability properties. Automata, Languages and Programming","volume":"1853","author":"Baier C.","year":"2000","unstructured":"C. Baier , B. R. Haverkort , H. Hermanns , J.-P. Katoen . On the logical specification of performability properties. Automata, Languages and Programming , LNCS 1853 : 780 -- 792 , 2000 .]] C. Baier, B. R. Haverkort, H. Hermanns, J.-P. Katoen. On the logical specification of performability properties. Automata, Languages and Programming, LNCS 1853: 780--792, 2000.]]","journal-title":"LNCS"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"e_1_2_1_7_1","first-page":"61","article-title":"Efficient computation of maximal timed reachability probabilities in uniform continuous-time Markov decision processes. Tools and Algorithms for the Construction and Analysis of Systems","volume":"2988","author":"Baier C.","year":"2004","unstructured":"C. Baier , B. R. Haverkort , H. Hermanns , and J.-P. Katoen . Efficient computation of maximal timed reachability probabilities in uniform continuous-time Markov decision processes. Tools and Algorithms for the Construction and Analysis of Systems , LNCS 2988 : 61 -- 76 , 2004 .]] C. Baier, B. R. Haverkort, H. Hermanns, and J.-P. Katoen. Efficient computation of maximal timed reachability probabilities in uniform continuous-time Markov decision processes. Tools and Algorithms for the Construction and Analysis of Systems, LNCS 2988: 61--76, 2004.]]","journal-title":"LNCS"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2003.10.001"},{"key":"e_1_2_1_9_1","first-page":"492","article-title":"Comparative branching-time semantics for Markov chains. Concurrency Theory","volume":"2761","author":"Baier C.","year":"2003","unstructured":"C. Baier , H. Hermanns , J.-P. Katoen and V. Wolf . Comparative branching-time semantics for Markov chains. Concurrency Theory , LNCS 2761 , pp. 492 -- 508 , 2003 .]] C. Baier, H. Hermanns, J.-P. Katoen and V. Wolf. Comparative branching-time semantics for Markov chains. Concurrency Theory, LNCS 2761, pp. 492--508, 2003.]]","journal-title":"LNCS"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/646734.701464"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s004460050046"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(02)00067-X"},{"key":"e_1_2_1_13_1","unstructured":"G. Ciardo A. S. Miner. SMART. Stochastic model checking analyzer for reliability and timing. http:\/\/www.cs.ucr.edu\/~ciardo\/SMART\/]] G. Ciardo A. S. Miner. SMART. Stochastic model checking analyzer for reliability and timing. http:\/\/www.cs.ucr.edu\/~ciardo\/SMART\/]]"},{"key":"e_1_2_1_14_1","volume-title":"Model Checking","author":"Clarke E.","year":"1999","unstructured":"E. Clarke , O. Grumberg and D. Peled . Model Checking . MIT Press , 1999 .]] E. Clarke, O. Grumberg and D. Peled. Model Checking. MIT Press, 1999.]]"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2005.64"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30182-0_55"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(03)00343-0"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(02)00068-1"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/647883.738242"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100072"},{"key":"e_1_2_1_22_1","first-page":"57","article-title":"Beyond memoryless distributions: model checking semi-Markov chains. Process Algebra and Probabilistic Methods","volume":"2165","author":"Infante-L\u00f3pez G. G.","year":"2001","unstructured":"G. G. Infante-L\u00f3pez , H. Hermanns and J.-P. Katoen . Beyond memoryless distributions: model checking semi-Markov chains. Process Algebra and Probabilistic Methods , LNCS 2165 : 57 -- 70 , 2001 .]] G. G. Infante-L\u00f3pez, H. Hermanns and J.-P. Katoen. Beyond memoryless distributions: model checking semi-Markov chains. Process Algebra and Probabilistic Methods, LNCS 2165:57--70, 2001.]]","journal-title":"LNCS"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0140-2"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1059816.1059820"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"e_1_2_1_26_1","first-page":"202","article-title":"Statistical model checking of black-box probabilistic systems. Computer-Aided Verification","volume":"3114","author":"Sen K.","year":"2004","unstructured":"K. Sen , M. Viswanathan and G. Agha . Statistical model checking of black-box probabilistic systems. Computer-Aided Verification , LNCS 3114 : 202 -- 215 , 2004 .]] K. Sen, M. Viswanathan and G. Agha. Statistical model checking of black-box probabilistic systems. Computer-Aided Verification, LNCS 3114: 202--215, 2004.]]","journal-title":"LNCS"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_16"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/647771.760735"}],"container-title":["ACM SIGMETRICS Performance Evaluation Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1059816.1059819","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T13:34:08Z","timestamp":1672234448000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1059816.1059819"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,3]]},"references-count":28,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2005,3]]}},"alternative-id":["10.1145\/1059816.1059819"],"URL":"http:\/\/dx.doi.org\/10.1145\/1059816.1059819","relation":{},"ISSN":["0163-5999"],"issn-type":[{"value":"0163-5999","type":"print"}],"subject":["Computer Networks and Communications","Hardware and Architecture","Software"],"published":{"date-parts":[[2005,3]]},"assertion":[{"value":"2005-03-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}