Learning Real-Time One-Counter Automata Using Polynomially Many Queries

The problem of identifying a model from a given dataset is an area of interest in various fields of computer science, like formal verification and machine learning. However, inferring the right model from labelled samples is challenging. For instance, finding a minimal separating dfa  – a dfa that accepts a given set of positive samples and rejects a given set of negative samples – is known to be \(\textsf{NP}\)-complete [9]. Angluin [2] introduced an active learning framework called \(\textsc {L}^*\), involving a learner and a teacher. The learner can ask membership and equivalence queries to the teacher. Angluin showed that dfa can be learnt in polynomial time with respect to the size of the minimal dfa.

In this paper, we are interested in active learning of a deterministic real-time one-counter automaton (droca). These are finite-state machines equipped with a non-negative integer counter that can be incremented or decremented on reading an input symbol. The counter adds expressive power, enabling a droca to recognise certain non-regular context-free languages (e.g., \(\{a^nb^n\mid n>0\}\)). However, this added power also introduces significant challenges in learning.

Our contribution. We introduce the notion of counter-synchronous drocas  – two drocas are counter-synchronous if, for any word, the counter value reached on reading that word is the same on both machines. Given two drocas with \(\textsf{K}\) states, we give an \(\mathcal {O}(\textsf{K}^6)\) time¹ algorithm that solves the following two problems (see Theorem 3): (1) check if they are counter-synchronous, and (2) check whether they are equivalent, if they are counter-synchronous. For visibly one-counter automata (droca where the input alphabet determines the counter-actions), we have devised an even faster \(\mathcal {O}(\alpha (\textsf{K}^3)\textsf{K}^3)\) algorithm for checking equivalence (see Theorem 4).

The main result of this paper is a novel approach for active learning of drocas. However, the active learning framework differs from that introduced by Angluin in a few crucial aspects (see Section 4). Similar to the work by Bruyère et al. [4], we use an additional query called counter value query. This allows the learner to ask for the counter value reached on reading a word in the droca. Furthermore, the learner has access to a minimal synchronous-equivalence query on the droca. The teacher returns true for an equivalence query if the learnt droca is counter-synchronous and equivalent to the teacher’s droca. Otherwise, it returns a minimal word that violates this property.

In this framework, we give an algorithm that learns a minimal counter-synchronous droca. A key innovation in our approach is the use of a SAT solver for solving the \(\textsf{NP}\)-hard problem of finding a minimal separating dfa from a set of positive and negative samples. The solver, in conjunction with a modified version of \(\textsc {L}^*\), learns a characteristic dfa (see Definition 6). Subsequently, we use this characteristic dfa to construct a minimal counter-synchronous droca. Our algorithm requires only a polynomial number of queries to the SAT solver and the teacher. Consequently, our algorithm is in \(\mathsf {P^{NP}}\).

Justification for using a SAT solver. We argue that unless \(\mathsf {P=NP}\), learning a minimal visibly one-counter automaton (voca) cannot be done in polynomial time. This follows from the fact that minimisation of voca can be reduced to learning a minimal voca. Furthermore, It was pointed out by Michaliszyn and Otop [15] that minimising voca is \(\textsf{NP}\)-complete. This follows from the result by Gauwin et al.[8] that minimising vpda is \(\textsf{NP}\)-complete.

Comparison with existing methods. From a complexity theoretical perspective, drocas can be learned with polynomial space and exponential time with a straightforward brute-force approach. This method entails enumerating all conceivable drocas, starting with a one-state droca, and submitting equivalence queries for each. This approach, without a doubt, entails an exponential number of equivalence queries. All existing algorithms for learning drocas, including the algorithm by Fahmy and Roos [7], the algorithm by Bruyère et al. [4], and the algorithm for learning vocas by Neider and Löding [17] require exponential time and an exponential number of queries with respect to the number of states of a minimal droca recognising the language. All these algorithms share the idea of learning the initial portion of an infinite behavioural graph and then seek to identify a repetitive structure in it. However, in the worst-case scenario, this repetitive structure becomes apparent only after learning an exponentially large portion of the graph. In this case, the learnt droca will be exponentially large. Consequently, learning this exponential-sized behaviour necessitates exponentially many queries. Moreover, the equivalence queries also run on these exponentially large drocas, making it even more infeasible. Bruyère et al. [4] were the first to pursue a practical learning application of learning drocas. However, due to the difficulty in checking the equivalence of drocas, they had to use a weaker form of equivalence query that checks for counter-examples up to some random counter value. Their equivalence check might say two non-equivalent drocas are equivalent if the minimal counter-example is large.

Our approach (MinOCA) differs fundamentally from these existing methods by eliminating the need to observe the automaton’s behaviour up to exponentially large counter values. We propose an algorithm for learning drocas using only a polynomial number of queries. This sets it apart from existing techniques that require exponentially many queries for learning. One significant bottleneck in learning drocas is the equivalence test by the teacher. Given two drocas with number of states less than some \(\textsf{K}\in \mathbb {N}\), the equivalence check takes \(\mathcal {O}(\textsf{K}^{26})\) time². This is impractical for real-world applications. To mitigate this, we use the synchronous-equivalence check that runs in \(\mathcal {O}(\textsf{K}^6)\) time. We obtain significantly smaller counter-examples while using this equivalence check. Our equivalence queries are also on models whose size is less than or equal to a minimal counter-synchronised droca. Furthermore, unlike existing techniques that learn exponentially large drocas, our algorithm always learns an equivalent counter-synchronous droca with the minimal number of states.

Experiments. We evaluate an implementation of our algorithm and compare the results obtained with the existing technique by Bruyère et al. [4]. Experiments were conducted on randomly generated drocas with number of states ranging from 2 to 15 and the input alphabet size varying from 2 to 5. The results indicate that the proposed method outperforms the existing one [4].

The remainder of this paper is organised as follows: Section 2 gives the definitions and preliminaries. Section 3 gives equivalence results of counter-synchronised drocas. Section 4 details our learning algorithm for drocas, Section 5 covers the implementation details and presents our experimental results. Finally, Section 6 summarises our work and suggests future research directions.

For any finite set S, |S| denotes its cardinality. Non-negative numbers are denoted by \(\mathbb {N}\), and [i, j] denote the interval \(\{i, i+1, \ldots , j\} \subseteq \mathbb {N}\). For any \(d\in \mathbb {N}\), the sign of d (denoted by \(sign(d)\)) is defined as \(sign(d)=0\) if \(d=0\) and is 1 otherwise. Let \(w=a_0a_1a_2\ldots a_n \in \varSigma ^*\). For \(j,k\in [0,n]\), with \(j<k\), we use w[j] to denote the letter \(a_j\) and \(w_{[j \cdots k]}\) to denote the factor \(a_j a_{j+1}\cdots a_{k}\).

We use \(|\mathcal {A} |\) to denote the size of \(\mathcal {A} \), which we consider to be |Q|. A configuration \(\texttt {c}\) of a droca is a pair \((q, n)\in Q \times \mathbb {N}\), where \(q\in Q\) denotes the current state and \(n\in \mathbb {N}\) is the counter value. The configuration \(c_0=(q_0,0)\) is called the initial configuration of \(\mathcal {A} \). Let \(p,q \in Q, n\in \mathbb {N}, e \in \{-1,0,+1\}\) and \(a \in \varSigma \). A transition between two configurations (p, n) and \((q, n+e)\) on the symbol a is defined, if \(\delta _{sign(n)}({p},a) = ({q},e)\). We use \((p,n)\xrightarrow {a}(q,n+e)\) to denote this. A run on a word \(w=a_1\dots a_n\) from a configuration \((p_1,m_1)\) is the sequence of transitions \((p_1,m_1) \xrightarrow {a_1} (p_2,m_2) \xrightarrow {a_2} (p_3,m_3) \xrightarrow {a_3} \dots \xrightarrow {a_{n-1}} (p_n,m_n)\) where \(p_i \in Q\) and \(m_i\)s are counter values. In this case, we denote the run by \((p_1,m_1) \xrightarrow {w} (p_n,m_n)\). Note that the counter values always stay non-negative, implying a decrement is not permitted from a configuration with zero counter value.

Let \(q \in Q,\ n\in \mathbb {N}\), and \(w \in \varSigma ^*\) with \((q_0,0)\xrightarrow {w}(q,n)\). We use \({\texttt {ce}}_\mathcal {A} (w)= n\) to denote the counter value reached on reading w from the initial configuration. We call \({\texttt {ce}}_\mathcal {A} (w)\) the counter-effect of w. We denote by \(height_{\mathcal {A}}(w)\) the maximal counter-effect of the prefixes of w in \(\mathcal {A}\). We drop the subscript \(\mathcal {A} \) when the \(\textsc {droca} \) under consideration is evident. \(\mathcal {A} \) is deterministic (resp. complete) if, for any word w, there is at most (resp. at least) one run on w starting from any configuration. We say that a word w is accepted by \(\mathcal {A} \) if and only if \((q_0,0) \xrightarrow {w} (q_f,m)\) for some \(q_f \in F\) and \(m \in \mathbb {N}\). The language of \(\mathcal {A} \), denoted by \(\mathcal {L}(\mathcal {A})\), is the set of all words accepted by \(\mathcal {A} \). For convenience, we use \(\mathcal {A} (w)=1\) if \(w\in \mathcal {L}(\mathcal {A})\) and \(\mathcal {A} (w)=0\) otherwise. Two drocas \(\mathcal {A} \) and \(\mathcal {B} \) are equivalent if \(\mathcal {L}(\mathcal {A})=\mathcal {L}(\mathcal {B})\).

There are no \(\epsilon \)-transitions in a droca. We consider only complete drocas in this paper. Every incomplete droca can be made complete without changing its language by directing all the undefined transitions to a new non-final sink state.

The equivalence of drocas was shown to be in \(\textsf{NL}\) by Böhm and Göller [3]. They show that there exists a \(\mathcal {O}(\textsf{K}^{26})\) length word that distinguishes two non-equivalent drocas of size \(\textsf{K}\). However, this is not suitable for practical applications.

We give an efficient \(\mathcal {O}(\textsf{K}^6)\) algorithm to check the equivalence of counter-synchronised drocas. If two drocas are not counter-synchronised, then our algorithm outputs the smallest word for which they reach different counter values. If they are counter-synchronised and not equivalent, then our algorithm outputs the smallest word that is accepted by one and rejected by the other. In both these cases, the length of the counter-example is \(\mathcal {O}(\textsf{K}^5)\).

In Theorem 4, we can treat \(\alpha \) as a constant since \(\alpha (j) \le 4\) for all \(j<2^{1000}\) (see [1]). Hopcroft and Karp [11] showed that equivalence checking of two dfas of size n can be done in \(\mathcal {O}(\alpha (n)n)\) time.

A visibly one-counter automaton (voca) is a (droca) where the input alphabet is \(\varSigma = (\varSigma _{+}, \varSigma _{-},\varSigma _{0})\). The counter value is incremented (resp. decremented, not changed) on reading a symbol from \(\varSigma _{+}\) (resp. \(\varSigma _{-}\), \(\varSigma _0\)). Note that vocas over the same alphabet are counter-synchronous by definition as the word itself defines the counter value reached. For vocas, we give a faster \(\mathcal {O}(\alpha (\textsf{K}^3)\textsf{K}^3)\) time algorithm for equivalence checking using ideas from [14].

We consider the synchronous run of \(\mathcal {A} \) and \(\mathcal {B} \). A configuration pair of this synchronous run is \((\boldsymbol{\textbf{x}}_{(p,q)}, n)\) where \(p \in P, q \in Q\), and \(n \in \mathbb {N}\). The initial configuration pair is \(c_{\iota } = (\boldsymbol{\textbf{x}}_{(p_{\iota },q_{\iota })}, 0)\). Given two configuration pairs \(c_1=(\boldsymbol{\textbf{x}}_{(p,q)},n)\) and \(c_2=(\boldsymbol{\textbf{x}}_{(p',q')},m)\), \(c_1 \xrightarrow {u} c_2\) denotes \((p,n) \xrightarrow {u} (p',m)\) and \((q,n) \xrightarrow {u} (q',m)\). The transition matrix on u from \(c_1\) is \(\mathbb {M}\in \{0,1\}^{(|\mathcal {A} |+|\mathcal {B} |)^2}\) where \(\mathbb {M}[i,j]=1\) if and only if \((p_i,n) \xrightarrow {u} (p_j,m)\) or \((q_{i-|\mathcal {A} |},n)\xrightarrow {u}(q_{j-|\mathcal {A} |},m)\). Hence, \(\boldsymbol{\textbf{x}}_{(p,q)} \mathbb {M}= \boldsymbol{\textbf{x}}_{(p',q')}\). Claims 1 to 3 follow.

Let w be a minimal word such that \(\mathcal {A} (w)\ne \mathcal {B} (w)\). Let \(c_{\ell }=(\boldsymbol{\textbf{x}}_{\ell },n_{\ell })\) be such that \(c_{\iota } \xrightarrow {w} c_{\ell }\). Hence, \(\boldsymbol{\textbf{x}}_{\ell } {\boldsymbol{\mathbf {\eta }}}^\top \ne 0\). Note that there is no configuration pair that repeats during the run of w. Otherwise, we can remove the run between the repetitions to get a shorter word. This will contradict the minimality of w.

Let \(\textsf{K}\in \mathbb {N}\) such that \(|\mathcal {A} |,|\mathcal {B} |<\textsf{K}\). From Claim 4 and Claim 5, we get that \(height(w)\le 2(\textsf{K}+\textsf{K}^2)\). Similar to that in Theorem 3, we reduce the problem of finding the distinguishing word to equivalence check of dfas of size \(\mathcal {O}(\textsf{K}^3)\).    \(\square \)

In this section, we give an \(\textsc {L}^*\)-like algorithm for active learning of drocas using polynomially many queries with the help of a SAT solver. In this framework, we have a learner and a teacher. The learner aims to construct a droca that recognises the same language as the teacher’s droca (call it \(\mathcal {A} \)). The teacher answers the following types of queries by the learner.

The requirement for the teacher to return a counter-example z such that the counter values reached on reading z in the teachers and learners drocas are different can be removed. But in that case, we have to use the equivalence check for drocas (not necessarily counter-synchronous). The number of queries needed will be polynomial in the length of the minimal counter-example that distinguishes two drocas. Including this additional condition allows the use of the counter-synchronous equivalence check (see Theorem 3), which is much faster. The assumption of the teacher returning a minimal counter-example can be removed if we use partial-equivalence queries. A partial-equivalence query takes two drocas and a limit as inputs and determines whether the two drocas are equivalent for all words whose length does not exceed the limit. If they are not, then it returns a distinguishing word whose length is less than the limit. Neider and Löding [17] and Bruyère et al. [4] used partial-equivalence queries to learn the behaviour of drocas up to a certain counter value. One can simulate the teacher returning a minimal counter-example by a polynomial number of partial-equivalence queries. Similarly, a partial-equivalence query can be replaced with an equivalence query that returns a minimal counter-example.

The proposed method, henceforth denoted as MinOCA, was implemented in Python³ and is tested against a set of randomly generated drocas. In this section, we discuss the implementation details and compare MinOCA with the method by Bruyère et al. [4], hereafter referred to as BPS.

Equivalence Query: Even though there is a polynomial time algorithm to check the equivalence of two drocas  [3], the polynomial is so large that it is not suitable for practical applications. In MinOCA, we construct a droca that is counter-synchronised with the droca to be learnt. The equivalence is checked by a breadth-first search on the configuration graph up to the counter value and length obtained from Theorem 3. The minimal synchronous-equivalence query either returns a word for which the constructed droca and droca to be learnt reach different counter values or returns a word that is accepted by one and rejected by the other. In our implementation, after each equivalence query, we increment the value of d and make the table is d-closed and d-consistent.

One major distinction between MinOCA and BPS is that the latter employs an approximate equivalence query, while the former uses an exact equivalence query. This implies that the droca returned by BPS after learning may not be correct. On the other hand, the droca returned by MinOCA is always correct.

Finding a Minimal-Separating DFA: We utilise the Python library DFAMiner by Dell’Erba et al. [6] that uses a SAT solver to find a minimal separating dfa from a given set of positive and negative samples. Various other techniques for computing a minimal separating automaton can be found in [12, 16, 18].

Random Generation of DROCAs: We follow a procedure similar to that by Bruyère et al. [4] to randomly generate drocas with a given number of states.

Let \(n\in \mathbb {N}\) be the number of states of the droca to be generated. The procedure GenerateDROCA used to generate random drocas is as follows. First, we initialise the set of states \(Q=\{q_1,q_2,\ldots , q_n\}\). For all \(q\in Q\), we add q to the set of final states F with probability 0.5. If \(Q=F\) or \(F=\emptyset \) after this step, then we restart the procedure. Otherwise, for all \(q\in Q\) and \(a\in \varSigma \), we assign \(\delta _0(q,a)=(p,c)\) (resp. \(\delta _1 (q,a)=(p,c)\)), with p a random state in Q and c a random counter operation in \(\{0,+1\}\) (resp. \(\{0,+1,-1\}\)). The constructed droca is \(\mathcal {A} =(Q, \varSigma , \{q_1\}, \delta _0,\delta _1, F)\). If the number of reachable states of \(\mathcal {A}\) from the initial configuration is not n, then we discard \(\mathcal {A} \) and restart the whole procedure. Otherwise, we output \(\mathcal {A} \).

Dataset for comparing MinOCA and BPS. A dataset containing a total of 5600 drocas was generated, with the input alphabet size varying from 2 to 5 and the number of states ranging from 2 to 15. For each combination of input alphabet size and number of states, 100 random drocas were generated. The notion of acceptance in BPS is by final state and zero counter value. MinOCA employs the widely accepted notion of acceptance with the final state only. For comparison, we generated random drocas where both acceptance conditions coincide. In order to achieve this, we use the procedure GenerateDROCA with an added condition that mandates that the final states can only be reached by transitions that read a symbol from counter value of zero and do not modify the counter value.

Experimental Results: We implemented MinOCA in Python and used the Java implementation of BPS. The computations were performed on an Apple M1 chip with 8GB of RAM, running macOS Sonoma Version 14.3. MinOCA spends most of the time in finding a minimal separating dfa. The scalability of our algorithm is hence dependent on the scalability of finding a minimal separating dfa.

A timeout of 5 minutes was allotted for both BPS and MinOCA for learning each droca. If the algorithm times out, we discard that sample and process the next one. The number of languages successfully learned by MinOCA and BPS for different input sizes is depicted in Figure 3. Notice that MinOCA outperforms BPS in terms of the number of successfully learnt drocas.

Figure 4 shows the average length of the longest counter-examples. MinOCA provides a smaller counter-example on average. Figure 5 shows the average number of states in the learnt drocas. The number of states of the automaton learnt by MinOCA is always less than or equal to the input size. Figure 6 shows the average number of equivalence queries used for successfully learning the input drocas. The number of equivalence queries is smaller for MinOCA in all cases.

In Figures 7 and 8, MinOCA learns a minimal counter-synchronised droca equivalent to the input. However, the droca learnt by BPS is equivalent but is not counter-synchronous with respect to the input. It is also not complete.

In this paper, we presented a novel approach for active learning of drocas. We showed that a drocas can be learnt using polynomially many queries with the help of a SAT solver. This is in contrast to the existing techniques that require exponentially many queries. Our algorithm learns a minimal counter-synchronous droca, which results in significantly smaller counter-examples on equivalence queries. Additionally, the development of a specialised equivalence-checking algorithm for counter-synchronous drocas, with a time complexity of \(\mathcal {O}(n^6)\), further contributes to the feasibility of our approach. For vocas, we optimised this equivalence-checking process to \(\mathcal {O}(n^3)\), enabling efficient learning. We evaluated our algorithm against randomly generated drocas. The results indicate that our method significantly outperforms the existing method by Bruyère et al. [4].

In future work, the proposed algorithm can be improved by finding better methods for identifying the minimal separating dfa. The algorithm can also be applied to learn vocas, and the scalability of this approach warrants further investigation. Additionally, extending these ideas to learn more general models, such as visibly pushdown automata, represents a valuable direction for further research. Another open problem is to determine whether active learning of drocas can be done in polynomial time. This problem is open, even in the case of vocas. However, learning a minimal voca cannot be done in polynomial time unless \(\mathsf {P=NP}\). Exploring the possibility of finding a polynomial-time algorithm to obtain a polynomial approximation is worthy of further study.