
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · semigroups and automata theory · Logic, programming, and type systems
