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 › Academic › peer-review

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
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	https://doi.org/10.1007/978-3-642-16164-3_15
Publication status	Published - 2010
Externally published	Yes
Event	17th International SPIN Workshop on Model Checking Software 2010 - University of Twente, Enschede, Netherlands Duration: 27 Sep 2010 → 29 Sep 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

Access to Document

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

Cite this

Calin, G., Crouzen, P., D'Argenio, P. R., Hahn, E. M., & Zhang, L. (2010). Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains. In J. van de Pol, & M. Weber (Eds.), Model Checking Software: 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. Proceedings (pp. 193-211). (Lecture Notes in Computer Science; Vol. 6349). Springer. https://doi.org/10.1007/978-3-642-16164-3_15

Calin, Georgel ; Crouzen, Pepijn ; D'Argenio, Pedro R. ; Hahn, Ernst Moritz ; Zhang, Lijun. / Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains. Model Checking Software: 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. Proceedings. editor / Jaco van de Pol ; Michael Weber. Berlin, Heidelberg : Springer, 2010. pp. 193-211 (Lecture Notes in Computer Science).

@inproceedings{655a5c65660e4a69887f48e505de3186,

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

isbn = "978-3-642-16163-6",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "193--211",

editor = "{van de Pol}, Jaco and Michael Weber",

booktitle = "Model Checking Software",

address = "Netherlands",

note = "17th International SPIN Workshop on Model Checking Software 2010 ; Conference date: 27-09-2010 Through 29-09-2010",

}

Calin, G, Crouzen, P, D'Argenio, PR, Hahn, EM & Zhang, L 2010, Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains. in J van de Pol & M Weber (eds), Model Checking Software: 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6349, Springer, Berlin, Heidelberg, pp. 193-211, 17th International SPIN Workshop on Model Checking Software 2010, Enschede, Netherlands, 27/09/10. https://doi.org/10.1007/978-3-642-16164-3_15

Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains. / Calin, Georgel; Crouzen, Pepijn; D'Argenio, Pedro R.; Hahn, Ernst Moritz ; Zhang, Lijun.

Model Checking Software: 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. Proceedings. ed. / Jaco van de Pol; Michael Weber. Berlin, Heidelberg : Springer, 2010. p. 193-211 (Lecture Notes in Computer Science; Vol. 6349).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

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

N1 - Conference code: 17

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

SN - 978-3-642-16163-6

T3 - Lecture Notes in Computer Science

SP - 193

EP - 211

BT - Model Checking Software

A2 - van de Pol, Jaco

A2 - Weber, Michael

PB - Springer

CY - Berlin, Heidelberg

T2 - 17th International SPIN Workshop on Model Checking Software 2010

Y2 - 27 September 2010 through 29 September 2010

ER -

Calin G, Crouzen P, D'Argenio PR, Hahn EM, Zhang L. Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains. In van de Pol J, Weber M, editors, Model Checking Software: 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. Proceedings. Berlin, Heidelberg: Springer. 2010. p. 193-211. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-16164-3_15

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

Abstract

Publication series

Workshop

Access to Document

Fingerprint

Cite this