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 (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}$-难的。我们引入了$\textit{正则抽象框架}$，这是对Esparza等人方法的推广，与Hong和Lin的正则抽象非常相似。一个框架包含一个$\textit{约束}$的正则语言以及一个称为$\textit{解释}$的转换器，该转换器为每个约束分配满足该约束的RTS配置集合。正则抽象框架的示例包括Esparza等人的公式、八边形、有界差分矩阵以及视图。我们证明了上述决策问题推广到正则抽象框架后仍然属于$\textsf{EXPSPACE}$，并证明了一个匹配的（非平凡的）$\textsf{EXPSPACE}$-难下界。$\textsf{EXPSPACE}$-难性意味着，在最坏情况下，识别可达配置超近似的自动机具有双指数数量的状态。我们引入了一种学习算法，以惰性方式计算该自动机，一旦当前假设已足够强以证明安全性即停止计算。我们报告了一个实现，并展示了我们的实验结果优于Esparza等人的结果。