HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 1:45:32 PM
Last modification on : Friday, February 4, 2022 - 3:25:13 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:58:16 PM


  • 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⟩



Record views


Files downloads