In: Fundamenta Informaticae, Vol. 11, pages 433-452. 1988.
Abstract: When using labelled transiton systems to model languages like CCS, one specifies transitons with their proofs instead of simple actions. Then the label of a transtions identifies uniquely that transition, and one may use this inforamtion to define a concurrency relation on (proved) transitons, and a notion of residual of a (proved) transiton by a concurrent one.