Concurrency meets probability: theory and practice (abstract)

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.