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.
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.
Original language | English |
---|---|
Title of host publication | Model Checking Software |
Subtitle of host publication | 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. Proceedings |
Editors | Jaco van de Pol, Michael Weber |
Place of Publication | Berlin, Heidelberg |
Publisher | Springer |
Pages | 193-211 |
ISBN (Electronic) | 978-3-642-16164-3 |
ISBN (Print) | 978-3-642-16163-6 |
DOIs | |
Publication status | Published - 2010 |
Externally published | Yes |
Event | 17th International SPIN Workshop on Model Checking Software 2010 - University of Twente, Enschede, Netherlands Duration: 27 Sept 2010 → 29 Sept 2010 Conference number: 17 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 6349 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Workshop
Workshop | 17th International SPIN Workshop on Model Checking Software 2010 |
---|---|
Country/Territory | Netherlands |
City | Enschede |
Period | 27/09/10 → 29/09/10 |
Keywords
- n/a OA procedure