×

zbMATH — the first resource for mathematics

A theory for the composition of concurrent processes. (English) Zbl 1347.68267
Albert, Elvira (ed.) et al., Formal techniques for distributed objects, components, and systems. 36th IFIP WG 6.1 international conference, FORTE 2016, held as part of the 11th international federated conference on distributed computing techniques, DisCoTec 2016, Heraklion, Crete, Greece, June 6–9, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-39569-2/pbk; 978-3-319-39570-8/ebook). Lecture Notes in Computer Science 9688, 175-194 (2016).
Summary: 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.
For the entire collection see [Zbl 1339.68004].

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX Cite
Full Text: DOI
References:
[1] De Simone, R.: Higher-level synchronising devices in MEIJE-SCCS. Theor. Comput. Sci. 37, 245–267 (1985) · Zbl 0598.68027
[2] Larsen, K.G.: A context dependent equivalence between processes. Theor. Comput. Sci. 49, 184–215 (1987) · Zbl 0612.68027
[3] Hennessy, M., Lin, H.: Symbolic bisimulations. Theor. Comput. Sci. 138(2), 353–389 (1995) · Zbl 0874.68187
[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)
[5] Hennessy, M., Rathke, J.: Bisimulations for a calculus of broadcasting systems. Theor. Comput. Sci. 200(1–2), 225–260 (1998) · Zbl 0915.68065
[6] Arnold, A.: Synchronised behaviours of processes and rational relations. Acta Informatica 17, 21–29 (1982) · Zbl 0478.68027
[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)
[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) · Zbl 05622591
[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 · Zbl 06571872
[10] Rensink, A.: Bisimilarity of open terms. In: Expressiveness in Languages for Concurrency (1997) · Zbl 0911.68066
[11] Deng, Y.: Algorithm for verifying strong open bisimulation in \[ \pi \] {\(\pi\)} calculus. J. Shanghai Jiaotong Univ. 2, 147–152 (2001) · Zbl 1007.68135
[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)
[13] Clarke, E.M., Grumberg, O., Jha, S.: Verifying parameterized networks. ACM Trans. Program. Lang. Syst. 19(5), 726–750 (1997) · Zbl 01935869
[14] Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1989). SU Fisher Research 511/24
[15] Henrio, L., Madelaine, E., Zhang, M.: A theory for the composition of concurrent processes - extended version. Rapport de recherche RR-8898, INRIA, April 2016 · Zbl 1347.68267
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.