Computing Inductive Invariants of Regular Abstraction Frameworks

TL;DR

This work generalises the inductive-invariant verification approach for regular transition systems from Esparza et al. to arbitrary regular abstraction frameworks, defining AbstractSafety and proving its $EXPSPACE$-completeness via a complex reduction from exponentially bounded Turing machines. It shows that inductive constraints form a regular language and that potential reachability can be recognised by transducers, enabling an over-approximation of reachable configurations that preserves safety guarantees. The authors present a learning-based algorithm that lazily constructs a small yet sufficient set of inductive constraints by solving the separability problem (with SAT heuristics for the length-preserving case) and compare it experimentally against prior methods, achieving smaller automata and improved results on benchmarks. The results illuminate the trade-offs between expressiveness of the abstraction framework and computational hardness, and demonstrate a practical path to scalable verification of infinite-state systems through regular abstractions and automata learning.

Abstract

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.

Figures (6)

• Figure 1: Transducers for the interpretations of Example \ref{['ex:traps']} and \ref{['ex:tokenpassingandtraps']}. We have $\Gamma= 2^\Sigma$, and so the alphabet of the transducer is $(2^\Sigma)_\# \times \Sigma_\#$. The symbols $[{{\star} \atop {\#}}]$ and $[{{\#} \atop {\star}}]$ stand for the sets of all letters of the form $[{{\gamma} \atop {\#}}]$ and $[{{\#} \atop {\sigma}}]$, respectively .
• Figure 2: On the left, DFA recognising all non-trivial inductive constraints of Example \ref{['ex:tokenpassingflows']}. On the right, fragment with the same interpretation as the DFA on the left.
• Figure 3: A sample run of the regular transition system described in Example \ref{['ex:rtspspace']}. Here, $\mathit{mark}(x,y)$ means that the $y$-th bit of the prime number $x$ is changed to 1, and thus every position not equivalent to $y \pmod x$ is unmarked. Note that the first position of the TM part (the one with $\#$) is position 0. We write $x^y$ instead of $[{y \atop x}]$. We highlight bits and symbols that were written to in pink (bits which are unmarked by the mark transition, but were already unmarked, are drawn in darker pink).
• Figure 4: Constraints in Example \ref{['ex:rtspspace']}. (1) Two configurations $u,v$, where $u\in C_I$, $v\in C_U$. (2) The (not necessarily inductive) constraint $A_1$, separating $u,v$. (3) The matching inductive constraint $A_2$.
• Figure 5: Pseudo-code representation of the transducers for $\Delta_\mathit{mark}$ and $\Delta_\mathit{write}'$.

Theorems & Definitions (26)

• Definition 1
• Example 2: Token passing AbdullaJNS04
• Definition 3
• Remark 4
• Lemma 4
• Example 5
• Example 6
• Example 7
• Definition 8
• Example 9