Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Learning real-time one-counter automata using polynomially many queries

Prince Mathew, Vincent Penelle, A. V. Sreejith

TL;DR

The paper tackles learning deterministic real-time one-counter automata (DROCA) using active learning with polynomial query complexity, addressing the NP-hard barrier of minimal separation through a SAT-based construction. It introduces counter-synchronous DROCA and develops efficient equivalence checks (O(K^5) for general counter-synchronised DROCAs and O(K^3) for voca), placing learning in the $P^{NP}$ class when combined with these checks. The MinOCA algorithm, a SAT-assisted L*-style learner, builds a minimal counter-synchronous DROCA by deriving a characteristic DFA from an observation table and converting it to a DROCA, with a provable bound of at most $| ext{A}|^5+1$ minimal synchronous-equivalence queries. Experimental results on randomly generated DROCAs demonstrate that MinOCA outperforms the prior BPS method in terms of counter-example size, learned automata compactness, and overall query efficiency, validating the practical viability of the approach and suggesting avenues for extending to voca and visibly pushdown automata.

Abstract

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 DROCA 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.

Learning real-time one-counter automata using polynomially many queries

TL;DR

The paper tackles learning deterministic real-time one-counter automata (DROCA) using active learning with polynomial query complexity, addressing the NP-hard barrier of minimal separation through a SAT-based construction. It introduces counter-synchronous DROCA and develops efficient equivalence checks (O(K^5) for general counter-synchronised DROCAs and O(K^3) for voca), placing learning in the class when combined with these checks. The MinOCA algorithm, a SAT-assisted L*-style learner, builds a minimal counter-synchronous DROCA by deriving a characteristic DFA from an observation table and converting it to a DROCA, with a provable bound of at most minimal synchronous-equivalence queries. Experimental results on randomly generated DROCAs demonstrate that MinOCA outperforms the prior BPS method in terms of counter-example size, learned automata compactness, and overall query efficiency, validating the practical viability of the approach and suggesting avenues for extending to voca and visibly pushdown automata.

Abstract

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 DROCA 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.

Paper Structure

This paper contains 26 sections, 9 theorems, 2 equations, 22 figures, 10 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Our contribution.
  3. Justification for using a SAT solver.
  4. Comparison with existing methods.
  5. Experiments.
  6. Definitions and Preliminaries
  7. Equivalence of Counter-Synchronised DROCAs
  8. Learning DROCAs
  9. Observation Table
  10. Constructing a DROCA from an Observation Table
  11. Constructing a Characteristic DFA Using a SAT Solver:
  12. Constructing a DROCA from a Characteristic DFA:
  13. MinOCA: The Learning Algorithm
  14. Example: MinOCA in Action.
  15. Analysis of "MinOCA":
  16. ...and 11 more sections

Key Result

theorem thmcountertheorem

Let $\mathcal{A}$ and $\mathcal{B}$ be "drocas" where $|\mathcal{A}\xspace|,|\mathcal{B}\xspace|\leq\mathsf{K}$. If $\mathcal{A}$ is not "counter-synchronised" and "equivalent" to $\mathcal{B}$, then there is a minimal word $w$ where $|w|\leq 2\mathsf{K}^5$, $"height_{\mathcal{A}\xspace}"(w),\ "heig

Figures (22)

  • Figure 1: The figure shows the synchronous run of a word on two "vocas" such that it reaches a final state in one "voca" and a non-final state in the other. The dashed line denotes the part of the synchronous run that can be removed.
  • Figure 2: A "droca" recognising the language $\{a^nb^na \mid n>0\}$ is given in \ref{['vocaEx']}. The "characteristic dfa" corresponding to this "droca" is shown in \ref{['underlyingDFA']}.
  • Figure 3: Example: The "droca" under learning.
  • Figure 4: The "characteristic dfa" obtained from $\texttt{"ConstructAutomaton"}$ using \ref{['tabExMinOCA2']} as input.
  • Figure 5: The "droca" obtained from the "characteristic dfa" in \ref{['DFAexminOCA1']}.
  • ...and 17 more figures

Theorems & Definitions (21)

  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • theorem thmcountertheorem
  • theorem thmcountertheorem
  • proof
  • Claim 1
  • Claim 2
  • Claim 3
  • Claim 4
  • Claim 5
  • ...and 11 more