View Related Documents

Abstract

Concurrent systems are commonly verified after computing a state graph describing all possible behaviors. Unfortunately, this state graph is often too large to be effectively built. Partial-order techniques have been developed to avoid combinatorial explosion while preserving the properties of interest. This paper investigates the combination of two such approaches, persistent sets and covering steps, and proposes partial enumeration algorithms that cumulate their respective benefits.

Keywords  Concurrent systems - state space exploration - partial-order - persistent sets - covering steps graph - verification methods

Fulltext Preview

Image of the first page of the fulltext document