Time-Bounded Reachability in Distributed Input/Output Interactive
In Model Checking Software - 17th International SPIN Workshop
, pages 193-211, Springer
, Lecture Notes in Computer Science 6349, 2010.Downloads: pdf, bibURL: http://dx.doi.org/10.1007/978-3-642-16164-3_15
Abstract. We develop an algorithm to compute timed reachability
probabilities for distributed models which are both probabilistic and
nondeterministic. To obtain realistic results we consider the recently
introduced class of (strongly) distributed schedulers, for which no analysis
techniques are known.
Our algorithm is based on reformulating the nondeterministic models as
parametric ones, by interpreting scheduler decisions as parameters. We then
apply the PARAM tool to extract the reachability probability as a polynomial
function, which we optimize using nonlinear programming.