Succinct Determinisation of Counting Automata via Sphere Construction
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.
Wed 4 DecDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
10:30 - 12:00 | Logic and AutomataResearch Papers at Bali Room Chair(s): Peter Thiemann University of Freiburg, Germany | ||
10:30 30mTalk | Pumping, With or Without Choice Research Papers Aquinas Hobor National University of Singapore, Singapore, Elaine Li Runtime Verification, Inc., Frank Stephan National University of Singapore | ||
11:00 30mTalk | Simulations in Rank-Based Buchi Automata Complementation Research Papers Yu-Fang Chen Academia Sinica, Vojtěch Havlena Brno University of Technology, Ondřej Lengál Brno University of Technology | ||
11:30 30mTalk | Succinct Determinisation of Counting Automata via Sphere Construction Research Papers Lukáš Holík Brno University of Technology, Tomáš Vojnar Brno University of Technology, Ondřej Lengál Brno University of Technology , Lenka Turoňová Brno University of Technology, Margus Veanes Microsoft Research, Olli Saarikivi |