# Configuration Theories: Concurrency in Sequent Form

Pietro Cenciarelli 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".