Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains

Georgel Calin; Pepijn Crouzen; Pedro R. D'Argenio; Ernst Moritz Hahn; Lijun Zhang

doi:10.1007/978-3-642-16164-3_15

Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains

Georgel Calin
, Pepijn Crouzen
, Pedro R. D'Argenio
, Ernst Moritz Hahn
, Lijun Zhang

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

4 Citations (Scopus)

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.

Original language	English
Title of host publication	Model Checking Software - 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. Proceedings
Pages	193-211
Number of pages	19
DOIs	https://doi.org/10.1007/978-3-642-16164-3_15
Publication status	Published - 2010
Externally published	Yes

Access to Document

10.1007/978-3-642-16164-3_15

https://doi.org/10.1007/978-3-642-16164-3_15

Cite this

@inproceedings{da4089719e6d4531b117ef2506e713fe,

title = "Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains",

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.",

author = "Georgel Calin and Pepijn Crouzen and D'Argenio, \{Pedro R.\} and Hahn, \{Ernst Moritz\} and Lijun Zhang",

year = "2010",

doi = "10.1007/978-3-642-16164-3\_15",

language = "English",

pages = "193--211",

booktitle = "Model Checking Software - 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. Proceedings",

}

Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains. / Calin, Georgel; Crouzen, Pepijn; D'Argenio, Pedro R. et al.
Model Checking Software - 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. Proceedings. 2010. p. 193-211.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains

AU - Calin, Georgel

AU - Crouzen, Pepijn

AU - D'Argenio, Pedro R.

AU - Hahn, Ernst Moritz

AU - Zhang, Lijun

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-16164-3_15

DO - 10.1007/978-3-642-16164-3_15

M3 - Conference contribution

SP - 193

EP - 211

BT - Model Checking Software - 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. Proceedings

ER -

Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains

Abstract

Access to Document

Fingerprint

Cite this