Reduction Semantics in Markovian Process Algebra

Mario Bravetti 1, 2
1 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : Markovian process algebras allow for performance analysis by automatic generation of Continuous Time Markov Chains. The inclusion of exponential distribution rate information in process algebra terms, however, causes non trivial issues to arise in the definition of their semantics. As a consequence, technical settings previously considered do not make it possible to base Markovian semantics on directly computing reductions between communicating processes: this would require the ability to readjust processes, i.e. a commutative and associative parallel operator and a congruence relation on terms enacting such properties. Semantics in reduction style is, however, often used for complex languages, due to its simplicity and conciseness. In this paper we introduce a new technique based on stochastic binders that allows us to define Markovian semantics in the presence of such a structural congruence. As application examples, we define the reduction semantics of Markovian versions of the π-calculus, considering both the cases of Markovian durations: being additional standalone prefixes (as in Interactive Markov Chains) and being, instead, associated to standard synchro-nizable actions, giving them a duration (as in Stochastic π-calculus). Notably, in the latter case, we obtain a "natural" Markovian semantics for π-calculus (CCS) parallel that preserves, for the first time, its associativity. In both cases we show our technique for defining reduction semantics to be correct with respect to the standard Markovian one (in labeled style) by providing Markovian extensions of the classical π-calculus Harmony theorem.
Document type :
Journal articles
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/hal-01921194
Contributor : Mario Bravetti <>
Submitted on : Tuesday, November 13, 2018 - 4:32:20 PM
Last modification on : Thursday, November 15, 2018 - 1:20:08 AM
Long-term archiving on : Thursday, February 14, 2019 - 3:57:02 PM

File

jlamp.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Mario Bravetti. Reduction Semantics in Markovian Process Algebra. Journal of Logical and Algebraic Methods in Programming, Elsevier, 2018, 96, pp.41-64. ⟨10.1016/j.jlamp.2018.01.002⟩. ⟨hal-01921194⟩

Share

Metrics

Record views

46

Files downloads

91