A Theory for the Composition of Concurrent Processes

  • Ludovic Henrio
  • Eric MadelaineEmail author
  • Min Zhang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9688)


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.


Open Transition Composition Operator Operational Semantic Label Transition System Concurrent Process 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    De Simone, R.: Higher-level synchronising devices in MEIJE-SCCS. Theor. Comput. Sci. 37, 245–267 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Larsen, K.G.: A context dependent equivalence between processes. Theor. Comput. Sci. 49, 184–215 (1987)CrossRefzbMATHGoogle Scholar
  3. 3.
    Hennessy, M., Lin, H.: Symbolic bisimulations. Theor. Comput. Sci. 138(2), 353–389 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Lin, H.: Symbolic transition graph with assignment. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 50–65. Springer, Heidelberg (1996)Google Scholar
  5. 5.
    Hennessy, M., Rathke, J.: Bisimulations for a calculus of broadcasting systems. Theor. Comput. Sci. 200(1–2), 225–260 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Arnold, A.: Synchronised behaviours of processes and rational relations. Acta Informatica 17, 21–29 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Henrio, L., Madelaine, E., Zhang, M.: pNets: an expressive model for parameterisednetworks of processes. In: 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP 2015) (2015)Google Scholar
  8. 8.
    Cansado, A., Madelaine, E.: Specification and verification for grid component-based applications: from models to tools. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds.) FMCO 2008. LNCS, vol. 5751, pp. 180–203. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  9. 9.
    Henrio, L., Kulankhina, O., Li, S., Madelaine, E.: Integrated environment for verifying and running distributed components. In: Stevens, P. (ed.) FASE 2016. LNCS, vol. 9633, pp. 66–83. Springer, Heidelberg (2016). doi: 10.1007/978-3-662-49665-7_5 CrossRefGoogle Scholar
  10. 10.
    Rensink, A.: Bisimilarity of open terms. In: Expressiveness in Languages for Concurrency (1997)Google Scholar
  11. 11.
    Deng, Y.: Algorithm for verifying strong open bisimulation in \(\pi \) calculus. J. Shanghai Jiaotong Univ. 2, 147–152 (2001)zbMATHGoogle Scholar
  12. 12.
    Bultan, T., Gerber, R., Pugh, W.: Symbolic model checking of infinite state systems using presburger arithmetic. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 400–411. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  13. 13.
    Clarke, E.M., Grumberg, O., Jha, S.: Verifying parameterized networks. ACM Trans. Program. Lang. Syst. 19(5), 726–750 (1997)CrossRefGoogle Scholar
  14. 14.
    Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1989). SU Fisher Research 511/24zbMATHGoogle Scholar
  15. 15.
    Henrio, L., Madelaine, E., Zhang, M.: A theory for the composition of concurrent processes - extended version. Rapport de recherche RR-8898, INRIA, April 2016Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2016

Authors and Affiliations

  1. 1.University of Nice Sophia Antipolis, CNRS, UMR 7271Sophia AntipolisFrance
  2. 2.INRIA Sophia Antipolis MéditérannéeSophia AntipolisFrance
  3. 3.Shanghai Key Laboratory of Trustworthy ComputingECNUShanghaiChina

Personalised recommendations