Learning Realtime One-Counter Automata

Automata used to model a software or hardware system can be large and tedious to construct. The concept of active automata learning, introduced by Angluin in [1], aims at inferring an automaton in a black-box manner, that is, by only observing runs of the system without having access to its implementation. In this presentation, we focus on learning of realtime one-counter automata. The main idea behind Angluin’s framework is as follows: a learner wants to learn a deterministic finite automaton (DFA) accepting a language L in in-teraction with a teacher who knows a DFA accepting L. The interactions with the teacher are limited to two types of queries: membership queries where the learner asks whether a word belongs to the language L, and equivalence queries where the learner asks whether a conjectured automaton accepts L. If the answer of an equivalence query is negative, the teacher provides a counterexample (a word witnessing non-equivalence). The algorithm called L∗ proposed in [1] uses a data structure called observation table to store the learnt knowledge. For each pair (u, v) of words of this 2-D table, a membership query over uv is asked in order to fill the cell. Once the table satisfies two conditions, namely the table must be closed and consistent, the learner is able to construct a DFA from it and ask an equivalence query about it. If the teacher answers true, then the learning process is done. Otherwise, the learner uses the provided counterexample to refine the observation table and repeats this process. Realtime one-counter automata (ROCA) are deterministic finite automata augmented with a natural-valued counter. On each transition, the allowed counter operations are −1, 0, or +1. A word is accepted by an ROCA if the run ends in an accepting state with a counter value equal to zero, and the counter value never goes below 0 while reading the word. A language L accepted by an ROCA defines a (potentially) infinite deterministic automaton A_L accepting L, obtained by unfolding the counter value. Fortunately, this automaton A_L has a finite ultimately periodic description, i. e. , a description with a “prefix” part followed by a part that is repeated ad infinitum. From this periodic description, it is possible to construct an ROCA accepting L. The idea behind our learning algorithm for L is to first learn a sufficiently large prefix of A_L, extract a valid ultimately periodic description from the prefix, and construct an ROCA accepting L from the description. Fahmy and Roos already proposed a learning algorithm for ROCAs in [2] but we are unable to replicate the proofs. Our algorithm shares some ideas with the learning algorithm proposed in [4] for visibly one-counter automata. However the process of learning ROCAs is more difficult since the counter value cannot be derived from the alphabet. In our work with Véronique Bruyère (University of Mons) and Guillermo A. Pérez (University of Antwerp), we propose a new learning algorithm for ROCAs, based on L∗. We still have a teacher and a learner interacting, but, this time, four queries are available: membership and equivalence queries as before, and counter value queries to request the counter value of a word, and partial equivalence queries to check whether the learnt prefix of the automaton A_L is correct. The observation table must now store the results of both membership and counter value queries and encode the prefix of A_L, up to some counter limit l. Once the table is closed and consistent, a DFA is created and a partial equivalence query is asked about it. If the teacher returns a counterexample, the table is refined, without increasing l. If the teacher answers true, then from this correct prefix of A_L, we extract multiple potential ultimately periodic descriptions, construct an ROCA from each of them, and ask equivalence queries for each ROCA. If one of them accepts the target language, then the learning process is done. Otherwise, we increase the counter limit l, use one of the counterexamples to refine the table, and repeat the process. We have developed a prototype tool implementing our learning algorithm. Learning an ROCA can be useful to infer a JSON Schema [3], a formalism used to annotate and validate JSON documents. In order to learn a JSON Schema, the four queries are implemented as follows. Membership queries determine whether a document satisfies the schema, which can be checked with a JSON validator. Counter values are defined by either the number of unmatched list-start symbols [ or the number of unmatched object-start symbols { in an (incomplete) JSON document. For both equivalence and partial equivalence, as in most active learning setups, we employ conformance testing techniques for DFAs in the partial equivalence case and JSON generators in the full equivalence case. [1] Dana Angluin. “Learning Regular Sets from Queries and Counterexamples”. In: Inf. Comput. 75. 2 (1987), pp. 87–106. doi: 10. 1016/0890-5401(87)90052-6. [2] Amr F. Fahmy and Robert S. Roos. “Efficient Learning of Real Time One-Counter Automata”. In: Algorithmic Learning Theory, 6th International Conference, ALT ’95, Fukuoka, Japan, October 18-20, 1995, Proceedings. Ed. by Klaus P. Jantke, Takeshi Shinohara, and Thomas Zeugmann. Vol. 997. Lecture Notes in Computer Science. Springer, 1995, pp. 25–40. doi: 10. 1007/3-540-60454-5_26. [3] JSON Schema. URL: https: //json-schema. org [4] Daniel Neider and Christof Löding. Learning visibly one-counter automata in polynomial time. Technical Report AIB-2010-02. RWTH Aachen, 2010.

Authors

• Gaëtan Staquet

Keywords

No keywords are indexed for this paper.