A Non-Interleaving Semantics for CCS Based on Proved Transitions

Article type: Research Article

Authors: Boudol, Gérard | Castellani, Ilaria

Affiliations: INRIA Sophia-Antipolis, 06560 Valbonne, France

Abstract: When using labelled transition systems to model languages like CCS or TCSP, one specifies transitions by a set of structural rules. We consider labelling transitions with their proofs – in the given system of rules – instead of simple actions. Then the label of a transition identifies uniquely that transition, and one may use this information to define a concurrency relation on (proved) transitions, and a notion of residual of a (proved) transition by a concurrent one. We apply Berry and Lévy’s notion of equivalence by permutations to sequences of proved transitions for CCS to obtain a partial order semantics for this language.

DOI: 10.3233/FI-1988-11406

Journal: Fundamenta Informaticae, vol. 11, no. 4, pp. 433-452, 1988