{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,20]],"date-time":"2025-04-20T16:23:15Z","timestamp":1745166195295,"version":"3.28.0"},"reference-count":33,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1109\/qest.2006.19","type":"proceedings-article","created":{"date-parts":[[2011,6,8]],"date-time":"2011-06-08T12:59:16Z","timestamp":1307537956000},"page":"157-166","source":"Crossref","is-referenced-by-count":23,"title":["Game-based Abstraction for Markov Decision Processes"],"prefix":"10.1109","member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.08.005"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"18","first-page":"441","article-title":"PRISM: A tool for automatic verification of probabilistic systems","volume":"3920","author":"hinton","year":"2006","journal-title":"LNCS"},{"key":"33","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47813-2_15"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00051-8"},{"key":"16","first-page":"71","article-title":"Don't know in probabilistic systems","volume":"3925","author":"fecher","year":"2006","journal-title":"LNCS"},{"key":"13","first-page":"66","article-title":"Computing minimum and maximum reachability times in probabilistic systems","volume":"1664","author":"de alfaro","year":"1999","journal-title":"LNCS"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1998.743507"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2004.1348038"},{"journal-title":"Formal Verification of Probabilistic Systems","year":"1997","author":"de alfaro","key":"12"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.08.008"},{"key":"20","first-page":"419","article-title":"An abstraction framework for mixed nondeterministic and probabilistic systems","volume":"2925","author":"huth","year":"2004","journal-title":"LNCS"},{"journal-title":"Denumerable Markov Chains","year":"1966","author":"kemeny","key":"22"},{"key":"23","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/s10009-004-0140-2","article-title":"Probabilistic symbolic model checking with PRISM: A hybrid approach","volume":"6","author":"kwiatkowska","year":"2004","journal-title":"International Journal on Software Tools for Technology Transfer"},{"article-title":"Game-based abstraction for Markov decision processes","year":"2006","author":"kwiatkowska","key":"24"},{"key":"25","first-page":"105","article-title":"Performance analysis of probabilistic timed automata using digital clocks","volume":"2791","author":"kwiatkowska","year":"2003","journal-title":"LNCS"},{"key":"26","article-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"mciver","year":"2004","journal-title":"Monographs in Computer Science"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.008"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24611-4_11"},{"year":"0","key":"29"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2004.1348037"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1287\/moor.16.3.580"},{"key":"10","first-page":"39","article-title":"Reachability analysis of probabilistic systems by successive refinements","volume":"2165","author":"d'argenio","year":"2001","journal-title":"LNCS"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1007\/s004460050046"},{"journal-title":"Modeling and Verification of Randomized Distributed Real-Time Systems","year":"1995","author":"segala","key":"30"},{"journal-title":"Model checking","year":"1999","author":"clarke","key":"7"},{"key":"6","first-page":"154","article-title":"Counterexample- guided abstraction refinement","volume":"1855","author":"clarke","year":"2000","journal-title":"LNCS"},{"key":"32","first-page":"275","article-title":"A game-based framework for CTL counter-examples and 3-valued abstraction-refinement","volume":"2725","author":"shoham","year":"2003","journal-title":"LNCS"},{"year":"0","key":"5"},{"key":"31","first-page":"394","article-title":"Model-checking Markov chains in the presence of uncertainties","volume":"3920","author":"sen","year":"2006","journal-title":"LNCS"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2004.1348035"},{"key":"9","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1090\/dimacs\/013\/04","article-title":"On algorithms for simple stochastic games. Advances in computational complexity theory","volume":"13","author":"condon","year":"1993","journal-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90048-K"}],"event":{"name":"Third International Conference on the Quantitative Evaluation of Systems - (QEST'06)","start":{"date-parts":[[2006,9,11]]},"location":"Riverside, CA, USA","end":{"date-parts":[[2006,9,14]]}},"container-title":["Third International Conference on the Quantitative Evaluation of Systems - (QEST'06)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/11169\/35961\/01704010.pdf?arnumber=1704010","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T14:25:40Z","timestamp":1560263140000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1704010\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"references-count":33,"URL":"https:\/\/doi.org\/10.1109\/qest.2006.19","relation":{},"subject":[],"published":{"date-parts":[[2006]]}}}