On (Omega-)Regular Model Checking

Axel Legay, Pierre Wolper

Checking infinite-state systems is frequently done by encoding infinite sets of states as regular languages. Computing such a regular representation of, say, the set of reachable s…