Debits and credits in Petri nets and linear logic

Post date: 25-May-2015 20:55:04

Upcoming paper (to appear in LRC 2015)

Debits and credits in Petri nets and linear logic

M. Bartoletti, P. Degano, P. Di Giamberardino, and R. Zunino

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.