Synthesis and Verification of Register Automata over Data Sequences (Technical Report)

2026-10-23 · ArXiv

arXiv:2511.19100v2 Announce Type: replace

Abstract: 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;

原文链接：https://arxiv.org/abs/2511.19100

查看更多资讯请见 AI 行业资讯。