Lending Petri nets and contracts
Logic in Computer Science
2020-04-17 v2 Multiagent Systems
Software Engineering
Abstract
Choreography-based approaches to service composition typically assume that, after a set of services has been found which correctly play the roles prescribed by the choreography, each service respects his role. Honest services are not protected against adversaries. We propose a model for contracts based on a extension of Petri nets, which allows services to protect themselves while still realizing the choreography. We relate this model 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.
Keywords
Cite
@article{arxiv.1211.3624,
title = {Lending Petri nets and contracts},
author = {Massimo Bartoletti and Tiziana Cimoli and G. Michele Pinna},
journal= {arXiv preprint arXiv:1211.3624},
year = {2020}
}