A Theory for the Composition of Concurrent Processes

Ludovic Henrio 1 Eric Madelaine 1, 2 Min Zhang 3
2 KAIROS - Logical Time for Formal Embedded System Design
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : In this paper, we provide a theory for the operators composing concurrent processes. Open pNets (parameterised networks of synchronised automata) are new semantic objects that we propose for defining the semantics of composition operators. This paper defines the operational semantics of open pNets, using “open transitions” that include symbolic hypotheses on the behaviour of the pNets “holes”. We discuss when this semantics can be finite and how to compute it symbolically, and we illustrate this construction on a simple operator. This paper also defines a bisimulation equivalence between open pNets, and shows its decidability together with a congruence theorem.
Complete list of metadatas

Cited literature [15 references]  Display  Hide  Download

https://hal.inria.fr/hal-01432917
Contributor : Hal Ifip <>
Submitted on : Thursday, January 12, 2017 - 11:34:17 AM
Last modification on : Monday, February 11, 2019 - 10:10:02 AM
Long-term archiving on : Friday, April 14, 2017 - 11:54:43 AM

File

426757_1_En_12_Chapter.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Ludovic Henrio, Eric Madelaine, Min Zhang. A Theory for the Composition of Concurrent Processes. 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2016, Heraklion, Greece. pp.175-194, ⟨10.1007/978-3-319-39570-8_12⟩. ⟨hal-01432917⟩

Share

Metrics

Record views

407

Files downloads

108