In this paper, we introduce a novel method for active learning of deterministic real-time one-counter automata (DROCA). The existing techniques for learning DROCA rely on observing the behaviour of the DROCA up to exponentially large counter-values. Our algorithm eliminates this need and requires only a polynomial number of queries. Additionally, our method differs from existing techniques as we learn a minimal counter-synchronous DROCA, resulting in much smaller counter-examples on equivalence queries. Learning a minimal counter-synchronous automaton cannot be done in polynomial time unless $P = NP$, even in the case of visibly one-counter automata. We use a SAT solver to overcome this difficulty. The solver is used to compute a minimal separating DFA from a given set of positive and negative samples. We prove that the equivalence of two counter-synchronous DROCAs can be checked significantly faster than that of general DROCAs. For visibly one-counter automata, we have discovered an even faster algorithm for equivalence checking. We implemented the proposed learning algorithm and tested it on randomly generated DROCAs. Our evaluations show that the proposed method outperforms the existing techniques on the test set.
I am pursuing my PhD in Theoretical Computer Science under the guidance of Dr. Sreejith A V in the School of Mathematics and Computer Science at Indian Institute of Technology, Goa. Currently, our research focuses on developing improved algorithms for the active learning of one-counter automata. Recently, we demonstrated that deterministic real-time one-counter automata (DROCAs) can be efficiently learned using a polynomial number of queries. This represents a significant advancement over previous algorithms, which required an exponential number of queries for learning DROCAs.
Earlier research also established that problems, including equivalence, regularity, and covering for weighted one-counter automata (over fields) with counter determinacy, can be solved in polynomial time. This finding mark a promising step toward addressing the open problem of equivalence of weighted one-counter automata.