A lightweight regular model checking approach for parameterized systems

In recent years, we have designed a lightweight approach to regular model checking specifically designed for parameterized systems with global conditions. Our approach combines the strength of regular languages, used for representing infinite sets of configurations, with symbolic model checking and approximations. In this paper, we give a uniform presentation of several variations of a symbolic backward reachability scheme in which different classes of regular expressions are used in place of BDDs. The classification of the proposed methods is based on the precision of the resulting approximated analysis.