%0 Conference Proceedings
%T A Theory for the Composition of Concurrent Processes
%+ Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S)
%+ Logical Time for Formal Embedded System Design (KAIROS)
%+ East China Normal University [Shangaï] (ECNU)
%A Henrio, Ludovic
%A Madelaine, Eric
%A Zhang, Min
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Heraklion, Greece
%Y Elvira Albert
%Y Ivan Lanese
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-9688
%P 175-194
%8 2016-06-06
%D 2016
%R 10.1007/978-3-319-39570-8_12
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01432917/document
%2 https://inria.hal.science/hal-01432917/file/426757_1_En_12_Chapter.pdf
%L hal-01432917
%U https://inria.hal.science/hal-01432917
%~ UNICE
%~ CNRS
%~ INRIA
%~ INRIA-SOPHIA
%~ I3S
%~ INRIASO
%~ INRIA_TEST
%~ LORIA2
%~ TESTALAIN1
%~ IFIP-LNCS
%~ IFIP
%~ INRIA2
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-9688
%~ UNIV-COTEDAZUR