Conference paper
Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains
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.
Language: | English |
---|---|
Publisher: | Springer Berlin Heidelberg |
Year: | 2010 |
Pages: | 193-211 |
Proceedings: | 17th International SPIN Workshop |
ISBN: | 1280389591 , 3642161634 , 3642161642 , 9781280389597 , 9783642161636 and 9783642161643 |
ISSN: | 16113349 and 03029743 |
Types: | Conference paper |
DOI: | 10.1007/978-3-642-16164-3_15 |