A fully abstract semantics for value-passing CCS for trees

doi:10.1007/s11704-018-7069-1

Front. Comput. Sci.

2019, Vol. 13

Issue (4) : 828-849 https://doi.org/10.1007/s11704-018-7069-1

RESEARCH ARTICLE

A fully abstract semantics for value-passing CCS for trees

Ying JIANG¹, Shichao LIU^1,²(

), Thomas EHRHARD³

¹. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China
². University of Chinese Academy of Sciences, Beijing 100049, China
³. CNRS, IRIF, UMR 8243, Univ Paris Diderot, Sorbonne Paris Cité, F-75205 Paris, France

Download: PDF(703 KB)
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

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

Corresponding Author(s): Shichao LIU

Just Accepted Date: 26 March 2018 Online First Date: 22 October 2018 Issue Date: 29 May 2019

Cite this article:

Ying JIANG,Shichao LIU,Thomas EHRHARD. A fully abstract semantics for value-passing CCS for trees[J]. Front. Comput. Sci., 2019, 13(4): 828-849.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-018-7069-1
https://academic.hep.com.cn/fcs/EN/Y2019/V13/I4/828

1	C A RHoare. Communicating sequential processes. Communications of the ACM, 1983, 26(1): 100–106 https://doi.org/10.1145/357980.358021
2	RMilner. Communication and Concurrency. New York etc.: Prentice- Hall, Inc., 1989
3	RMilner, JParrow, DWalker. A calculus of mobile processes, I. Information and Computation, 1992, 100(1): 1–40 https://doi.org/10.1016/0890-5401(92)90008-4
4	GBoudol, I Castellani, MHennessy, MNielsen, G Winskel. 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	GBoudol, I Castellani. A non-interleaving semantics for CCS based on proved transitions. Research Report, 1988
6	GBoudol, I Castellani, MHennessy, AKiehn. A theory of processes with localities. Formal Aspects of Computing, 1994, 6(2): 165–200 https://doi.org/10.1007/BF01221098
7	ICastellani. Process algebras with localities. Handbook of Process Algebra, 2001, 945–1045 https://doi.org/10.1016/B978-044482830-9/50033-3
8	PDegano, R De Nicola, UMontanari. A partial ordering semantics for CCS. Theoretical Computer Science, 1990, 75(3): 223–262 https://doi.org/10.1016/0304-3975(90)90095-Y
9	AKiehn. Comparing locality and causality based equivalences. Acta Informatica, 1994, 31(8): 697–718 https://doi.org/10.1007/BF01178730
10	WReisig. Petri Nets: an Introduction. Springer Science & Business Media, 1985 https://doi.org/10.1007/978-3-642-69968-9
11	GWinskel. An introduction to event structures. In: Proceedings of the Workshop of the REX Project Research and Eduction in Concurrent Systems. 1988, 364–397
12	G LFerrari, DHirsch, ILanese, U Montanari, ETuosto. 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	BKönig, U Montanari. Observational equivalence for synchronized graph rewriting with mobility. In: Proceedings of International Symposium on Theoretical Aspects of Computer Software. 2001, 145–164 https://doi.org/10.1007/3-540-45500-0_7
14	TEhrhard, YJiang. CCS for trees. 2013, arXiv preprint arXiv:1306.1714
15	TEhrhard, YJiang. A dendroidal process calculus. 2015
16	SLiu, YJiang. 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 https://doi.org/10.1109/TASE.2016.19
17	RMilner, D Sangiorgi. Barbed bisimulation. In: Proceedings of International Colloquium on Automata, Languages, and Programming. 1992, 685–695
18	ABouajjani, M Müller-Olm, TTouili. Regular symbolic analysis of dynamic networks of pushdown systems. In: Proceedings of International Conference on Concurrency Theory. 2005, 473–487 https://doi.org/10.1007/11539452_36
19	PLammich, M Müller-Olm, AWenner. Predecessor sets of dynamic pushdown networks with tree-regular constraints. In: Proceedings of International Conference on Computer Aided Verification. 2009, 525–539 https://doi.org/10.1007/978-3-642-02658-4_39
20	HComon, M Dauchet, RGilleron, CLöding, F Jacquemard, DLugiez, STison, M Tommasi. Tree automata techniques and applications.1997
21	K ABartlett, R A Scantlebury, P TWilkinson. A note on reliable fullduplex transmission over half-duplex links. Communications of the ACM, 1969, 12(5): 260–261 https://doi.org/10.1145/362946.362970
22	DSangiorgi. Introduction to Bisimulation and Coinduction. Cambridge: Cambridge University Press, 2011 https://doi.org/10.1017/CBO9780511777110
23	JEsparza, JKnoop. 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 https://doi.org/10.1007/3-540-49019-1_2
24	PLinz. An Introduction to Formal Languages and Automata. USA: Jones and Bartlett Publishers, Inc., 2011
25	JAranda, G CDi, MNielsen, F D Valencia. 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 https://doi.org/10.1007/978-3-540-76637-7_26
26	J C MBaeten, J A Bergstra, J WKlop. Decidability of bisimulation equivalence for process generating context-free languages. Journal of the ACM, 1993, 40(3): 653–682 https://doi.org/10.1145/174130.174141
27	SLiu, YJiang. 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 https://doi.org/10.1109/TASE.2016.19
28	ILanese, D Sangiorgi. An operational semantics for a calculus for wireless systems. Theoretical Computer Science, 2010, 411(19): 1928–1948 https://doi.org/10.1016/j.tcs.2010.01.023
29	ICastellani, M Hennessy. Distributed bisimulations. Journal of the ACM, 1989, 36(4): 887–911 https://doi.org/10.1145/76359.76369
30	DSangiorgi. Expressing mobility in process algebras: first-order and higher-order paradigms. University of Edinburgh, 1993
31	BBollig. Logic for communicating automata with parameterized topology. In: Proceedings of the 23th EACSL Conference on Computer Science Logic. 2014, 18 https://doi.org/10.1145/2603088.2603093
32	MMerro. An observational theory for mobile ad hoc networks (full version). Information and Computation, 2009, 207(2): 194–208 https://doi.org/10.1016/j.ic.2007.11.010
33	SNanz, CHankin. A framework for security analysis of mobile wireless networks. Theoretical Computer Science, 2006, 367(1): 203–227 https://doi.org/10.1016/j.tcs.2006.08.036

[1]

Download

[1]	Yanfang MA, Min ZHANG, Yixiang CHEN, Liang CHEN. Two-thirds simulation indexes and modal logic characterization[J]. Front Comput Sci Chin, 2011, 5(4): 454-471.

Viewed

Full text

Abstract

Cited

Shared

Discussed