Proved trees

An incremental parametric model is presented that permits to recover different descriptions of concurrent systems. Given a calculus, its semantics is defined through a privileged transition system with transitions labelled by their proofs; then computations, i.e., paths in the transition system, are given a tree structure (proved trees). Different representation of the behaviour of a process are obtained by observing, via an observation function, the proved tree associated to the process. As an example, the paper shows how the interleaving, causal, and locational semantics are recovered, and shows how the correspending bisimulations are compared, by a simple inspection of the used observation functions. Also, an algebra of proved trees is defined, and a generalized expansion law is exhibited. Through the appropriate observation function, this generalized law originates the analogous expansion law in the selected approach.