Skip to Main content Skip to Navigation

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

Eric Fabre 1
1 SIGMA2 - Signal, models, algorithms
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, INRIA Rennes
Abstract : 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.
Document type :
Complete list of metadata
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 6:41:59 PM
Last modification on : Thursday, February 11, 2021 - 2:48:05 PM
Long-term archiving on: : Sunday, April 4, 2010 - 8:30:31 PM


  • HAL Id : inria-00071757, version 1


Eric Fabre. Factorization of Unfoldings for Distributed Tile Systems Part 1 : Reduced Interaction Case. [Research Report] RR-4829, INRIA. 2003. ⟨inria-00071757⟩



Record views


Files downloads