{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T05:16:43Z","timestamp":1672291003926},"reference-count":27,"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":"Markov decision processes (MDP) can serve as operational model for probabilistic distributed systems and yield the basis for model checking algorithms against qualitative or quantitative properties. In this paper, we summarize the main steps of a quantitative analysis for a given MDP and formula of linear temporal logic, give an introduction to the modelling language ProbMela which provides a simple and intuitive way to describe complex systems with a MDP-semantics and present the basic features of the MDP model checker LiQuor.<\/jats:p>","DOI":"10.1145\/1059816.1059821","type":"journal-article","created":{"date-parts":[[2007,1,17]],"date-time":"2007-01-17T18:32:02Z","timestamp":1169058722000},"page":"22-27","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["ProbMela and verification of Markov decision processes"],"prefix":"10.1145","volume":"32","author":[{"given":"Christel","family":"Baier","sequence":"first","affiliation":[]},{"given":"Frank","family":"Ciesinski","sequence":"additional","affiliation":[]},{"given":"Marcus","family":"Gr\u00f6\u00dfer","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Bonn, R\u00f6merstr, Bonn, Germany"}]}],"member":"320","published-online":{"date-parts":[[2005,3]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"57","volume-title":"Proc. of the Second ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)","author":"Baier C.","year":"2004","unstructured":"C. Baier , F. Ciesinski , and M. Gr\u00f6\u00dfer . Probmela: a modeling language for communicating probabilistic systems . In Proc. of the Second ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE) , pages 57 -- 66 . IEEE CS Press , 2004 .]] C. Baier, F. Ciesinski, and M. Gr\u00f6\u00dfer. Probmela: a modeling language for communicating probabilistic systems. In Proc. of the Second ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pages 57--66. IEEE CS Press, 2004.]]"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1025129.1026092"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s004460050046"},{"key":"e_1_2_1_4_1","volume-title":"Lp solve. www.cs.sunysb.edu\/ algorith\/implement\/lpsolve\/implement.shtml","author":"Berkelaar M.","year":"1996","unstructured":"M. Berkelaar . Lp solve. www.cs.sunysb.edu\/ algorith\/implement\/lpsolve\/implement.shtml , 1996 .]] M. Berkelaar. Lp solve. www.cs.sunysb.edu\/ algorith\/implement\/lpsolve\/implement.shtml, 1996.]]"},{"key":"e_1_2_1_5_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Proc. Foundations of Software Technology and Theoretical Computer Science (FST & TCS)","author":"Bianco A.","year":"1995","unstructured":"A. Bianco and L. de Alfaro . Model checking of probabilistic and nondeterministic systems . In Proc. Foundations of Software Technology and Theoretical Computer Science (FST & TCS) , volume 1026 of Lecture Notes in Computer Science , pages 499 -- 513 , 1995 .]] A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In Proc. Foundations of Software Technology and Theoretical Computer Science (FST & TCS), volume 1026 of Lecture Notes in Computer Science, pages 499--513, 1995.]]"},{"key":"e_1_2_1_6_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_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/210332.210339"},{"key":"e_1_2_1_8_1","first-page":"87","article-title":"Modest - a modelling and description language for stochastic timed systems. Proc. PAPM\/PROBMIV'01","volume":"2165","author":"Argenio P.","year":"2001","unstructured":"P. d' Argenio , H. Hermanns , J. P. Katoen , and R. Klaren . Modest - a modelling and description language for stochastic timed systems. Proc. PAPM\/PROBMIV'01 , LNCS , 2165 : 87 -- 104 , 2001 .]] P. d'Argenio, H. Hermanns, J. P. Katoen, and R. Klaren. Modest - a modelling and description language for stochastic timed systems. Proc. PAPM\/PROBMIV'01, LNCS, 2165:87--104, 2001.]]","journal-title":"LNCS"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1025129.1026093"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/646733.701309"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/647770.734262"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/3-540-60761-7","volume-title":"On the costs and benefits of using partial-order methods for the verification of concurrent systems. In {25}","author":"Godefroid P.","year":"1996","unstructured":"P. Godefroid . On the costs and benefits of using partial-order methods for the verification of concurrent systems. In {25} , pages 289 -- 303 , 1996 .]] P. Godefroid. On the costs and benefits of using partial-order methods for the verification of concurrent systems. In {25}, pages 289--303, 1996.]]"},{"key":"e_1_2_1_14_1","series-title":"Series in Real-Time Safety Critical Systems","volume-title":"Time and Probability in Formal Design of Distributed Systems","author":"Hansson H.","year":"1994","unstructured":"H. Hansson . Time and Probability in Formal Design of Distributed Systems . Series in Real-Time Safety Critical Systems . Elsevier , 1994 .]] H. Hansson. Time and Probability in Formal Design of Distributed Systems. Series in Real-Time Safety Critical Systems. Elsevier, 1994.]]"},{"key":"e_1_2_1_15_1","volume-title":"The SPIN Model Checker, Primer and Reference Manual","author":"Holzmann G.","year":"2003","unstructured":"G. Holzmann . The SPIN Model Checker, Primer and Reference Manual . Addison Wesley , 2003 .]] G. Holzmann. The SPIN Model Checker, Primer and Reference Manual. Addison Wesley, 2003.]]"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90004-2"},{"key":"e_1_2_1_18_1","volume-title":"Universitaet Bonn","author":"Klein J.","year":"2005","unstructured":"J. Klein . Linear time logic and deterministic omega-automata. Master's thesis , Universitaet Bonn , 2005 .]] J. Klein. Linear time logic and deterministic omega-automata. Master's thesis, Universitaet Bonn, 2005.]]"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0140-2"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/567532.567547"},{"key":"e_1_2_1_22_1","first-page":"14","article-title":"pGCL: formal reasoning for random algorithms","volume":"22","author":"Morgan C.","year":"1999","unstructured":"C. Morgan and A. McIver . pGCL: formal reasoning for random algorithms . Spec. Iss.of SACJ , 22 : 14 -- 27 , 1999 .]] C. Morgan and A. McIver. pGCL: formal reasoning for random algorithms. Spec. Iss.of SACJ, 22:14--27, 1999.]]","journal-title":"Spec. Iss.of SACJ"},{"key":"e_1_2_1_23_1","volume-title":"The ANTLR Reference Manual. 2.6 ed","author":"Parr T.","year":"1999","unstructured":"T. Parr . The ANTLR Reference Manual. 2.6 ed ., 1999 .]] T. Parr. The ANTLR Reference Manual. 2.6 ed., 1999.]]"},{"key":"e_1_2_1_24_1","first-page":"79","volume-title":"Partial order reduction: Linear and branching time logics and process algebras. In {25}","author":"Peled D.","year":"1996","unstructured":"D. Peled . Partial order reduction: Linear and branching time logics and process algebras. In {25} , pages 79 -- 88 , 1996 .]] D. Peled. Partial order reduction: Linear and branching time logics and process algebras. In {25}, pages 79--88, 1996.]]"},{"key":"e_1_2_1_25_1","volume-title":"Partial Order Methods in Verification","author":"Peled D.","unstructured":"D. Peled , V. Pratt , and G. Holzmann , editors . Partial Order Methods in Verification , volume 29(10) of DIMACS Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, 1997 .]] D. Peled, V. Pratt, and G. Holzmann, editors. Partial Order Methods in Verification, volume 29(10) of DIMACS Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, 1997.]]"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","volume-title":"Markov Decision Processes---Discrete Stochastic Dynamic Programming","author":"Puterman M. L.","year":"1994","unstructured":"M. L. Puterman . Markov Decision Processes---Discrete Stochastic Dynamic Programming . John Wiley & Sons, Inc. , New York , 1994 .]] M. L. Puterman. Markov Decision Processes---Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc., New York, 1994.]]","DOI":"10.1002\/9780470316887"},{"key":"e_1_2_1_27_1","volume-title":"1st International Conference on Quantitative Evaluation of SysTems (QEST 2004","author":"Proceedings","year":"2004","unstructured":"Proceedings of the 1st International Conference on Quantitative Evaluation of SysTems (QEST 2004 ). Enschede, the Netherlands. IEEE Computer Society Press , 2004 .]] Proceedings of the 1st International Conference on Quantitative Evaluation of SysTems (QEST 2004). Enschede, the Netherlands. IEEE Computer Society Press, 2004.]]"},{"key":"e_1_2_1_28_1","first-page":"79","volume-title":"{25}","author":"Valmari A.","year":"1996","unstructured":"A. Valmari . Stubborn set methods for process algebras. In {25} , pages 79 -- 88 , 1996 .]] A. Valmari. Stubborn set methods for process algebras. In {25}, pages 79--88, 1996.]]"},{"key":"e_1_2_1_29_1","first-page":"332","volume-title":"Symposium on Logic in Computer Science (LICS'86)","author":"Vardi M. Y.","year":"1986","unstructured":"M. Y. Vardi and P. Wolper . An automata-theoretic approach to automatic program verification . In Symposium on Logic in Computer Science (LICS'86) , pages 332 -- 345 , Washington, D. C., USA , June 1986 . IEEE Computer Society Press.]] M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Symposium on Logic in Computer Science (LICS'86), pages 332--345, Washington, D. C., USA, June 1986. IEEE Computer Society Press.]]"}],"container-title":["ACM SIGMETRICS Performance Evaluation Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1059816.1059821","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T13:33:59Z","timestamp":1672234439000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1059816.1059821"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,3]]},"references-count":27,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2005,3]]}},"alternative-id":["10.1145\/1059816.1059821"],"URL":"http:\/\/dx.doi.org\/10.1145\/1059816.1059821","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"}}]}}