Synthesis and Verification of Register Automata over Data Sequences (Technical Report)
Authors: Chih-Duo Hong, Hongjian Jiang, Anthony W. Lin, Oliver Markgraf, Julian Parsert, Tony Tan
Organizations: National Chengchi University, Taipei, Taiwan · University of Kaiserslautern-Landau, Kaiserslautern, Germany · MPI-SWS, Kaiserslautern, Germany · University of Liverpool, Liverpool, United Kingdom
Data sequences, such as time series, traces, and sensor streams, are words over large or infinite data domains. Their properties often depend on comparisons between values at different positions, which finite automata cannot express directly. We study synthesis and verification for Deterministic Register Automata (DRAs) over ordered data sequences. DRAs combine finite control with registers for remembered data values, providing compact symbolic descriptions of quantitative sequence languages. Our technical core is a local-search synthesis procedure and an exact robustness checker for DRAs. We fix the alphabet theory to ordered rationals (\Q;<,=) with rational guard constants and use non-negative affine accumulator costs. For a fixed number of DRA registers, the checker runs in polynomial time; its dependence on that number is exponential. It reduces robustness to coverability and then to a shortest-path problem. Since the search ranges over \Q+, it produces variable-length witnesses and, for RAA-definable alignment costs such as DTW, explores a counterexample space with no a priori length bound. As an application, we use learned DRAs as interpretable surrogates for queried neural sequence classifiers. A probably approximately correct (PAC) validation loop refines rejected candidates, returns genuine non-robustness witnesses for the classifier when found, and accepts a surrogate only with statistical guarantees for fidelity and local stability. We implement the framework in \textscRAExc, enabling the synthesis of interpretable automata and the verification of their robustness. We evaluate the approach on benchmark languages and sequentialized MNIST, demonstrating high accuracy while verifying the robustness of the learned automata.
Figures & tables
Figure 1: Two S&P 500 price sequences. Red and blue triangles mark lows and highs, respectively. The left uptrend is robust to small last value decreases, while the right uptrend is fragile.
Figure 2: A deterministic register automaton A that identifies the higher-highs-higher-lows price pattern.
NLSTMNT
LLS
Language
Description
Acc
Acc
Acc
Time
S R T
L1
a∗
100.00
100.00
100.00
1.00
2 1 2
L2
(ab)∗
100.00
100.00
99.95
20.08
4 1 8
L3
anbm with odd n and even m
100.00
100.00
100.00
0.53
4 1 4
L4
No symbol repeats three times consecutively
97.90
99.30
99.45
27.90
4 2 8
L5
a(a∣b)∗ with even counta,countb
100.00
100.00
79.00
753.26
4 1 7
Table 1: Benchmarks and RQ1 results. Li : Tomita languages; Si : trend patterns over rational sequences, incl. the higher-highs/higher-lows family of Example 1 ( S9 – S11 ). Acc : balanced test accuracy (%); Time : synthesis time (s); S/R/T : states/registers/transitions.
Metric
+/−/?
Multi
Max
Spur.
Cost
∣w∣=∣v∣
Last letter
21/14/3
8
5
358
0.0625
0
Edit
0/36/2
6
6
362
1
5
Hamming
2/35/1
5
5
50
1
0
Manhattan
15/19/4
11
9
835
0.011–0.106
0
DTW
0/38/0
6
5
232
0–0.083
36
Table 2: Validation loop per metric (38 configurations each). Multi / Max : concluded runs with several rounds / most rounds; Spur. : spurious witnesses in concluded runs; Cost : confirmed witness costs; ∣w∣=∣v∣ : witnesses changing the length.
Figure 3: Learning time and checking time per sequence under last-letter distance.
Appendix figures & tables2 assets
Supplementary material from the paper’s appendix.
Appendix
LLS
SMT-based
RALib (active)
Lang
Acc
Time
S/R
Acc
Time
S/R
Acc
Time
S/R
L1
100.00
1.0
2/1
99.80
23.7
2/1
100.00
4.7
3/1
L2
99.95
20.1
4/1
98.40
78.5
4/1
100.00
5.2
5/2
L3
100.00
0.5
4/1
99.75
55.1
4/1
100.00
6.5
6/2
L4
99.45
27.9
4/2
99.85
507.2
4/2
100.00
3.5
4/1
L5
79.00
753.3
4/1
100.00
82.3
4/1
100.00
4.0
4/2
Appendix
Table 3: Learner comparison. Acc : balanced test accuracy (%); Time : learning time (s); S/R : states/registers.
Table 4: RQ2 outcomes per metric. Every configuration not listed is non-robust, with a witness confirmed on the network. (L)/(T): for NLSTM or NT only; otherwise for both.
Register automata are finite automata equipped with memory that recognize data languages over infinite alphabets. In this work, we investigate active learning algorithms for deterministic register automata (DRAs) over ordered data domains--covering both dense domains, such as the rationals, and non-dense domains such as the integers. We show that the active learning problem for DRAs over both dense and non-dense ordered domains can be treated within a single unified framework. More specifically, we develop and implement a polynomial-time active learning procedure for DRAs over ordered domains, using oracles for membership, equivalence and memorability queries. The memorability queries were originally introduced for learning DRAs over domains with identity tests. Our unified framework also leads to a new consequence: minimization of DRAs over the non-dense ordered domain of integers is decidable, extending a result previously known only for dense domains. Finally, we give improved complexity bounds of several decision problems for DRAs over ordered domains that are closely related to the queries used in active learning.
Yong Li, Qiyi Tang, Di-De Yen
Key Laboratory of System Software (Chinese Academy of Sciences), Beijing, China · Institute of Software, Chinese Academy of Sciences, Beijing, China · School of Computer Science and Informatics, University of Liverpool, UK
Test-set accuracy is silent on two issues that matter when deploying autoregressive neural sequence models: how much probability mass the system under test (SUT) places on constraint-violating alternatives that are reachable under sampling and what fraction of the input population satisfies a domain requirement. We answer both with probabilistic model checking. The pipeline extracts a discrete-time Markov chain (DTMC) from the SUT's token-by-token generation, verifies formal PCTL specifications with the PRISM model checker, and aggregates the per-input verdicts into a coverage curve over the input space. A soundness theorem establishes the DTMC as an under-approximation, so every verdict yields a certified interval on the SUT's true reachability probability. The coverage built from those verdicts is, therefore, conservative by construction. A counterexample-guided abstraction refinement (CEGAR) loop adaptively tightens the interval, and a maximum-likelihood algorithm extracts the most probable falsifying trace. Two case studies exercise the pipeline. On a GPT-2 computer-aided process-planning (CAPP) model with 100% test accuracy, the pipeline quantifies the probability mass greedy decoding hides, but that is reachable with sampling; and identifies the smallest training fraction at which an ordering requirement holds population-wide, neither of which test accuracy can report. We then verify the SMILES molecular generator with a 50x larger vocabulary. The only change is an external chemical-validity oracle, and the pipeline identifies the gap between structural completeness and chemical validity.
We present a formal and constructive framework for simulating Alternating Finite Automata (AFAs) using Logic-Gated Time-Shared Feedforward Networks (LG-TS-FFNs). Unlike prior neural automata models limited to Nondeterministic Finite Automata (NFAs) and existential reachability, our architecture integrates learnable, state-dependent biases that function as differentiable logic gates, enabling the representation of both Existential OR and Universal AND aggregation within a shared-parameter linear recurrence. We prove that this architectural modification upgrades the network's computational class to be structurally isomorphic to AFAs, thereby inheriting their exponential succinctness: the network can represent regular languages requiring 2n states in an NFA with only n neurons. We rigorously establish that the forward pass of an LG-TS-FFN exactly simulates the reachability dynamics of an AFA, including instantaneous ε-closures. Furthermore, we demonstrate empirical learnability: a continuous relaxation of the logic gates allows the network to simultaneously recover the automaton's topology and logical semantics from binary labels via standard gradient descent. Extensive experiments confirm that our model achieves perfect recovery of ground-truth automata, bridging the gap between statistical learning and succinct, universal logical reasoning.