{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T02:27:40Z","timestamp":1773282460200,"version":"3.50.1"},"reference-count":44,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010,9]]},"DOI":"10.1109\/allerton.2010.5707120","type":"proceedings-article","created":{"date-parts":[[2011,2,3]],"date-time":"2011-02-03T21:50:52Z","timestamp":1296769852000},"page":"1691-1698","source":"Crossref","is-referenced-by-count":41,"title":["Advances and challenges of probabilistic model checking"],"prefix":"10.1109","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","article-title":"Approximate probabilistic model checking","volume":"2937","author":"herault","year":"2004","journal-title":"Proc VMCAI'04"},{"key":"ref38","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-24611-4_9","article-title":"Symbolic representations and analysis of large probabilistic systems","volume":"2925","author":"miner","year":"2004","journal-title":"Validation of Stochastic Systems A Guide to Current Research"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2010.24"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(4:8)2008"},{"key":"ref31","article-title":"Modelling and verification of randomized distributed real time systems","author":"segala","year":"1995"},{"key":"ref30","article-title":"Assume guarantee verification for probabilistic systems","volume":"6105","author":"kwiatkowska","year":"2010","journal-title":"Proc TACAS'10"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2004.1348037"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2004.1348038"},{"key":"ref35","article-title":"Symmetry reduction for probabilistic model checking","volume":"4114","author":"kwiatkowska","year":"2006","journal-title":"Proc CAV'06"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_9"},{"key":"ref10","article-title":"PRISM web site","year":"0"},{"key":"ref40","article-title":"Probabilistic verification of discrete event systems using acceptance sampling","volume":"2404","author":"younes","year":"2002","journal-title":"Proc CAV'02"},{"key":"ref11","article-title":"Model checking probabilistic real time systems","author":"jensen","year":"1996","journal-title":"Proc 7th Nordic Workshop on Programming Theory"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00215-8"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00046-9"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-006-0005-2"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2009.41"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.01.004"},{"key":"ref18","article-title":"Stochastic games for verification of probabilistic timed automata","volume":"5813","author":"kwiatkowska","year":"2009","journal-title":"Proc FORMATS'09"},{"key":"ref19","year":"0"},{"key":"ref28","article-title":"Abstraction refinement for probabilistic software","volume":"5403","author":"kattenbelt","year":"2009","journal-title":"Proc VMCAI'09"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-010-0097-6"},{"key":"ref3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-9455-6","author":"kemeny","year":"1976","journal-title":"Denumerable Markov Chains"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_26"},{"key":"ref5","article-title":"Cost-optimisation of the IPv4 Zeroconf protocol","author":"bohnenkamp","year":"2003","journal-title":"Proc IPDS'03"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"ref7","doi-asserted-by":"crossref","DOI":"10.1002\/9780470316887","author":"puterman","year":"1994","journal-title":"Markov Decision Processes Discrete Stochastic Dynamic Programming"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2009.11"},{"key":"ref9","first-page":"269","article-title":"Verifying continuous time Markov chains","volume":"1102","author":"aziz","year":"1996","journal-title":"Proc CAV'96"},{"key":"ref1","article-title":"PRISM: A tool for automatic verification of probabilistic systems","volume":"3920","author":"hinton","year":"2006","journal-title":"Proc TACAS'06"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2010.41"},{"key":"ref22","article-title":"Don't know in probabilistic systems","volume":"3925","author":"fecher","year":"2006","journal-title":"Proc SPIN'06"},{"key":"ref21","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45804-2","author":"hermanns","year":"2002","journal-title":"Interactive Markov Chains and the Quest for Quantified Quality"},{"key":"ref42","article-title":"A framework for verification of software with time and probabilities","author":"kwiatkowska","year":"2010","journal-title":"Proc FORMATS'10"},{"key":"ref24","article-title":"Reachability analysis of probabilistic systems by successive refinements","volume":"2165","author":"d'argenio","year":"2001","journal-title":"Proc PAPMIPROBMIV'01"},{"key":"ref41","first-page":"241","article-title":"Counterexample generation in probabilistic model checking","volume":"35","author":"han","year":"0","journal-title":"IEEE TSE"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_37"},{"key":"ref44","article-title":"Probabilistic reachability for parametric Markov models","volume":"5578","author":"hahn","year":"2009","journal-title":"Proc SPIN'09"},{"key":"ref26","article-title":"Probabilistic CEGAR","volume":"5123","author":"hermanns","year":"2008","journal-title":"Proc CAV'08"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2008.19"},{"key":"ref25","article-title":"Game-based abstraction for Markov decision processes","author":"kwiatkowska","year":"2006","journal-title":"Proc QEST'06"}],"event":{"name":"2010 48th Annual Allerton Conference on Communication, Control, and Computing (Allerton)","location":"Monticello, IL, USA","start":{"date-parts":[[2010,9,29]]},"end":{"date-parts":[[2010,10,1]]}},"container-title":["2010 48th Annual Allerton Conference on Communication, Control, and Computing (Allerton)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5701578\/5706874\/05707120.pdf?arnumber=5707120","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,18]],"date-time":"2021-11-18T13:57:41Z","timestamp":1637243861000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5707120\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,9]]},"references-count":44,"URL":"https:\/\/doi.org\/10.1109\/allerton.2010.5707120","relation":{},"subject":[],"published":{"date-parts":[[2010,9]]}}}