On Combining the Persistent Sets Method with the Covering Steps Graph Method

摘要

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.