A fully abstract semantics for value-passing CCS for trees

Abstract

We propose a fully abstract semantics for valuepassing CCS for trees (VCCTS) with the feature that processes are located at the vertices of a graph whose edges describe possible interaction capabilities. The operational semantics is given both in terms of a reduction semantics and in terms of a labelled transition semantics. We develop a theory of behavioral equivalences by introducing both weak barbed congruence and weak bisimilarity. In particular, we show that, on image-finite processes, weak barbed congruence coincides with weak bisimilarity. To illustrate potential applications and the powerful expressiveness of VCCTS, we formally compare VCCTS with some well-known models, e.g., dynamic pushdown networks, top-down tree automata and value-passing CCS.

Keywords

process calculus / non-interleaving semantics / barbed congruence / bisimulation

References

[1] Hoare C A R. Communicating sequential processes. Communications of the ACM, 1983, 26(1): 100–106

[2] Milner R. Communication and Concurrency. New York etc.: Prentice- Hall, Inc., 1989

[3] Milner R, Parrow J, Walker D. A calculus of mobile processes, I. Information and Computation, 1992, 100(1): 1–40

[4] Boudol G, Castellani I, Hennessy M, Nielsen M, Winskel G. Twenty Years on: Reflections on the CEDISYS Project. Combining True Concurrency with Process Algebra. Concurrency, Graphs and Models. Springer, Berlin, Heidelberg, 2008, 757–777

[5] Boudol G, Castellani I. A non-interleaving semantics for CCS based on proved transitions. Research Report, 1988

[6] Boudol G, Castellani I, Hennessy M, Kiehn A. A theory of processes with localities. Formal Aspects of Computing, 1994, 6(2): 165–200

[7] Castellani I. Process algebras with localities. Handbook of Process Algebra, 2001, 945–1045

[8] Degano P, De Nicola R, Montanari U. A partial ordering semantics for CCS. Theoretical Computer Science, 1990, 75(3): 223–262

[9] Kiehn A. Comparing locality and causality based equivalences. Acta Informatica, 1994, 31(8): 697–718

[10] Reisig W. Petri Nets: an Introduction. Springer Science & Business Media, 1985

[11] Winskel G. An introduction to event structures. In: Proceedings of the Workshop of the REX Project Research and Eduction in Concurrent Systems. 1988, 364–397

[12] Ferrari G L, Hirsch D, Lanese I, Montanari U, Tuosto E. Synchronised hyperedge replacement as a model for service oriented computing. In: Proceedings of International Symposium on FormalMethods for Components and Objects. 2005, 22–43

[13] König B, Montanari U. Observational equivalence for synchronized graph rewriting with mobility. In: Proceedings of International Symposium on Theoretical Aspects of Computer Software. 2001, 145–164

[14] Ehrhard T, Jiang Y. CCS for trees. 2013, arXiv preprint arXiv:1306.1714

[15] Ehrhard T, Jiang Y. A dendroidal process calculus. 2015

[16] Liu S, Jiang Y. Value-passing CCS for trees: a theory for concurrent systems. In: Proceedings of the 10th International Symposium on Theoretical Aspects of Software Engineering. 2016, 101–108

[17] Milner R, Sangiorgi D. Barbed bisimulation. In: Proceedings of International Colloquium on Automata, Languages, and Programming. 1992, 685–695

[18] Bouajjani A, Müller-Olm M, Touili T. Regular symbolic analysis of dynamic networks of pushdown systems. In: Proceedings of International Conference on Concurrency Theory. 2005, 473–487

[19] Lammich P, Müller-Olm M, Wenner A. Predecessor sets of dynamic pushdown networks with tree-regular constraints. In: Proceedings of International Conference on Computer Aided Verification. 2009, 525–539

[20] Comon H, Dauchet M, Gilleron R, Löding C, Jacquemard F, Lugiez D, Tison S, Tommasi M. Tree automata techniques and applications.1997

[21] Bartlett K A, Scantlebury R A, Wilkinson P T. A note on reliable fullduplex transmission over half-duplex links. Communications of the ACM, 1969, 12(5): 260–261

[22] Sangiorgi D. Introduction to Bisimulation and Coinduction. Cambridge: Cambridge University Press, 2011

[23] Esparza J, Knoop J. An automata-theoretic approach to interprocedural data-flow analysis. In: Proceedings of International Conference on Foundations of Software Science and Computation Structure. 1999, 14–30

[24] Linz P. An Introduction to Formal Languages and Automata. USA: Jones and Bartlett Publishers, Inc., 2011

[25] Aranda J, Di G C, Nielsen M, Valencia F D. CCS with replication in the chomsky hierarchy: the expressive power of divergence. In: Proceedings of Asian Symposium on Programming Languages and Systems. 2007, 383–398

[26] Baeten J C M, Bergstra J A, Klop J W. Decidability of bisimulation equivalence for process generating context-free languages. Journal of the ACM, 1993, 40(3): 653–682

[27] Liu S, Jiang Y. Value-passing CCS for trees: a theory for concurrent systems. In: Proceedings of the 10th International Symposium on Theoretical Aspects of Software Engineering. 2016, 101–108

[28] Lanese I, Sangiorgi D. An operational semantics for a calculus for wireless systems. Theoretical Computer Science, 2010, 411(19): 1928–1948

[29] Castellani I, Hennessy M. Distributed bisimulations. Journal of the ACM, 1989, 36(4): 887–911

[30] Sangiorgi D. Expressing mobility in process algebras: first-order and higher-order paradigms. University of Edinburgh, 1993

[31] Bollig B. Logic for communicating automata with parameterized topology. In: Proceedings of the 23th EACSL Conference on Computer Science Logic. 2014, 18

[32] Merro M. An observational theory for mobile ad hoc networks (full version). Information and Computation, 2009, 207(2): 194–208

[33] Nanz S, Hankin C. A framework for security analysis of mobile wireless networks. Theoretical Computer Science, 2006, 367(1): 203–227

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag GmbH Germany, part of Springer Nature