Modular construction of finite and complete prefixes of Petri net unfoldings

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 provides a more compact representation of the system trajectories, and 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 prefix" is based on deriving summaries of component behaviours w.r.t. their interfaces, that are communicated to the neighbouring components. The latter integ...

• Type: Conference
• Year: 2008
• Where: ACSD
• Authors: Agnes Madalinski, Eric Fabre
• Keywords: ACSD 2008, Distributed System, Hardware, Petri Nets, Unfolding