Quantitative Analysis of Distributed Randomized Protocols

Christel BaierChristel Baier, Frank CiesinskiFrank Ciesinski, Marcus GrößerMarcus Größer

DOI Link

Christel Baier, Frank Ciesinski, Marcus Größer
Quantitative Analysis of Distributed Randomized Protocols
Proc. of the 10th International Workshop on Formal Methods for Industrial Critical Systems (FMICS), 2--7, 2005. ACM Press

Details
Bibtex

KurzfassungAbstract
A wide range of coordination protocols for distributed systems, internet protocols or systems with unreliable components can formally be modelled by Markov decision processes (MDP). MDPs can be viewed as a variant of state-transition diagrams with discrete probabilities and nondeterminism. While traditional model checking techniques for non-probabilistic systems aim to establish properties stating that all (or some) computations fulfill a certain condition, the verification problem for randomized systems requires reasoning about the quantitative behavior by means of properties that refer to the probabilities for certain computations, for instance, the probability to find a leader within 5 rounds or the probability for not reaching an error state.The paper starts with a brief introduction into modelling randomized systems with MDPs and the modelling language ProbMela which is a guarded command language with features of imperative languages, nondeterminism, parallelism, a probabilistic choice operator and lossy channels. We summarize the main steps for a quantitative analysis of MDPs against linear temporal logical specifications. The last part will report on the main features of the partial order reduction approach for MDPs and its implementation in the model checker LiQuor.
Forschungsgruppe:Research Group: Verifikation und formale quantitative Analyse„Verifikation und formale quantitative Analyse“ befindet sich nicht in der Liste (Computational Logic, Automatentheorie, Wissensverarbeitung, Knowledge-Based Systems, Knowledge Systems, Wissensbasierte Systeme, Logische Programmierung und Argumentation, Algebra und Diskrete Strukturen, Knowledge-aware Artificial Intelligence, Algebraische und logische Grundlagen der Informatik) zulässiger Werte für das Attribut „Forschungsgruppe“.Algebraic and Logical Foundations of Computer Science

@inproceedings{BCG2005,
  author    = {Christel Baier and Frank Ciesinski and Marcus Gr{\"{o}}{\ss}er},
  title     = {Quantitative Analysis of Distributed Randomized Protocols},
  booktitle = {Proc. of the 10th International Workshop on Formal Methods for
               Industrial Critical Systems (FMICS)},
  publisher = {ACM Press},
  year      = {2005},
  pages     = {2--7},
  doi       = {10.1145/1081180.1081182}
}