Publication Details
Succinct Determinisation of Counting Automata via Sphere Construction (Technical Report)
Holíková Lenka, Ing., Ph.D. (RG VERIFIT)
Lengál Ondřej, Ing., Ph.D. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
SAARIKIVI, O.
Veanes Margus
counting automata, determinisation, regular expressions with bounded repetition
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 naive 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 naive approach, our algorithm is much less prone to explode, produces
automata that can be several orders of magnitude smaller, and is overall faster.
@techreport{BUT185112,
author="HOLÍK, L. and HOLÍKOVÁ, L. and LENGÁL, O. and VOJNAR, T. and SAARIKIVI, O. and VEANES, M.",
title="Succinct Determinisation of Counting Automata via Sphere Construction (Technical Report)",
year="2019",
publisher="Cornell University Library",
address="Ithaca",
pages="1--19",
doi="10.48550/arXiv.1910.01996",
url="http://arxiv.org/abs/1910.01996"
}