Learning one-counter automata using SAT solver

In this presentation, we introduce a novel method for active learning of a minimal-sized Visibly one-counter automaton ($VOCA$) using SAT solver. We follow Angluin's $L^*$ algorithm. The algorithm uses only a polynomial number of membership or equivalence queries. All the existing literature, including the algorithm presented by Neider and Löding for learning $VOCA$, requires exponentially many queries relative to the size of a minimal $VOCA$ recognising the given language. Our approach eliminates the necessity to observe the $VOCA$'s behaviour up to exponentially large counter values. This sets it apart from existing techniques that rely on identifying repetitive patterns in behaviour graphs of exponential size. Michaliszyn and Otop observed that the problem of finding the minimal $VOCA$ is ${NP}$-Complete. If a polynomial time algorithm for learning the minimal $VOCA$ exists, it could be employed to minimise $VOCA$ in polynomial time. Consequently, a learning algorithm for $VOCA$ that achieves minimal representation in polynomial time does not exist. In the latter part of the work, we looked at learning Deterministic real-time one-counter automata ($DROCA$). However, we make use of an additional query, called counter-value query - the student gives the teacher a word, and the teacher returns the counter-value reached on traversing the word in the $DROCA$. We show that learning $DROCA$ can done using polynomially many queries within this framework. This improves the existing result by Bruy`ere et al. that needed an exponential number of queries, space and time for learning $DROCA$. This is a joint work with Dr. Vincent Penelle (Univ. Bordeaux) and Dr. Sreejith A. V (IIT Goa).

Authors

• Prince Mathew

Keywords

No keywords are indexed for this paper.