In: Charles Rattray, Savitri Maharaj, Carron Shankland (Eds.): Lecture Notes in Computer Science, Vol. 3116: Algebraic Methodology and Software Technology: 10th International Conference, AMAST 2004, Stirling, Scotland, UK, July 12-16, 2004, pages 164-180. Springer-Verlag, 2004.
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.