Factorization of Unfoldings for Distributed Tile Systems Part 1 : Reduced Interaction Case - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2003

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

Eric Fabre

Résumé

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.
Fichier principal
Vignette du fichier
RR-4829.pdf (411.58 Ko) Télécharger le fichier

Dates et versions

inria-00071757 , version 1 (23-05-2006)

Identifiants

  • HAL Id : inria-00071757 , version 1

Citer

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

Partager

Gmail Facebook X LinkedIn More