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.
Original languageUndefined
Title of host publication24th International Conference on Concurrency Theory, CONCUR 2013
Place of PublicationLondon
PublisherSpringer Verlag
Pages44-45
Number of pages2
ISBN (Print)978-3-642-40183-1
DOIs
StatePublished - Aug 2013
Event24th International Conference on Concurrency Theory, CONCUR 2013 - Buenos Aires, Argentina

Publication series

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

Conference

Conference24th International Conference on Concurrency Theory, CONCUR 2013
Abbreviated titleCONCUR
CountryArgentina
CityBuenos Aires
Period27/08/1330/08/13

Fingerprint

Semantics
Petri nets
Chemical analysis
Linear programming
Markov processes
Algebra
Testing
Industry

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

Katoen, J. P. (2013). Concurrency meets probability: theory and practice (abstract). In 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

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

24th International Conference on Concurrency Theory, CONCUR 2013. London : Springer Verlag, 2013. p. 44-45 (Lecture Notes in Computer Science; Vol. 8052).

Research output: ScientificConference contribution

@inbook{f18633f6ac0b481b8ab216509678472d,
title = "Concurrency meets probability: theory and practice (abstract)",
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.",
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",
author = "Katoen, {Joost P.}",
note = "eemcs-eprint-23888",
year = "2013",
month = "8",
doi = "10.1007/978-3-642-40184-8_4",
isbn = "978-3-642-40183-1",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "44--45",
booktitle = "24th International Conference on Concurrency Theory, CONCUR 2013",

}

Katoen, JP 2013, Concurrency meets probability: theory and practice (abstract). in 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.

24th International Conference on Concurrency Theory, CONCUR 2013. London : Springer Verlag, 2013. p. 44-45 (Lecture Notes in Computer Science; Vol. 8052).

Research output: ScientificConference 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 -

Katoen JP. Concurrency meets probability: theory and practice (abstract). In 24th International Conference on Concurrency Theory, CONCUR 2013. London: Springer Verlag. 2013. p. 44-45. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-642-40184-8_4