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.

Contracts as games on event structures

BARTOLETTI, MASSIMO;CIMOLI, TIZIANA;PINNA, GIOVANNI MICHELE;
2016-01-01

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.
2016
Event structures; Games; Contract calculus
File in questo prodotto:
File Dimensione Formato  
contracts-as-games.pdf

Solo gestori archivio

Descrizione: Articolo principale
Tipologia: versione pre-print
Dimensione 665.92 kB
Formato Adobe PDF
665.92 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11584/110837
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 12
  • ???jsp.display-item.citation.isi??? 8
social impact