Regular model checking is a well-established technique for the verification of infinite-state systems whose configurations can be represented as finite words over a suitable alphabet. It 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 set of reachable configurations. In this paper we develop a complementary approach. Instead of approaching the set of reachable configurations from below, we start with the set of all configurations and compute increasingly smaller regular supersets of it. We use that the set of reachable configurations is equal to the intersection of all inductive invariants of the system. Since the intersection is in general non-regular, we introduce $b$-bounded invariants, defined as those representable by CNF-formulas with at most $b$ clauses. We prove that, for every $b \geq 0$, the intersection of all $b$-bounded inductive invariants is regular, and show how to construct an automaton recognizing it. We study the complexity of deciding if this automaton accepts some unsafe configuration. We show that the problem is in \textsc{EXPSPACE} for every $b \geq 0$, and \textsc{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 \geq 0$，所有$b$有界归纳不变量的交集是正则的，并展示如何构造识别该集合的自动机。我们研究了判定该自动机是否接受某些不安全配置的复杂度。结果表明对于任意$b \geq 0$该问题属于\textsc{EXPSPACE}，而当$b=1$时为\textsc{PSPACE}完全问题。最后，我们通过多个基准案例研究了证明安全性性质所需的最小$b$值。