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 proceedingConference contributionAcademicpeer-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 languageEnglish
Title of host publicationModel Checking Software
Subtitle of host publication17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. Proceedings
EditorsJaco van de Pol, Michael Weber
Place of PublicationBerlin, Heidelberg
PublisherSpringer
Pages193-211
ISBN (Electronic)978-3-642-16164-3
ISBN (Print)978-3-642-16163-6
DOIs
Publication statusPublished - 2010
Externally publishedYes
Event17th International SPIN Workshop on Model Checking Software 2010 - University of Twente, Enschede, Netherlands
Duration: 27 Sep 201029 Sep 2010
Conference number: 17

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume6349
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Workshop

Workshop17th International SPIN Workshop on Model Checking Software 2010
CountryNetherlands
CityEnschede
Period27/09/1029/09/10

Fingerprint

Dive into the research topics of 'Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains'. Together they form a unique fingerprint.

Cite this