Department of
Computer Science
University of Rome "La Sapienza"
2pm 19 September 2003
Room 2511, JCMB, King's Buildings
Configuration theories (Cenciarelli 2002) describe concurrent systems axiomatically. Rules for composing configurations (of events) are represented by sequents \Gamma\vdash_\rho\Delta, where \Gamma and \Delta are sequences of partially ordered sets (of events) and \rho is a matrix of monotone maps from the components of \Gamma to the components of \Delta. The structural rules of Gentzen's sequent calculus are decorated by suitable operations on matrices, where cut corresponds to product. The calculus is interpreted in configuration structures. A notion of logical equivalence arises: two structures are equivalent when they satisfy the same sequents. Such equivalence is intermediate between (pomset) trace equivalence and (history preserving) bisimulation at first order while it is stronger than bisimulation (equates less) at higher order, where configuration theories become "resource sensitive".