Skip to main navigation Skip to search Skip to main content

Efficient symbolic detection of global properties in distributed systems

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

9 Scopus citations

Abstract

A new approach is presented for detecting whether a computation of an asynchronous distributed system satisfies PossΦ (read "possibly Φ"), meaning the system could have passed through a global state satisfying property Φ. Previous general-purpose algorithms for this problem explicitly enumerate the set of global states through which the system could have passed during the computation. The new approach is to represent this set symbolically, in particular, using ordered binary decision diagrams. We describe an implementation of this approach, suitable for off-line detection of properties, and compare its performance to the enumeration-based algorithm of Alagar & Venkatesan. In typical cases, the new algorithm is significantly faster. We have measured over 400-fold speedup in some cases.

Original languageEnglish
Title of host publicationComputer Aided Verification - 10th International Conference, CAV'98, Proceedings
PublisherSpringer Verlag
Pages357-368
Number of pages12
ISBN (Print)3540646086, 9783540646082
DOIs
StatePublished - 1998
Event10th International Conference on Computer-Aided Verification, CAV'98 - Vancouver, BC, Canada
Duration: Jun 28 1998Jul 2 1998

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1427 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference10th International Conference on Computer-Aided Verification, CAV'98
Country/TerritoryCanada
CityVancouver, BC
Period06/28/9807/2/98

Fingerprint

Dive into the research topics of 'Efficient symbolic detection of global properties in distributed systems'. Together they form a unique fingerprint.

Cite this