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
DEGANO, PIERPAOLO;
2015-01-01
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.