Concurrency meets probability: theory and practice (abstract)

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

    12 Downloads (Pure)


    Treating random phenomena in concurrency theory has a long tradition. Petri nets [18, 10] and process algebras [14] have been extended with probabilities. The same applies to behavioural semantics such as strong and weak (bi)simulation [1], and testing pre-orders [5]. Beautiful connections between probabilistic bisimulation [16] and Markov chain lumping [15] have been found. A plethora of probabilistic concurrency models has emerged [19]. Over the years, the focus shifted from covering discrete to treating continuous stochastic phenomena [12, 13]. We argue that both aspects can be elegantly combined with non-determinism, yielding the Markov automata model [8]. This model has nice theoretical characteristics. It is closed under parallel composition and hiding. Conservative extensions of (bi)simulation are congruences [8, 4]. It has a simple process algebraic counterpart [20]. On-the-fly partial-order reduction yields substantial state-space reductions [21]. Their quantitative analysis largely depends on (efficient) linear programming and scales well [11]. More importantly though: Markov automata serve an important practical need. They are the obvious choice for providing semantics to the Architecture Analysis & Design Language (AADL [9]), an industry standard for the automotive and aerospace domain. As experienced in several ESA projects, this holds in particular for the AADL annex dealing with error models [3]. They provide a compositional semantics to dynamic fault trees [6], a key model for reliability engineering [2]. Finally, they give a natural semantics to every generalised stochastic Petri net (GSPN [17]), a prominent model in performance analysis. This conservatively extends the existing GSPN semantics that is restricted to well-defined" nets, i.e., nets without non-determinism [7]. Powerful software tools support this and incorporate ecient analysis and minimisation algorithms [11]. This substantiates our take-home message: Markov automata bridge the gap between an elegant theory and practical engineering needs.
    Original languageUndefined
    Title of host publication24th International Conference on Concurrency Theory, CONCUR 2013
    Place of PublicationLondon
    Number of pages2
    ISBN (Print)978-3-642-40183-1
    Publication statusPublished - Aug 2013
    Event24th International Conference on Concurrency Theory, CONCUR 2013 - Buenos Aires, Argentina
    Duration: 27 Aug 201330 Aug 2013
    Conference number: 24

    Publication series

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


    Conference24th International Conference on Concurrency Theory, CONCUR 2013
    Abbreviated titleCONCUR
    CityBuenos Aires


    • EC Grant Agreement nr.: FP7/2007-2013
    • EC Grant Agreement nr.: FP7/295261
    • EC Grant Agreement nr.: FP7/318490
    • IR-88303
    • EWI-23888
    • METIS-300116
    • EC Grant Agreement nr.: FP7/257005

    Cite this