Submitted: July 2008
Abstract
This thesis introduces a model for asynchronous distributed systems which uses event-based communication and which is based on Switched PIOA. In order to enable model checking on these systems, we are interested in the probability of reaching a set of target states. Since we work on nondeterministic systems, we have to ask for the maximum reachability probability. We discuss why omniscient (arbitrary) schedulers yield counterintuitive probabilities and we show why that problem is undecidable for more realistic schedulers (distributed schedulers). The purpose of this thesis is to push the search for a decidable but non-trivial upper bound of the maximum reachability probability under the distributed schedulers. We give a discussion about which scheduler class is an appropriate candidate, as well as a possible algorithm and a proof strategy for the correctness of that algorithm.