A fully abstract semantics for value-passing CCS for trees  

作　　者：Ying JIANG Shichao LIU Thomas EHRHARD 

机构地区：[1]State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China [2]University of Chinese Academy of Sciences, Beijing 100049, China [3]CNRS, IRIF, UMR 8243, Univ Paris Diderot, Sorbonne Paris Cite, F-75205 Paris, France

出　　处：《Frontiers of Computer Science》2019年第4期828-849,共22页中国计算机科学前沿（英文版）

摘　　要：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.

关 键 词：process CALCULUS non-interleaving SEMANTICS barbed CONGRUENCE BISIMULATION 

分 类 号：TP[自动化与计算机技术]