An event-based model for contracts

TL;DR

This paper presents a novel event-based model for contracts that captures circular dependencies and obligations, establishing a logical correspondence and improving culpability analysis over previous models.

Contribution

It introduces an extended event structure model for contracts with a new relation for circular dependencies, linking it to a fragment of contract logic PCL, and refining culpability assessment.

Findings

Model accurately captures circular dependencies.

Establishes correspondence with a fragment of PCL.

Enhances culpability analysis with event ordering.

Abstract

We introduce a basic model for contracts. Our model extends event structures with a new relation, which faithfully captures the circular dependencies among contract clauses. We establish whether an agreement exists which respects all the contracts at hand (i.e. all the dependencies can be resolved), and we detect the obligations of each participant. The main technical contribution is a correspondence between our model and a fragment of the contract logic PCL. More precisely, we show that the reachable events are exactly those which correspond to provable atoms in the logic. Despite of this strong correspondence, our model improves previous work on PCL by exhibiting a finer-grained notion of culpability, which takes into account the legitimate orderings of events.