Non-deterministic contract automata

Abstract

Contracts provide a legal binding between two or more parties and used when they are engaging in operations in order to obtain some common agreement. The specification of deontic norms such as obligations and permissions allow for this interaction between communicating parties. At a specific point in a contract, a party may be given a number of options which it should do and this is when choices in contracts arise. Despite the existence of several logics used to represent contracts we focus our attention on contract automata, which are a formalism used to represent and reason about contracts. They provide an action-based view of contracts between parties with deontic clauses tagged in each state and allow for the representation of a very important feature, that of interaction between participating parties. However, they lack expressivity when it comes to the notion of choice — there currently exists no explicit way of knowing which party is deciding to make a choice in a contract. We provide two extensions to the definitions of contract automata in order to handle choices in contracts. Our first extension consists of mapping every action set to the participating party deciding to make the choice whilst the second extension consists of distinguishing between deterministic (where no choice is available) and choice transitions, represented using forking actions. Both extensions, despite having some differences, provide similar expressivity when representing choices explicitly, removing any element of ambiguity. By proving about several propositions we check the sanity of our formalisms and by also providing a use case between a student and the university, based on the assessment regulations of the University of Malta, we demonstrate the effectiveness of our extensions and the way they are implemented. Our work adds to the expressivity of contract automata by being able to handle external choices, explicitly stating which party is making the choice. This adds a new dimension to contract representation when using contract automata and provides a basis for future research.