PhD Program in Mathematics and Computer Science

At
a very abstract level, a contract can be seen as sets of events,
together with relations to specify the causal dependencies and the
conflicts between events. This seems to suggest event structures – one
of the fundamental causal models for concurrency – as a natural
candidate for representing contracts. For instance, one can interpret
the enabling b|-a of a stable event structure as the contract clause
“I will do a after you have done b”.

However,
event structures do not capture a crucial aspect of contracts, i.e. the
capability of reaching an agreement in the presence of circularity in
the declared promises. For instance, one would expect that the contract
where A promises a in change of b, and B promises b in change of a, has
an agreement. This contrasts with the fact that the event structure with enablings b|-a and a|-b has only
one configuration – the empty set. This is because a|-b actually models
the fact that b may only happen after a has been done, and b|-a as the
fact that a may happen after b – and so neither a nor b can happen. Of
course, A could simply declare to do a, without asking b to be performed
first – but this would not protect A from a misbehaving B.

To
reconcile causality with circularity, A could relax her contract, i.e.
she could do a in change of the promise of B to do b. In this case A can
safely do the first step, because either B does b, or he will be
culpable of a contract violation.

In
this talk we present an extension of event structures which allows for
this kind of reasoning. The contract a||-b (intuitively, “I will do a if
you promise to do b”) reaches an agreement with the dual contract
b||-a, while protecting the participant who offers it. We characterise
configurations of these event structures as provability of formulae in
the contract logic PCL, an extension of intuitionistic logic with a
“contractual implication” connective.

We
then focus on the problem of determining, in any state of the execution
of a contract, which events have to be done next. This problem is
trivial in classical event structures (one has to do the events whose
causes have already been done), while it becomes relevant in the
presence of circularity: indeed, before performing an event a (whose
causes have not already been done) one has to be sure that its causes
will be done, eventually in the future. Also in this case we devise a
logical characterisation via an encoding in the logic PCL.

References