State Space Reduction for Process Algebra Specifications

Hubert Garavel and Wendelin Serwe

Theoretical Computer Science, 351(2) 131-145, February 2006.

Earlier version, slides and discussion available here.

Abstract:

Data-flow analysis to identify ``dead'' variables and reset them to an ``undefined'' value is an effective technique for fighting state explosion in the enumerative verification of concurrent systems. Although this technique is well-adapted to imperative languages, it is not directly applicable to value-passing process algebras, in which variables cannot be reset explicitly due to the single-assignment constraints of the functional programming style. This paper addresses this problem by performing data-flow analysis on an intermediate model (Petri nets extended with state variables) into which process algebra specifications can be translated automatically. It also addresses important issues, such as avoiding the introduction of useless reset operations and handling shared read-only variables that children processes inherit from their parents.

24 pages

PDF

PostScript