Lending Petri nets

• We study Lending Petri nets (LPNs), where places can have a negative number of tokens.
• We interpret LPNs as competitive multi-player concurrent games.
• We equip LPNs with associative composition operations.
• We study compositional verification and refinement of games over LPNs.
• We use LPNs to give a model to a fragment of Propositional Contract Logic.

We study Lending Petri nets, an extension of Petri nets where places may carry a negative number of tokens. This allows for modeling contracts where a participant may promise to give some of her resources under the guarantee that some other resources will eventually be obtained in exchange. We then propose an interpretation of the Horn fragment of Propositional Contract Logic in Lending Petri nets. In particular, we show that provability in the logic corresponds to reachability of certain markings in nets, and that proof traces correspond to “honored” firing sequences in nets.