Extending contract automata with reparation and hypothetical clauses

Abstract

Contracts specify the ideal interaction between two parties. This is done through specifying what the parties obligations and permissions, i.e. deontic norms. However, actual behaviour does not always match up to the ideal since parties may violate norms. Contracts deal with these situations by specifying norms that the parties can do to return in good standing, i.e. reparations. Contract automata are a formal approach that allow the specification of contracts. They however lack the notion of reparations. This formalism brings a new aspect to contract specification by employing synchronous composition to model the interaction between parties. We use a case study involving a contract between an airline and passenger to present three extensions that add different notions of reparations to contract automata. Our first extension takes a high-level approach, were if when doing some actions there is a violation reparation norms come into action. We extend this concept to allow the specification of reparations depending on the norms violated and those satisfied. These two approaches however neglect the possibility of a whole process being performed in reparation, but our third notion employs hierarchical automata to do this. We also introduce a method to model hypothetical clauses and conditional clauses. Hypothetical clauses are reparations, but they depend on the violation of hypothetical norms, i.e. norms that do not hold in the contract. This allows a contract to specify norms in the case that another contract is active and violated. Similarly, conditional clauses activate new norms depending if some others holds. Our work adds considerably to the expressiveness of contract automata, putting it on par with other approaches using deontic logic for contract specification.