CCS for Trees

TL;DR

This paper extends the concept of CCS to top-down tree automata by introducing a graph-parameterized parallel composition, enabling controlled interaction and establishing equivalence notions with formal proofs.

Contribution

It proposes a novel extension of CCS for top-down tree automata with a graph-based parallel composition and formal equivalence relations, advancing automata theory.

Findings

Defined a new parallel composition for tree automata

Established observational and bisimilarity equivalences

Proved an adequacy theorem linking the equivalences

Abstract

CCS can be considered as a most natural extension of finite state automata in which interaction is made possible thanks to parallel composition. We propose here a similar extension for top-down tree automata. We introduce a parallel composition which is parameterized by a graph at the vertices of which subprocesses are located. Communication is allowed only between subprocesses related by an edge in this graph. We define an observational equivalence based on barbs as well as weak bisimilarity equivalence and prove an adequacy theorem relating these two notions.