The link-calculus is a model for concurrency that extends the point-to-point communication discipline of Milner's CCS with multiparty interactions. Links are used to build chains describing how information flows among the different agents participating in a multiparty interaction. The inherent non-determinism in deciding both, the number of participants in an interaction and how they synchronize, makes it difficult to devise efficient verification techniques for this language. In this paper we propose a symbolic semantics and a symbolic bisimulation for the link-calculus which are more amenable to automating reasoning. Unlike the operational semantics of the link-calculus, the symbolic semantics is finitely branching and it represents, compactly, a possibly infinite number of transitions. We give necessary and sufficient conditions to efficiently check the validity of symbolic configurations. We also implement an interpreter based on this semantics and we show how to use such implementation for verification.
展开▼
