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, G. Michele; Zunino, Roberto. - In: THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING. - ISSN 2352-2216. - ELETTRONICO. - 85:3(2016), pp. 399-424. [10.1016/j.jlamp.2015.05.001]

Contracts as games on event structures

Zunino, Roberto
2016

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.
3
Bartoletti, Massimo; Cimoli, Tiziana; Pinna, G. Michele; Zunino, Roberto
Contracts as games on event structures / Bartoletti, Massimo; Cimoli, Tiziana; Pinna, G. Michele; Zunino, Roberto. - In: THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING. - ISSN 2352-2216. - ELETTRONICO. - 85:3(2016), pp. 399-424. [10.1016/j.jlamp.2015.05.001]
File in questo prodotto:
File Dimensione Formato  
main.pdf

accesso aperto

Tipologia: Post-print referato (Refereed author’s manuscript)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 665.83 kB
Formato Adobe PDF
665.83 kB Adobe PDF Visualizza/Apri

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: http://hdl.handle.net/11572/143019
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 12
  • ???jsp.display-item.citation.isi??? 8
social impact