Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Learning Deterministic One-Counter Automata in Polynomial Time

Prince Mathew, Vincent Penelle, A. V. Sreejith

TL;DR

This work tackles the problem of learning deterministic one-counter automata (DOCAs) in polynomial time using active learning. It introduces OL*, a black-box learning algorithm that operates with membership queries and minimal equivalence queries to produce a DOCA recognizing the target language, with runtime polynomial in the size of the minimal DOCA. The approach circumvents exponential-state barriers of prior methods by learning a bounded behavioural DFA, partitioning the DFA into regions, and constructing a DOCA via a polynomially bounded coloring and partial-DOCA assembly process; it also yields a way to approximate DOCA minimisation. The results bridge learning and minimisation for DOCAs, showing polynomial-time learnability and offering a viable avenue for approximating minimal DOCAs, albeit with potentially larger output sizes than the true minimum. The framework advances formal verification and automata-learning applications by providing a scalable route to learn and refine DOCA-based models without counter-value queries.

Abstract

We give an active learning algorithm for deterministic one-counter automata (DOCAs) where the learner can ask the teacher membership and minimal equivalence queries. The algorithm called OL* learns a DOCA in time polynomial in the size of the smallest DOCA, recognising the target language. All existing algorithms for learning DOCAs, even for the subclasses of deterministic real-time one-counter automata (DROCAs) and visibly one-counter automata (VOCAs), in the worst case, run in exponential time with respect to the size of the DOCA under learning. Furthermore, previous learning algorithms are ``grey-box'' algorithms relying on an additional query type - counter value query - where the teacher returns the counter value reached on reading a given word. In contrast, our algorithm is a ``black-box'' algorithm. It is known that the minimisation of VOCAs is NP-hard. However, OL* can be used for approximate minimisation of DOCAs. In this case, the output size is at most polynomial in the size of a minimal DOCA.

Learning Deterministic One-Counter Automata in Polynomial Time

TL;DR

This work tackles the problem of learning deterministic one-counter automata (DOCAs) in polynomial time using active learning. It introduces OL*, a black-box learning algorithm that operates with membership queries and minimal equivalence queries to produce a DOCA recognizing the target language, with runtime polynomial in the size of the minimal DOCA. The approach circumvents exponential-state barriers of prior methods by learning a bounded behavioural DFA, partitioning the DFA into regions, and constructing a DOCA via a polynomially bounded coloring and partial-DOCA assembly process; it also yields a way to approximate DOCA minimisation. The results bridge learning and minimisation for DOCAs, showing polynomial-time learnability and offering a viable avenue for approximating minimal DOCAs, albeit with potentially larger output sizes than the true minimum. The framework advances formal verification and automata-learning applications by providing a scalable route to learn and refine DOCA-based models without counter-value queries.

Abstract

We give an active learning algorithm for deterministic one-counter automata (DOCAs) where the learner can ask the teacher membership and minimal equivalence queries. The algorithm called OL* learns a DOCA in time polynomial in the size of the smallest DOCA, recognising the target language. All existing algorithms for learning DOCAs, even for the subclasses of deterministic real-time one-counter automata (DROCAs) and visibly one-counter automata (VOCAs), in the worst case, run in exponential time with respect to the size of the DOCA under learning. Furthermore, previous learning algorithms are ``grey-box'' algorithms relying on an additional query type - counter value query - where the teacher returns the counter value reached on reading a given word. In contrast, our algorithm is a ``black-box'' algorithm. It is known that the minimisation of VOCAs is NP-hard. However, OL* can be used for approximate minimisation of DOCAs. In this case, the output size is at most polynomial in the size of a minimal DOCA.

Paper Structure

This paper contains 20 sections, 12 theorems, 4 equations, 6 figures, 4 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Deterministic one-counter automata
  4. Active learning paradigm
  5. Discussion
  6. Exponential state-of-the-art algorithms
  7. Difficulty in learning a minimal DOCA
  8. Reset transitions
  9. Overview: algorithm
  10. Preliminary results
  11. Lexicographically minimal reachability witness
  12. Behavioural DFA
  13. Winning candidate sequence
  14. algorithm
  15. Learning in polynomial time
  16. ...and 5 more sections

Key Result

Theorem 1

Given a $\dul\ L$, there is a polynomial time algorithm ("") that learns a "doca" recognising $L$ using polynomially many "membership" and "minimal equivalence queries".

Figures (6)

  • Figure 1: The initial portion of the "configuration graph" of "voca" shown in \ref{['exBg']}. The counter values of configurations are given at the top. Transitions not shown in the configuration graph lead to state $q_7$ with the appropriate counter value. Configurations drawn with dotted circles do not have a word that is accepted from them.
  • Figure 2: A "voca" over the "pushdown alphabet" $\Sigma= (\{a\}, \{b\} \cup \bigcup_{i \in S} \{{\mathfrak{p}_i}\}, \emptyset)$ for the language $\texttt{PrimeMatch}(\{2,3\})$. Note that $(q_1,6) "\equiv" (q_3,6)$ but $(q_1,3) "\not\equiv" (q_3,3)$. All transitions not shown in the figure go to a non-final sink state $q_7$.
  • Figure 3: The initial portion of the "behavioural dfa" of "voca" shown in \ref{['exBg']}. Each state in the "behavioural dfa" represents an equivalence class of the Myhill-Nerode congruence. Equivalent configurations in the configuration graph will be a single state in the "behavioural dfa". The state $t$ drawn with a dotted circle does not have a word that is accepted from it, and all the transitions that are not shown in the graph go to this state.
  • Figure 6: Two "candidate sequences" "centered at" $p_0$. Either of them could be "$d$-winning".
  • Figure 7: Shift in sequences.
  • ...and 1 more figures

Theorems & Definitions (21)

  • Theorem 1
  • Definition 2
  • Proposition 3: docaequiv
  • Example 4
  • Corollary 5
  • Lemma 6
  • Lemma 7
  • Lemma 8
  • Remark 1
  • Remark 2
  • ...and 11 more