A Framework to Handle Linear Temporal Properties in (ω-)Regular Model Checking

Ahmed Bouajjani, Axel Legay, Pierre Wolper

Since the topic emerged several years ago, work on regular model checking has mostly been devoted to the verification of state reachability and safety properties. Though it was kno…