Distributed Unfolding of Petri Nets
Paolo Baldan(1) - Stefan Haar(2) - Barbara König(3)
(1) Dipartimento di Informatica, Università
Ca' Foscari di Venezia, Italy
(2) INRIA Rennes, Distribcom team, France
(3) Institut für Formale Methoden
der Informatik, Technische Universität
Stuttgart, Germany
Abstract:
Some recent Petri net-based approaches to fault diagnosis of
distributed systems suggest to factor the problem into local
diagnoses based on the unfoldings of local views of the system,
which are then correlated with diagnoses from neighbouring
supervisors.
In this paper we propose a notion of system factorisation expressed
in terms of pullback decomposition.
To ensure coherence of the local views and completeness of the
diagnosis, data exchange among the unfolders needs to be specified
with care. We introduce interleaving structures as a format for
data exchange between unfolders and we propose a distributed
algorithm for computing local views of the unfolding for each system
component.
The theory of interleaving structures is developed to prove
correctness of the distributed unfolding algorithm.