Contracts as games on event structures

Post date: 07-May-2015 08:35:53

Upcoming paper (to appear in Journal of Logical and Algebraic Methods in Programming)

Contracts as games on event structures

M. Bartoletti, T. Cimoli, G. M. Pinna, and R. Zunino

Abstract. Event structures are one of the classical models of concurrent systems. The idea is that an enabling X |- e represents the fact that the event e can only occur after all the events in the set X have already occurred. By interpreting events as actions promised by some participants, and by associating each participant with a goal (a function on sequences of events), we use event structures as a formal model for contracts. The states of a contract are sequences of events; a participant has a contractual obligation (in a given state) whenever some of its events is enabled in such a state. To represent the fact that participants are mutually distrusting, we study concurrent games on event structures; there, participants may play by firing events in order to reach their goals, and eventually win, lose or tie.

A crucial notion arising in this setting is that of agreement: a participant agrees on a set of contracts if she has a strategy to reach her goals in all the plays conforming to her strategy (or to make another participant sanctionable for not honouring an obligation). Another relevant notion is protection: a participant is protected by her contract when she has a strategy to avoid losing in any contexts, even in those where she has not reached an agreement. We study conditions for obtaining agreement and protection, and we show that these properties mutually exclude each other in a certain class of contracts. We then relate the notion of agreement in contracts with that of compliance in session types. In particular, we show that compliance corresponds to the fact that eager strategies lead to agreement.