In this paper we present briefly our eforts towards model checking law contracts. Our approach uses the formal action-based specification language for contracts CL. The actions of the language are well studied and form a algebraic structure for actions found in contracts which are interpreted as guarded rooted trees. The algebra is proven complete with respect to the interpretation as guarded rooted trees. The purpose of the CL language in the model checking process is to restrict the specification of contracts such that to avoid many of the common mistakes and deontic paradoxes. CL is also used to write the properties that one wants to check on the contract. We use a translation of CL into mu-calculus in order to obtain the (extended) labeled transition system representing the model of the contract. This is given to the NuSMV tool as input. For now, NuSMV supports only LTL-like properties, so we cannot use our CL to specifiy the properties. The extension of NuSMV in this respect is left for future work. We have used this method on a real contract example between an Internet provider and a client.

In this paper we present briefly our eforts towards model checking law contracts. Our approach uses the formal action-based specification language for contracts CL. The actions of the language are well studied and form a algebraic structure for actions found in contracts which are interpreted as guarded rooted trees. The algebra is proven complete with respect to the interpretation as guarded rooted trees. The purpose of the CL language in the model checking process is to restrict the specification of contracts such that to avoid many of the common mistakes and deontic paradoxes. CL is also used to write the properties that one wants to check on the contract. We use a translation of CL into mu-calculus in order to obtain the (extended) labeled transition system representing the model of the contract. This is given to the NuSMV tool as input. For now, NuSMV supports only LTL-like properties, so we cannot use our CL to specifiy the properties. The extension of NuSMV in this respect is left for future work. We have used this method on a real contract example between an Internet provider and a client.

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 conflict relation and a demanding partial order. We also study a canonical form of the actions which, among other things, helps to naturally define 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 defined operations on them. The algebra is proven to be complete over the standard interpretation.

In this paper we propose a formal language for writing electronic contracts, based on the deontic notions of obligation, permission, and prohibition. We take an ought-to-do approach, where deontic operators are applied to actions instead of state-of-affairs. We propose an extension of the mu-calculus in order to capture the intuitive meaning of the deontic notions and to express concurrent actions. We provide a translation of the contract language into the logic, the semantics of which faithfully captures the meaning of obligation, permission and prohibition. We also show how our language captures most of the intuitive desirable properties of electronic contracts, as well as how it avoids most of the classical paradoxes of deontic logic. We finally show its applicability on a contract example.