### Abstract

Original language | Undefined |
---|---|

Title of host publication | 24th International Conference on Concurrency Theory, CONCUR 2013 |

Place of Publication | London |

Publisher | Springer Verlag |

Pages | 44-45 |

Number of pages | 2 |

ISBN (Print) | 978-3-642-40183-1 |

DOIs | |

State | Published - Aug 2013 |

Event | 24th International Conference on Concurrency Theory, CONCUR 2013 - Buenos Aires, Argentina |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer Verlag |

Volume | 8052 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Conference

Conference | 24th International Conference on Concurrency Theory, CONCUR 2013 |
---|---|

Abbreviated title | CONCUR |

Country | Argentina |

City | Buenos Aires |

Period | 27/08/13 → 30/08/13 |

### Fingerprint

### Keywords

- 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

*24th International Conference on Concurrency Theory, CONCUR 2013*(pp. 44-45). (Lecture Notes in Computer Science; Vol. 8052). London: Springer Verlag. DOI: 10.1007/978-3-642-40184-8_4

}

*24th International Conference on Concurrency Theory, CONCUR 2013.*Lecture Notes in Computer Science, vol. 8052, Springer Verlag, London, pp. 44-45, 24th International Conference on Concurrency Theory, CONCUR 2013, Buenos Aires, Argentina, 27-30 August. DOI: 10.1007/978-3-642-40184-8_4

**Concurrency meets probability: theory and practice (abstract).** / Katoen, Joost P.

Research output: Scientific › Conference contribution

TY - CHAP

T1 - Concurrency meets probability: theory and practice (abstract)

AU - Katoen,Joost P.

N1 - eemcs-eprint-23888

PY - 2013/8

Y1 - 2013/8

N2 - 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.

AB - 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.

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - EC Grant Agreement nr.: FP7/295261

KW - EC Grant Agreement nr.: FP7/318490

KW - IR-88303

KW - EWI-23888

KW - METIS-300116

KW - EC Grant Agreement nr.: FP7/257005

U2 - 10.1007/978-3-642-40184-8_4

DO - 10.1007/978-3-642-40184-8_4

M3 - Conference contribution

SN - 978-3-642-40183-1

T3 - Lecture Notes in Computer Science

SP - 44

EP - 45

BT - 24th International Conference on Concurrency Theory, CONCUR 2013

PB - Springer Verlag

ER -