Regular transition systems (RTS) are a popular formalism for modeling infinite-state systems in general, and parameterised systems in particular. In a CONCUR 22 paper, Esparza et al. introduce a novel approach to the verification of RTS, based on inductive invariants. The approach computes the intersection of all inductive invariants of a given RTS that can be expressed as CNF formulas with a bounded number of clauses, and uses it to construct an automaton recognising an overapproximation of the reachable configurations. The paper shows that the problem of deciding if the language of this automaton intersects a given regular set of unsafe configurations is in $\textsf{EXPSPACE}$ and $\textsf{PSPACE}$-hard. We introduce $\textit{regular abstraction frameworks}$, a generalisation of the approach of Esparza et al., very similar to the regular abstractions of Hong and Lin. A framework consists of a regular language of $\textit{constraints}$, and a transducer, called the $\textit{interpretation}$, that assigns to each constraint the set of configurations of the RTS satisfying it. Examples of regular abstraction frameworks include the formulas of Esparza et al., octagons, bounded difference matrices, and views. We show that the generalisation of the decision problem above to regular abstraction frameworks remains in $\textsf{EXPSPACE}$, and prove a matching (highly non-trivial) $\textsf{EXPSPACE}$-hardness bound. $\textsf{EXPSPACE}$-hardness implies that, in the worst case, the automaton recognising the overapproximation of the reachable configurations has a double-exponential number of states. We introduce a learning algorithm that computes this automaton in a lazy manner, stopping whenever the current hypothesis is already strong enough to prove safety. We report on an implementation and show that our experimental results improve on those of Esparza et al.

翻译：摘要：正则迁移系统（RTS）是建模无限状态系统（特别是参数化系统）的流行形式化方法。在CONCUR 22会议论文中，Esparza等人提出了一种基于归纳不变量验证RTS的新方法。该方法计算给定RTS的所有可表示为子句数有界CNF公式的归纳不变量的交集，并利用该交集构造一个识别可达配置超近似的自动机。该论文表明，判定该自动机语言是否与给定正则不安全配置集相交的问题属于 $\textsf{EXPSPACE}$ 且是 $\textsf{PSPACE}$-难的。我们引入**正则抽象框架**，这是对Esparza等人方法的推广，与Hong和Lin的正则抽象非常相似。该框架由正则的**约束**语言和一个称为**解释**的转换器组成，该转换器将每个约束映射为RTS中满足该约束的配置集。正则抽象框架的示例包括Esparza等人的公式、八边形、有界差分矩阵和视图。我们证明，将上述判定问题推广到正则抽象框架仍属于 $\textsf{EXPSPACE}$，并给出了匹配的（高度非平凡）$\textsf{EXPSPACE}$-难度下界。$\textsf{EXPSPACE}$-难度意味着，在最坏情况下，识别可达配置超近似的自动机具有双指数数量的状态。我们引入了一种学习算法，该算法以惰性方式计算该自动机，并在当前假设足以证明安全性时停止。我们报告了实现结果，并表明我们的实验性能优于Esparza等人的结果。