<XML><RECORDS><RECORD><REFERENCE_TYPE>0</REFERENCE_TYPE><REFNUM>8674</REFNUM><AUTHORS><AUTHOR>Graham,D.</AUTHOR><AUTHOR>Calder,M.</AUTHOR><AUTHOR>Miller,A.</AUTHOR></AUTHORS><YEAR>2009</YEAR><TITLE>An inductive technique for parameterised model checking of degenerative distributed randomised protocols</TITLE><PLACE_PUBLISHED>ENTCS, volume 250(1)</PLACE_PUBLISHED><PUBLISHER>Electronic Notes in Theoretical Computer Science</PUBLISHER><PAGES>87-103</PAGES><ISBN>10.1016/j.entcs.2009.08.007</ISBN><LABEL>Graham:2009:8674</LABEL><KEYWORDS><KEYWORD>parameterised probabilistic model checking</KEYWORD></KEYWORDS<ABSTRACT>We present a technique to tackle the parameterised probabilistic model checking problem for a particular class of randomised distributed systems, which we model as Markov Decision Processes. These systems, termed \emph{degenerative}, have the property that a model of a system with some communication graph will eventually behave like a model of a system with a \emph{reduced} graph. We describe an induction schema for reasoning about models of a degenerative system over arbitrary graphs. We thereby show that a certain class of quantitative LTL properties will hold for a model of a system with any communication graph if it holds for all models of a system with some base graph. We demonstrate our technique via a case study (a randomised leader election protocol) specified using the PRISM modelling language.</ABSTRACT></RECORD></RECORDS></XML>