Model Checking Contractual Protocols

TL;DR

This paper explores using model checking with Petri Nets to verify contractual protocols, focusing on dynamic agreements and their evolution over time, especially useful in negotiations and drafting.

Contribution

It introduces a novel approach applying Petri Nets for contract verification, integrating model checking into legal contract analysis and pre-contractual processes.

Findings

Demonstrates the verification process through an illustrative example

Shows potential for improving contract drafting and negotiation

Highlights the applicability of Petri Nets in legal contract modeling

Abstract

This paper discusses how model checking, a technique used for the verification of behavioural requirements of dynamic systems, can be usefully deployed for the verification of contracts. A process view of agreements between parties is taken, whereby a contract is modelled as it evolves over time in terms of actions or more generally events that effect changes in its state. Modelling is done with Petri Nets in the spirit of other research work on the representation of trade procedures. The paper illustrates all the phases of the verification technique through an example and argues that the approach is useful particularly in the context of pre-contractual negotiation and contract drafting. The work reported here is part of a broader project on the development of logic-based tools for the analysis and representation of legal contracts.