×

A ground-complete axiomatization of stateless bisimilarity over Linda. (English) Zbl 1302.68198

Summary: This paper offers a finite, ground-complete axiomatization of stateless bisimilarity over the tuple-space-based coordination language Linda. As stepping stones towards that result, axiomatizations of stateless bisimilarity over the sequential fragment of Linda without the nask primitive, and over the full sequential sub-language are given. It is also shown that stateless bisimilarity coincides with standard bisimilarity over the sequential fragment of Linda without the nask primitive.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

Reo; Linda
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aceto, L.; Fokkink, W.; Ingólfsdóttir, A.; Luttik, B., Finite equational bases in process algebra: results and open questions, (Processes, Terms and Cycles. Processes, Terms and Cycles, Lect. Notes Comput. Sci., vol. 3838 (2005), Springer), 338-367 · Zbl 1171.68558
[2] Arbab, F., Reo: a channel-based coordination model for component composition, Math. Struct. Comput. Sci., 14, 3, 1-38 (2004) · Zbl 1085.68552
[3] Baeten, J. C.; Basten, T.; Reniers, M. A., Process Algebra: Equational Theories of Communicating Processes, Camb. Tracts Theor. Comput. Sci., vol. 50 (2010), Cambridge University Press · Zbl 1234.68001
[4] Baeten, J. C.M., Embedding untimed into timed process algebra: the case for explicit termination, Math. Struct. Comput. Sci., 13, 4, 589-618 (2003) · Zbl 1088.68118
[5] Basu, A.; Bensalem, S.; Bozga, M.; Combaz, J.; Jaber, M.; Nguyen, T.-H.; Sifakis, J., Rigorous component-based system design using the BIP framework, IEEE Softw., 28, 3, 41-48 (2011)
[6] Bergstra, J. A.; Klop, J. W., Fixedpoint semantics in process algebra (1982), Center for Mathematics: Center for Mathematics Amsterdam, The Netherlands, Technical Report IW 206/82
[7] Bliudze, S.; Sifakis, J., The algebra of connectors — structuring interaction in BIP, IEEE Trans. Comput., 57, 10, 1315-1330 (2008) · Zbl 1390.68031
[8] Bos, V.; Kleijn, J. J., Redesign of a systems engineering language — formalisation of \(χ\), Form. Asp. Comput., 15, 4, 370-389 (2003) · Zbl 1093.68597
[9] Brogi, A.; Jacquet, J.-M., On the expressiveness of Linda-like concurrent languages, (Castellani, I.; Palamidessi, C., Proceedings of the 5th International Workshop on Expressiveness in Concurrency. Proceedings of the 5th International Workshop on Expressiveness in Concurrency, EXPRESS’98. Proceedings of the 5th International Workshop on Expressiveness in Concurrency. Proceedings of the 5th International Workshop on Expressiveness in Concurrency, EXPRESS’98, Electron. Notes Theor. Comput. Sci., vol. 16 (1998), Elsevier Science: Elsevier Science Dordrecht, The Netherlands) · Zbl 0917.68026
[10] Busi, N.; Gorrieri, R.; Zavattaro, G., A process algebraic view of Linda coordination primitives, Theor. Comput. Sci., 192, 167-199 (1998) · Zbl 0895.68016
[11] Carriero, N.; Gelernter, D., Linda in context, Commun. ACM, 32, 4, 444-458 (1989)
[12] Cuijpers, P. J.; Reniers, M. A., Hybrid process algebra, J. Log. Algebr. Program., 62, 2, 191-245 (2005) · Zbl 1090.68071
[13] De Nicola, R.; Hennessy, M., Testing equivalences for processes, Theor. Comput. Sci., 34, 83-133 (1984) · Zbl 0985.68518
[14] De Nicola, R.; Pugliese, R., Linda-based applicative and imperative process algebras, Theor. Comput. Sci., 238, 1-2, 389-437 (2000) · Zbl 0944.68064
[15] Gelernter, D., Generative communication in Linda, ACM Trans. Program. Lang. Syst., 7, 1, 80-112 (1985) · Zbl 0559.68030
[16] Groote, J. F., A new strategy for proving \(ω\)-completeness applied to process algebra, (Baeten, J. C.M.; Klop, J. W., Theories of Concurrency: Unification and Extension. Theories of Concurrency: Unification and Extension, CONCUR’90, Amsterdam, The Netherlands, August 27-30, 1990, Proceedings. Theories of Concurrency: Unification and Extension. Theories of Concurrency: Unification and Extension, CONCUR’90, Amsterdam, The Netherlands, August 27-30, 1990, Proceedings, Lect. Notes Comput. Sci., vol. 458 (1990), Springer), 314-331
[17] Groote, J. F.; Ponse, A., Process algebra with guards: combining Hoare logic with process algebra, Form. Asp. Comput., 6, 2, 115-164 (1994) · Zbl 0806.68078
[18] Hennessy, M.; Ingólfsdóttir, A., Communicating processes with value-passing and assignments, Form. Asp. Comput., 5, 5, 432-466 (1993) · Zbl 0784.68055
[19] Hennessy, M.; Ingólfsdóttir, A., A theory of communicating processes with value passing, Inf. Comput., 107, 2, 202-236 (1993) · Zbl 0794.68098
[20] Hennessy, M.; Lin, H.; Rathke, J., Unique fixpoint induction for message-passing process calculi, Sci. Comput. Program., 41, 3, 241-275 (2001) · Zbl 0998.68089
[21] Milner, A. R., Communication and Concurrency (1989), Prentice Hall · Zbl 0683.68008
[22] Milner, A. R.; Sangiorgi, D., Barbed bisimulation, (Kuich, W., Proceedings of 19th International Colloquium on Automata, Languages and Programming. Proceedings of 19th International Colloquium on Automata, Languages and Programming, ICALP’92. Proceedings of 19th International Colloquium on Automata, Languages and Programming. Proceedings of 19th International Colloquium on Automata, Languages and Programming, ICALP’92, Lect. Notes Comput. Sci., vol. 623 (1992), Springer-Verlag: Springer-Verlag Berlin, Germany), 85-695 · Zbl 1425.68298
[23] Moller, F., The importance of the left merge operator in process algebras, (Paterson, M., Automata, Languages and Programming, 17th International Colloquium. Automata, Languages and Programming, 17th International Colloquium, ICALP90, Warwick University, England, July 16-20, 1990, Proceedings. Automata, Languages and Programming, 17th International Colloquium. Automata, Languages and Programming, 17th International Colloquium, ICALP90, Warwick University, England, July 16-20, 1990, Proceedings, Lect. Notes Comput. Sci., vol. 443 (1990), Springer), 752-764 · Zbl 0774.68039
[24] Mousavi, M. R.; Reniers, M. A.; Groote, J. F., Notions of bisimulation and congruence formats for SOS with data, Inf. Comput., 200, 1, 107-147 (2005) · Zbl 1082.68075
[25] Park, D. M., Concurrency and automata on infinite sequences, (Proceedings of the 5th GI Conference. Proceedings of the 5th GI Conference, Lect. Notes Comput. Sci., vol. 104 (1981), Springer-Verlag), 167-183
[26] Vrancken, J. L.M., The algebra of communicating processes with empty process, Theor. Comput. Sci., 177, 2, 287-328 (1997) · Zbl 0901.68112
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.