Reduction Semantics in Markovian Process Algebra - Archive ouverte HAL Access content directly
Journal Articles Journal of Logical and Algebraic Methods in Programming Year : 2018

Reduction Semantics in Markovian Process Algebra

(1, 2)
1
2

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.
Fichier principal
Vignette du fichier
jlamp.pdf (578.99 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01921194 , version 1 (13-11-2018)

Identifiers

Cite

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

Altmetric

Share

Gmail Facebook Twitter LinkedIn More