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

TL;DR

This paper develops a framework for verifying linear temporal properties within regular model checking, providing detailed constructions and addressing cycle detection challenges in infinite computations.

Contribution

It introduces precise methods for checking linear temporal properties in regular model checking with finite and infinite words, and proposes solutions to cycle detection issues.

Findings

Exact constructions for linear temporal property verification

Partial solution for cycle detection in infinite computations

Enhanced framework for regular model checking

Abstract

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 known that linear temporal properties could also be checked within this framework, little has been done about working out the corresponding details. This paper addresses this issue in the context of regular model checking based on the encoding of states by finite or infinite words. It works out the exact constructions to be used in both cases, and proposes a partial solution to the problem resulting from the fact that infinite computations of unbounded configurations might never contain the same configuration twice, thus making cycle detection problematic.