Personal tools
You are here: Home Events Abstract Archives 2003 Configuration Theories: Concurrency in Sequent Form

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

Document Actions