Learning Realtime One-Counter Automata

TL;DR

This paper introduces a novel learning algorithm for realtime one-counter automata that leverages membership, equivalence, counter value, and partial equivalence queries, demonstrated through benchmarks and JSON validation.

Contribution

It extends Angluin's L* algorithm with new query types to learn one-counter automata more effectively.

Findings

Successfully learned automata from random benchmarks

Effective in JSON-stream validation use case

Demonstrated practical applicability of the algorithm

Abstract

We present a new learning algorithm for realtime one-counter automata. Our algorithm uses membership and equivalence queries as in Angluin's L* algorithm, as well as counter value queries and partial equivalence queries. In a partial equivalence query, we ask the teacher whether the language of a given finite-state automaton coincides with a counter-bounded subset of the target language. We evaluate an implementation of our algorithm on a number of random benchmarks and on a use case regarding efficient JSON-stream validation.