Factorization of Unfoldings for Distributed Tile Systems Part 1 : Reduced Interaction Case

We consider products of transition systems, that we representas tile systems. Tile systems can be viewed as Petri nets¸: places are replaced by (state) variables, and transitions change the value of part of these variables. A tile system is said to be distributed when it is formed of several components interacting through shared variables. We provide runs of these systems with true concurrency semantics. The unfolding technique, a convenient tool to represent runs with concurrent events, has been shown to apply to such models by Esparza and Römer. In this paper, we propose an even more compact representation of the system behavior. Specifically, we show that the unfolding of the global system can be expressed as a product of local branching processes, one per component. We also describe a modular procedure to build these local branching processes, based on exchanges of information between interacting components, which avoids any use of global information such as the global unfolding. We believe this result could open a new way to modular model checking techniques, in the spirit of previous work of the authors about modular diagnosis algorithms