Skip to Main content Skip to Navigation
Journal articles

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 metadata

Cited literature [24 references]  Display  Hide  Download
Contributor : Mario Bravetti Connect in order to contact the contributor
Submitted on : Tuesday, November 13, 2018 - 4:32:20 PM
Last modification on : Friday, October 30, 2020 - 12:04:03 PM
Long-term archiving on: : Thursday, February 14, 2019 - 3:57:02 PM


Files produced by the author(s)




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⟩



Record views


Files downloads