Seminar: Lending Petri Nets (and contracts)
Post date: 15-Apr-2013 15:43:22
Lending Petri Nets (and contracts)
April 16, 15.00 (Aula F)
April 17, 11.00 (Lab. 5)
Palazzo delle Scienze - Cagliari
G. Michele Pinna
Dipartimento di Matematica e Informatica - Università degli Studi di Cagliari
Abstract. In the first part of this seminar, we give a brief introduction to Petri nets, one of the classical models of distributed systems. Petri nets have been applied in various areas, among which the description and analysis of business processes.
In the second part, we present Lending Petri nets, a variant of Petri nets which allows places to "lend" tokens under the guarantee that credits will be honoured - that is, lent tokens are eventually returned.
Lending Petri nets are then exploited to model contracts for business processes. In particular, we show how they can be used to formalise contracts which protect themselves while still realizing the desired choreography. We relate Lending Petri nets with Propositional Contract Logic, by showing a translation of formulae into our Petri nets which preserves the logical notion of agreement, and allows for compositional verification.