Configuration Structures and Logical Equivalence

Abstract. Configuration theories [Cen02] describe concurrent systems axiomatically. Rules for composing configurations (of events) are repre-sented by sequents Γ `ρ ∆, where Γ and ∆ are sequences of posets (of events) and ρ is a matrix of monotone maps from the components of Γ to the components of ∆. The structural rules of Gentzen’s sequent cal-culus are decorated by suitable operations on matrices, where cut corre-sponds to product. The calculus is interpreted in a rather general class of configuration structures called monotone. Two such structures are called logically equivalent if they satisfy the same sequents. This notion of equiv-alence is shown to be intermediate between (pomset) trace equivalence and (history preserving) bisimulation. A new form of sequent, more ex-pressive than in [Cen02], is also proposed and some of the classical closure properties adopted in literature for configuration structures are thereof axiomatised. In this more expressive setting the notion of logical equiv-alence becomes “resource sensitive, ” and it is shown to correspond to isomorphism when models are restricted to tree-like structures.