A fully abstract semantics for value-passing CCS for trees |
| |
Authors: | Ying JIANG Shichao LIU Thomas EHRHARD |
| |
Affiliation: | 1. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China2. University of Chinese Academy of Sciences, Beijing 100049, China3. CNRS, IRIF, UMR 8243, Univ Paris Diderot, Sorbonne Paris Cité F-75205 Paris, France |
| |
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 |
|
| 点击此处可从《Frontiers of Computer Science》浏览原始摘要信息 |
|
点击此处可从《Frontiers of Computer Science》下载全文 |
|