A Complete Set of Satisfaction Rules for Property Detection in Distributed Computations

Michel Hurfin 1 Masaaki Mizuno 2
1 ADP - Distributed Algorithms and Protocols
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, INRIA Rennes
Abstract : This paper presents a general framework for specification and detection of properties in distributed computations. A property of states in distributed computation in progress is defined by predicates (called behavioral patterns) and satisfaction rules (called modal operators). A behavioral pattern is obtained by combining basic predicates that are defined over either local states or consistent global states of the computation. In both cases, we model a distributed computation by a directed acyclic graph in which vertices represent (local or global) states and edges represent causal relation over the states. Specification and verification of behavioral patterns are formulated as instances of the language recognition problem, and basic concepts used in formal language theory are applied. A basic predicate is assimilated to a symbol, and a behavioral pattern is specified as a language (i.e., a set of words) defined over an alphabet of symbols. Based on this model and given a behavioral pattern, we define four modal operators (i.e., four different satisfaction rules). Three of them are equivalent to modal operators previously introduced in related works. Finally, we present algorithms to verify each of the four modal operators over a class of behavioral patterns, called regular patterns.
Type de document :
[Research Report] RR-2908, INRIA. 1996
Liste complète des métadonnées

Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 13:45:32
Dernière modification le : mercredi 16 mai 2018 - 11:23:02
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:58:16



  • HAL Id : inria-00073788, version 1


Michel Hurfin, Masaaki Mizuno. A Complete Set of Satisfaction Rules for Property Detection in Distributed Computations. [Research Report] RR-2908, INRIA. 1996. 〈inria-00073788〉



Consultations de la notice


Téléchargements de fichiers