Undecidability Results for Distributed Probabilistic Systems

12 years 4 months ago
Undecidability Results for Distributed Probabilistic Systems
Abstract. In the verification of concurrent systems involving probabilities, the aim is to find out the maximum/minimum probability that a given event occurs (examples of such events being “the system reaches a failure state”,“a message is delivered”). Such extremal probabilities are obtained by quantifying over all the possible ways in which the processes may be interleaved. Interleaving choices are considered a particular case of nondeterministic behaviour. Such behaviour is dealt with by considering schedulers that resolve the nondeterministic choices. Each scheduler determines a Markov chain for which actual probabilities can be calculated. In the recent literature on distributed systems, particular attention has been paid to the fact that, in order to obtain accurate results, the analysis must rely on partial information schedulers, instead of full-history dependent schedulers used in the setting of Markov decision processes. In this paper, we present undecidability resu...
Sergio Giro
Added 27 Jul 2010
Updated 27 Jul 2010
Type Conference
Year 2009
Where SBMF
Authors Sergio Giro
Comments (0)