Quantitative Analysis of Randomized Distributed Systems and Probabilistic Automata

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-review

Abstract

The automata-based model checking approach for randomized distributed systems relies on an operational interleaving semantics of the system by means of a Markov decision process (MDP) and a formalization of the desired event E by an ω-regular linear-time property, e.g., an LTL formula. The task is then to compute the greatest lower bound for the probability for E that can be guaranteed even in worst-case scenarios. Such bounds can be computed by a combination of polynomially time-bounded graph algorithm with methods for solving linear programs.

Details

Original languageEnglish
Title of host publicationAlgebraic Informatics
EditorsTraian Muntean, Dimitrios Poulakis, Robert Rolland
PublisherSpringer, Berlin [u. a.]
Pages4-5
Number of pages2
ISBN (print)978-3-642-40662-1
Publication statusPublished - 2013
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science, Volume 8080
ISSN0302-9743

Conference

Title5th International Conference on Algebraic Informatics
Abbreviated titleCAI 2013
Conference number
Duration3 - 6 September 2013
Degree of recognitionInternational event
Location
CityPorquerolles
CountryFrance

External IDs

Scopus 84884707437
ORCID /0000-0002-5321-9343/work/142236748

Keywords

Keywords

  • Randomized Distributed Systems, Probabilistic Automata

Library keywords