An Algebraic Structure for the Action-Based Contract Language CL - theoretical results †
Christian Prisacariu, Gerardo Schneider · NORA - Norwegian Open Research Archives · 2007
We introduce in this paper an algebra of actions specially tailored to serve as basis of an action-based formalism for writing electronic contracts.The proposed algebra is based on the work on Kleene algebras but does not consider the Kleene star and introduces a new constructor for modelling concurrent actions.The algebraic structure is resource-aware and incorporates special actions called tests.In order to be in accordance with the intuition behind electronic contracts we consider new properties of the algebraic structure, in particular a conict relation and a demanding partial order.We also study a canonical form of the actions which, among other things, helps to naturally dene a notion of action negation.Our action negation is more general than just negation of atomic actions, but more restricted than the negation involving the universal relation.A standard interpretation of the algebra is given in terms of guarded rooted trees with specially dened operations on them.The algebra is proven to be complete over the standard interpretation.