2010 | OriginalPaper | Buchkapitel
Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains
verfasst von : Georgel Calin, Pepijn Crouzen, Pedro R. D’Argenio, E. Moritz Hahn, Lijun Zhang
Erschienen in: Model Checking Software
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.