Regular model checking is a technique for the verification of infinite-state systems whose configurations can be represented as finite words over a suitable alphabet. The form we are studying applies to systems whose set of initial configurations is regular, and whose transition relation is captured by a length-preserving transducer. To verify safety properties, regular model checking iteratively computes automata recognizing increasingly larger regular sets of reachable configurations, and checks if they contain unsafe configurations. Since this procedure often does not terminate, acceleration, abstraction, and widening techniques have been developed to compute a regular superset of the reachable configurations. In this paper, we develop a complementary procedure. Instead of approaching the set of reachable configurations from below, we start with the set of all configurations and approach it from above. We use that the set of reachable configurations is equal to the intersection of all inductive invariants of the system. Since this intersection is non-regular in general, we introduce b-invariants, defined as those representable by CNF-formulas with at most b clauses. We prove that, for every $b\geq0$, the intersection of all inductive b-invariants is regular, and we construct an automaton recognizing it. We show that whether this automaton accepts some unsafe configuration is in EXPSPACE for every $b\geq0$, and PSPACE-complete for b=1. Finally, we study how large must b be to prove safety properties of a number of benchmarks.

翻译：正则模型检验是一种用于验证无限状态系统的技术，其配置可表示为特定字母表上的有限字。本文研究的形式适用于初始配置集为正则且转移关系由长度保持转换器捕获的系统。为验证安全性属性，正则模型检验迭代地计算识别越来越大的可达配置正则集的自动机，并检查它们是否包含不安全配置。由于该过程通常不终止，现已发展出加速、抽象和拓宽技术来计算可达配置的正则超集。本文提出一种互补方法：不从下方逼近可达配置集，而是从所有配置的集合出发，从上方进行逼近。我们利用可达配置集等于系统所有归纳不变量的交集这一性质。由于该交集通常非正则，我们引入b-不变量——定义为最多由b个子句的CNF公式可表示的集合。我们证明对于任意$b\geq0$，所有归纳b-不变量的交集是正则的，并构建识别该集合的自动机。我们证明对于任意$b\geq0$，判断该自动机是否接受某些不安全配置属于EXPSPACE问题，而当b=1时为PSPACE完全问题。最后，我们通过多个基准测试研究了证明安全性属性所需的最小b值。