Succinct Determinisation of Counting Automata via Sphere Construction (Technical Report)
Luk\'a\v{s} Hol\'ik, Ond\v{r}ej Leng\'al, Olli Saarikivi, Lenka, Turo\v{n}ov\'a, Margus Veanes, Tom\'a\v{s} Vojnar

TL;DR
This paper introduces an efficient algorithm for determinising counting automata that produces significantly smaller automata without unfolding counters, with practical benefits in pattern matching and network traffic analysis.
Contribution
The paper presents a novel, efficient determinisation algorithm for counting automata and a simplified version for monadic CAs, improving scalability and performance.
Findings
Produces smaller deterministic automata compared to naive methods
Reduces automata explosion in practical benchmarks
Faster and more scalable than existing approaches
Abstract
We propose an efficient algorithm for determinising counting automata (CAs), i.e., finite automata extended with bounded counters. The algorithm avoids unfolding counters into control states, unlike the na\"ive approach, and thus produces much smaller deterministic automata. We also develop a simplified and faster version of the general algorithm for the sub-class of so-called monadic CAs (MCAs), i.e., CAs with counting loops on character classes, which are common in practice. Our main motivation is (besides applications in verification and decision procedures of logics) the application of deterministic (M)CAs in pattern matching regular expressions with counting, which are very common in e.g. network traffic processing and log analysis. We have evaluated our algorithm against practical benchmarks from these application domains and concluded that compared to the na\"ive approach, our…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
Topicssemigroups and automata theory · Network Packet Processing and Optimization · Formal Methods in Verification
