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 transitions for CCS to obtain a partial order semantics for this language.