More stubborn set methods for process algebras

Abstract

Six stubborn set methods for computing reduced labelled transition systems are presented. Two of them preserve the traces, and one is tailored for on-the-fly verification of safety properties. The rest preserve the tree failures, fair testing equivalence, or the divergence traces. Two methods are entirely new, the ideas of three are recent and the adaptation to the process-algebraic setting with non-deterministic actions is new, and one is recent but slightly generalized. Most of the methods address problems in earlier solutions to the so-called ignoring problem. The correctness of each method is proven, and efficient implementation is discussed.