Affiliations: Faculty of Engineering Science, University Austral de
Chile, General Lagos 2086, Valdivia, Chile. E-mail: amadalin@uach.cl | IRISA/INRIA Rennes, Campus de Beaulieu, 35042 Rennes
CEDEX, France. E-mail: fabre@irisa.fr
Abstract: This paper considers distributed systems, defined as a collection of
components interacting through interfaces. Components, interfaces and
distributed systems are modeled as Petri nets. It is well known that the
unfolding of such a distributed system factorises, in the sense that it can be
expressed as the composition of unfoldings of its components. This factorised
form of the unfolding generally provides a more compact representation of the
system runs, because each component does not need to represent the possible
choices (conflicts) appearing in the other components. Moreover, the unfolding
factorisation makes it possible to analyse the system by parts. The paper focuses on the derivation of a finite and complete prefix (FCP) in the
unfolding of a distributed system. Specifically, one would like to directly
obtain such a FCP in factorised form, without computing first a FCP of the
global distributed system and then factorising it. The construction of such a
"modular FCP" is based on deriving summaries of
component behaviours w.r.t. their interfaces, that are then communicated to the
neighbouring components. The latter combine these summaries with their local
behaviours, and prepare interface summaries for the next components. This
globally takes the form of a message passing algorithm, where the global system
is never considered.
Keywords: Petri net, unfolding, finite complete prefix, distributed system, modular computation, pullback, category theory
