Hasse Diagram Generators and Petri Nets

Issue title: Applications and Theory of Petri Nets and Other Models of Concurrency, 2009

Article type: Research Article

Authors: de Oliveira Oliveira, Mateus

Affiliations: School of Computer Science, Tel Aviv University, Tel Aviv, Israel. mateusde@tau.ac.il

Note: [] Address for correspondence: Blavatnik School of Computer Science, Tel-Aviv University, Ramat Aviv, Tel-Aviv 69978, Israel

Abstract: In [18] Lorenz and Juhás raised the question of whether there exists a suitable formalism for the representation of infinite families of partial orders generated by Petri nets. Restricting ourselves to bounded p/t-nets, we propose Hasse diagram generators as an answer. We show that Hasse diagram generators are expressive enough to represent the partial order language of any bounded p/t net. We prove as well that it is decidable both whether the (possibly infinite) family of partial orders represented by a given Hasse diagram generator is included in the partial order language of a given p/t-net and whether their intersection is empty. Based on this decidability result, we prove that the partial order languages of two given Petri nets can be effectively compared with respect to inclusion. Finally we address the synthesis of k-safe p/t-nets from Hasse diagram generators.

Keywords: Causality, partial order theory of concurrency

DOI: 10.3233/FI-2010-367

Journal: Fundamenta Informaticae, vol. 105, no. 3, pp. 263-289, 2010