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$值。