{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T01:04:45Z","timestamp":1773104685334,"version":"3.50.1"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2010,8,3]],"date-time":"2010-08-03T00:00:00Z","timestamp":1280793600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2010,9]]},"DOI":"10.1007\/s10703-010-0097-6","type":"journal-article","created":{"date-parts":[[2010,8,2]],"date-time":"2010-08-02T16:09:37Z","timestamp":1280765377000},"page":"246-280","source":"Crossref","is-referenced-by-count":76,"title":["A game-based abstraction-refinement framework for\u00a0Markov decision processes"],"prefix":"10.1007","volume":"36","author":[{"given":"Mark","family":"Kattenbelt","sequence":"first","affiliation":[]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,8,3]]},"reference":[{"issue":"3","key":"97_CR1","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"C Baier","year":"1998","unstructured":"Baier C, Kwiatkowska M (1998) Model checking for a probabilistic branching time logic with fairness. Distrib Comput 11(3):125\u2013155","journal-title":"Distrib Comput"},{"issue":"3","key":"97_CR2","doi-asserted-by":"crossref","first-page":"580","DOI":"10.1287\/moor.16.3.580","volume":"16","author":"D Bertsekas","year":"1991","unstructured":"Bertsekas D, Tsitsiklis J (1991) An analysis of stochastic shortest path problems. Math Oper Res 16(3):580\u2013595","journal-title":"Math Oper Res"},{"key":"97_CR3","volume-title":"Probability and measure","author":"P Billingsley","year":"1979","unstructured":"Billingsley P (1979) Probability and measure. Wiley, New York"},{"key":"97_CR4","doi-asserted-by":"crossref","unstructured":"Chadha R, Viswanathan M (2010) A counterexample guided abstraction-refinement framework for Markov decision processes. ACM Trans Comput Logic (to appear)","DOI":"10.1145\/1838552.1838553"},{"key":"97_CR5","first-page":"206","volume-title":"Proc. 1st int. conf. quantitative evaluation of systems (QEST\u201904)","author":"K Chatterjee","year":"2004","unstructured":"Chatterjee K, de Alfaro L, Henzinger T (2004) Trading memory for randomness. In: Proc. 1st int. conf. quantitative evaluation of systems (QEST\u201904). IEEE Comput. Soc., Los Alamitos, pp\u00a0206\u2013217"},{"key":"97_CR6","unstructured":"Chatterjee K, Henzinger T, Jhala R, Majumdar R (2005) Counterexample-guided planning. In: Proc. 21st conference in uncertainty in artificial intelligence (UAI\u201905), pp\u00a0104\u2013111"},{"key":"97_CR7","unstructured":"Cheshire S, Adoba B, Guttman E (2002) Dynamic configuration of IPv4 link-local addresses (draft August 2002). Zeroconf Working Group of the Internet Engineering Task Force ( www.zeroconf.org )"},{"key":"97_CR8","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Proc. 12th int. conf. computer aided verification (CAV\u201900)","author":"E Clarke","year":"2000","unstructured":"Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Emerson A, Sistla A (eds) Proc. 12th int. conf. computer aided verification (CAV\u201900). Lecture notes in computer science, vol\u00a01855. Springer, Berlin, pp\u00a0154\u2013169"},{"issue":"2","key":"97_CR9","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0890-5401(92)90048-K","volume":"96","author":"A Condon","year":"1992","unstructured":"Condon A (1992) The complexity of stochastic games. Inf Comput 96(2):203\u2013224","journal-title":"Inf Comput"},{"key":"97_CR10","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1090\/dimacs\/013\/04","volume":"13","author":"A Condon","year":"1993","unstructured":"Condon A (1993) On algorithms for simple stochastic games. Advances in computational complexity theory. DIMACS Ser Discrete Math Theor Comput Sci 13:51\u201373","journal-title":"DIMACS Ser Discrete Math Theor Comput Sci"},{"key":"97_CR11","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/3-540-44804-7_3","volume-title":"Proc. 1st joint int workshop process algebra and probabilistic methods, performance modelling and verification (PAPM\/PROBMIV\u201901)","author":"P D\u2019Argenio","year":"2001","unstructured":"D\u2019Argenio P, Jeannet B, Jensen H, Larsen K (2001) Reachability analysis of probabilistic systems by successive refinements. In: de\u00a0Alfaro L, Gilmore S (eds) Proc. 1st joint int workshop process algebra and probabilistic methods, performance modelling and verification (PAPM\/PROBMIV\u201901). Lecture notes in computer science, vol\u00a02165. Springer, Berlin, pp\u00a039\u201356"},{"key":"97_CR12","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1007\/3-540-48320-9_7","volume-title":"Proc. 10th int. conf. concurrency theory (CONCUR\u201999)","author":"L Alfaro de","year":"1999","unstructured":"de Alfaro L (1999) Computing minimum and maximum reachability times in probabilistic systems. In: Baeten J, Mauw S (eds) Proc. 10th int. conf. concurrency theory (CONCUR\u201999). Lecture notes in computer science, vol\u00a01664. Springer, Berlin, pp\u00a066\u201381"},{"key":"97_CR13","unstructured":"de Alfaro L (1997) Formal verification of probabilistic systems. Ph.D. thesis, Stanford University"},{"key":"97_CR14","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/978-3-540-73368-3_38","volume-title":"Proc. 19th int. conf. computer aided verification (CAV\u201907)","author":"L Alfaro de","year":"2007","unstructured":"de Alfaro L, Roy P (2007) Magnifying-lens abstraction for Markov decision processes. In: Damm W, Hermanns H (eds) Proc. 19th int. conf. computer aided verification (CAV\u201907). Lecture notes in computer science, vol\u00a04590. Springer, Berlin, pp\u00a0325\u2013338"},{"key":"97_CR15","first-page":"564","volume-title":"Proc. 39th symp. foundations of computer science (FOCS\u201998)","author":"L Alfaro de","year":"1998","unstructured":"de Alfaro L, Henzinger T, Kupferman O (1998) Concurrent reachability games. In: Proc. 39th symp. foundations of computer science (FOCS\u201998). IEEE Comput. Soc., Los Alamitos, pp\u00a0564\u2013575"},{"issue":"3","key":"97_CR16","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1016\/j.tcs.2007.07.008","volume":"386","author":"L Alfaro de","year":"2007","unstructured":"de Alfaro L, Henzinger T, Kupferman O (2007) Concurrent reachability games. Theor Comput Sci 386(3):188\u2013217","journal-title":"Theor Comput Sci"},{"issue":"1","key":"97_CR17","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1016\/S0890-5401(03)00051-8","volume":"184","author":"J Desharnais","year":"2003","unstructured":"Desharnais J, Gupta V, Jagadeesan R, Panangaden P (2003) Approximating labelled Markov processes. Inf Comput 184(1):160\u2013200","journal-title":"Inf Comput"},{"key":"97_CR18","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/11691617_5","volume-title":"Proc. 13th int. spin workshop on model checking of software (SPIN\u201906)","author":"H Fecher","year":"2006","unstructured":"Fecher H, Leucker M, Wolf V (2006) Don\u2019t know in probabilistic systems. In: Valmari A (ed) Proc. 13th int. spin workshop on model checking of software (SPIN\u201906). Lecture notes in computer science, vol\u00a03925. Springer, Berlin, pp\u00a071\u201388"},{"key":"97_CR19","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Proc. 9th int. conf. computer aided verification (CAV\u201997)","author":"S Graf","year":"1997","unstructured":"Graf S, Saidi H (1997) Construction of abstract state graphs with PVS. In: Grumberg O (ed) Proc. 9th int. conf. computer aided verification (CAV\u201997). Lecture notes in computer science, vol\u00a01254. Springer, Berlin, pp\u00a072\u201383"},{"issue":"2","key":"97_CR20","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1109\/TSE.2009.5","volume":"35","author":"T Han","year":"2009","unstructured":"Han T, Katoen JP, Damman B (2009) Counterexample generation in probabilistic model checking. IEEE Trans Softw Eng 35(2):241\u2013257","journal-title":"IEEE Trans Softw Eng"},{"key":"97_CR21","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/978-3-540-70545-1_16","volume-title":"Proc. 20th int. conf. computer aided verification (CAV\u201908)","author":"H Hermanns","year":"2008","unstructured":"Hermanns H, Wachter B, Zhang L (2008) Probabilistic CEGAR. In: Gupta A, Malik S (eds) Proc. 20th int. conf. computer aided verification (CAV\u201908). Lecture notes in computer science, vol\u00a05123. Springer, Berlin, pp\u00a0162\u2013175"},{"key":"97_CR22","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Proc. 12th int. conf. tools and algorithms for the construction and analysis of systems (TACAS\u201906)","author":"A Hinton","year":"2006","unstructured":"Hinton A, Kwiatkowska M, Norman G, Parker D (2006) PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns H, Palsberg J (eds) Proc. 12th int. conf. tools and algorithms for the construction and analysis of systems (TACAS\u201906). Lecture notes in computer science, vol\u00a03920. Springer, Berlin, pp\u00a0441\u2013444"},{"issue":"1","key":"97_CR23","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1016\/j.tcs.2005.08.005","volume":"346","author":"J Hurd","year":"2005","unstructured":"Hurd J, McIver A, Morgan C (2005) Probabilistic guarded commands mechanized in HOL. Theor Comput Sci 346(1):96\u2013112","journal-title":"Theor Comput Sci"},{"key":"97_CR24","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/978-3-540-24611-4_12","volume-title":"Validation of stochastic systems","author":"M Huth","year":"2004","unstructured":"Huth M (2004) An abstraction framework for mixed nondeterministic and probabilistic systems. In: Baier C, Haverkort B, Hermanns H, Katoen JP, Siegle M (eds) Validation of stochastic systems. Lecture notes in computer science, vol\u00a02925. Springer, Berlin, pp\u00a0419\u2013444"},{"key":"97_CR25","doi-asserted-by":"crossref","unstructured":"Kattenbelt M, Kwiatkowska M, Norman G, Parker D (2008) Game-based probabilistic predicate abstraction in PRISM. In: Proc. 6th workshop quantitative aspects of programming languages (QAPL\u201908)","DOI":"10.1016\/j.entcs.2008.11.016"},{"key":"97_CR26","series-title":"Lecture notes in computer science","first-page":"182","volume-title":"Proc. 10th int. conf. verification, model checking and abstract interpretation (VMCAI\u201909)","author":"M Kattenbelt","year":"2009","unstructured":"Kattenbelt M, Kwiatkowska M, Norman G, Parker D (2009) Abstraction refinement for probabilistic software. In: Jones N, Muller-Olm M (eds) Proc. 10th int. conf. verification, model checking and abstract interpretation (VMCAI\u201909). Lecture notes in computer science, vol\u00a05403. Springer, Berlin, pp\u00a0182\u2013197"},{"key":"97_CR27","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov chains","author":"J Kemeny","year":"1976","unstructured":"Kemeny J, Snell J, Knapp A (1976) Denumerable Markov chains, 2nd edn. Springer, Berlin","edition":"2"},{"key":"97_CR28","first-page":"157","volume-title":"Proc. 3th int. conf. quantitative evaluation of systems (QEST\u201906)","author":"M Kwiatkowska","year":"2006","unstructured":"Kwiatkowska M, Norman G, Parker D (2006) Game-based abstraction for Markov decision processes. In: Proc. 3th int. conf. quantitative evaluation of systems (QEST\u201906). IEEE Comput. Soc., Los Alamitos, pp\u00a0157\u2013166"},{"key":"97_CR29","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/s10703-006-0005-2","volume":"29","author":"M Kwiatkowska","year":"2006","unstructured":"Kwiatkowska M, Norman G, Parker D, Sproston J (2006) Performance analysis of probabilistic timed automata using digital clocks. Form Methods Syst Des 29:33\u201378","journal-title":"Form Methods Syst Des"},{"key":"97_CR30","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/978-3-642-04368-0_17","volume-title":"Proc. 7th international conference on formal modelling and analysis of timed systems (FORMATS\u201909)","author":"M Kwiatkowska","year":"2009","unstructured":"Kwiatkowska M, Norman G, Parker D (2009) Stochastic games for verification of probabilistic timed automata. In: Ouaknine J, Vaandrager F (eds) Proc. 7th international conference on formal modelling and analysis of timed systems (FORMATS\u201909). Lecture notes in computer science, vol\u00a05813. Springer, Berlin, pp\u00a0212\u2013227"},{"key":"97_CR31","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K Larsen","year":"1991","unstructured":"Larsen K, Skou A (1991) Bisimulation through probabilistic testing. Inf Comput 94:1\u201328","journal-title":"Inf Comput"},{"key":"97_CR32","volume-title":"Abstraction, refinement and proof for probabilistic systems. Monographs in computer science","author":"A McIver","year":"2004","unstructured":"McIver A, Morgan C (2004) Abstraction, refinement and proof for probabilistic systems. Monographs in computer science. Springer, Berlin"},{"issue":"1\u20132","key":"97_CR33","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/j.scico.2005.02.008","volume":"58","author":"D Monniaux","year":"2005","unstructured":"Monniaux D (2005) Abstract interpretation of programs as Markov decision processes. Sci Comput Program 58(1\u20132):179\u2013205","journal-title":"Sci Comput Program"},{"key":"97_CR34","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"384","DOI":"10.1007\/978-3-540-24611-4_11","volume-title":"Validation of stochastic systems","author":"G Norman","year":"2004","unstructured":"Norman G (2004) Analysing randomized distributed algorithms. In: Baier C, Haverkort B, Hermanns H, Katoen JP, Siegle M (eds) Validation of stochastic systems. Lecture notes in computer science, vol\u00a02925. Springer, Berlin, pp\u00a0384\u2013418"},{"key":"97_CR35","unstructured":"PASS tool homepage. http:\/\/depend.cs.uni-sb.de\/PASS\/"},{"key":"97_CR36","series-title":"Lecture notes in computer science","first-page":"160","volume-title":"Program analysis and compilation, theory and practice, essays dedicated to Reinhard Wilhelm on the occasion of his 60th birthday","author":"AD Pierro","year":"2006","unstructured":"Pierro AD, Hankin C, Wiklicky H (2006) Abstract interpretation for worst and average case analysis. In: Reps T, Sagiv M, Bauer J (eds) Program analysis and compilation, theory and practice, essays dedicated to Reinhard Wilhelm on the occasion of his 60th birthday. Lecture notes in computer science, vol\u00a04444. Springer, Berlin, pp\u00a0160\u2013174"},{"key":"97_CR37","unstructured":"PRISM web site. http:\/\/www.prismmodelchecker.org\/"},{"key":"97_CR38","unstructured":"Segala R (1995) Modelling and verification of randomized distributed real time systems. Ph.D. thesis, Massachusetts Institute of Technology"},{"key":"97_CR39","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1007\/11691372_26","volume-title":"Proc. 12th int. conf. tools and algorithms for the construction and analysis of systems (TACAS\u201906)","author":"K Sen","year":"2006","unstructured":"Sen K, Viswanathan M, Agha G (2006) Model-checking Markov chains in the presence of uncertainties. In: Hermanns H, Palsberg J (eds) Proc. 12th int. conf. tools and algorithms for the construction and analysis of systems (TACAS\u201906). Lecture notes in computer science, vol\u00a03920. Springer, Berlin, pp\u00a0394\u2013410"},{"key":"97_CR40","doi-asserted-by":"crossref","unstructured":"Shapley L (1953) Stochastic games. In: Proc. national academy of science, vol\u00a039, pp\u00a01095\u20131100","DOI":"10.1073\/pnas.39.10.1953"},{"key":"97_CR41","series-title":"Electronic notes in theoretical computer science","first-page":"43","volume-title":"Proc. 6th workshop on quantitative aspects of programming languages (QAPL\u201908)","author":"M Smith","year":"2008","unstructured":"Smith M (2008) Probabilistic abstract interpretation of imperative programs using truncated normal distributions. In: Aldini A, Baier C (eds) Proc. 6th workshop on quantitative aspects of programming languages (QAPL\u201908). Electronic notes in theoretical computer science, vol\u00a0220(3). Elsevier, Dordrecht, pp\u00a043\u201359"},{"key":"97_CR42","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/3-540-48778-6_4","volume-title":"Proc. 5th int. AMAST workshop real-time and probabilistic systems (ARTS\u201999)","author":"M Stoelinga","year":"1999","unstructured":"Stoelinga M, Vaandrager F (1999) Root contention in IEEE 1394. In: Katoen JP (ed) Proc. 5th int. AMAST workshop real-time and probabilistic systems (ARTS\u201999). Lecture notes in computer science, vol\u00a01601. Springer, Berlin, pp\u00a053\u201374"},{"key":"97_CR43","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1007\/978-3-642-11319-2_26","volume-title":"Proc. 11th int. conf. verification, model checking and abstract interpretation (VMCAI\u201910)","author":"B Wachter","year":"2010","unstructured":"Wachter B, Zhang L (2010) Best probabilistic transformers. In: Barthe G, Hermenegildo M (eds) Proc. 11th int. conf. verification, model checking and abstract interpretation (VMCAI\u201910). Lecture notes in computer science, vol\u00a05944. Springer, Berlin, pp 362\u2013379"},{"key":"97_CR44","first-page":"129","volume-title":"Proc. 4th int. conf. quantitative evaluation of systems (QEST\u201907)","author":"B Wachter","year":"2006","unstructured":"Wachter B, Zhang L, Hermanns H (2006) Probabilistic model checking modulo theories. In: Proc. 4th int. conf. quantitative evaluation of systems (QEST\u201907). IEEE Comput. Soc., Los Alamitos, pp\u00a0129\u2013138"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-010-0097-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-010-0097-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-010-0097-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:05:51Z","timestamp":1559253951000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-010-0097-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,8,3]]},"references-count":44,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2010,9]]}},"alternative-id":["97"],"URL":"https:\/\/doi.org\/10.1007\/s10703-010-0097-6","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,8,3]]}}}