multiparty interaction

Seminary: Symbolic semantics for multiparty interactions in the link-calculus

July 19, 2017, 11.00 a.m., Aula Rossa, Polcoming Department, viale Mancini,5 (Sassari)
Tuesday, 18 July 2017

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 talk, we will introduce 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.

For further information