Exchanging resources often involves situations where a participant gives a resource without obtaining immediately the expected reward. For instance, one can buy an item without paying it in advance, but contracting a debt which must be eventually honoured. Resources, credits and debits can be represented, either implicitly or explicitly, in several formal models, among which Petri nets and linear logic. In this paper we study the relations between two of these models, namely intuitionistic linear logic with mix and Debit Petri nets. In particular, we establish a natural correspondence between provability in the logic, and marking reachability in nets.

Debits and Credits in Petri Nets and Linear Logic

BARTOLETTI, MASSIMO;DI GIAMBERARDINO, PAOLO;
2015

Abstract

Exchanging resources often involves situations where a participant gives a resource without obtaining immediately the expected reward. For instance, one can buy an item without paying it in advance, but contracting a debt which must be eventually honoured. Resources, credits and debits can be represented, either implicitly or explicitly, in several formal models, among which Petri nets and linear logic. In this paper we study the relations between two of these models, namely intuitionistic linear logic with mix and Debit Petri nets. In particular, we establish a natural correspondence between provability in the logic, and marking reachability in nets.
File in questo prodotto:
File Dimensione Formato  
illmix-dpn.pdf

embargo fino al 27/08/2016

Descrizione: Articolo principale
Tipologia: versione post-print
Dimensione 434.65 kB
Formato Adobe PDF
434.65 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: https://hdl.handle.net/11584/114096
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact