Learning Reactive Systems

Reactive systems are systems (or programs) that interact with their environment via inputs and outputs in an on-going manner. The verification and synthesis problems for reactive systems can be solved using automata theoretic algorithms, working with automata on infinite objects (Lmautomata). In recent years, machine learning techniques, in particular automata inference, are being used for many applications in design and verification of reactive systems. Examples include black-box checking, assume-guarantee reasoning, finding security bugs, mining specifications, regular model-checking, learning verification fixpoints, localizing errors, programming networks, and program re~ pair. However, since there is a lack of learning algorithms for reactive systems, the techniques in these applications resort to using inference of automata on finite words. Using finite word automata inference limits the properties and systems that can be inferred, and does not enable applying learning techniques in many other applications in verification and synthesis of reactive systems.

Our research studies problems at the heart of the challenge of inferring u2~automata. We have shown that non-deterministic Buchi automata, one of the most popular acceptor for regular welanguages, are not polynomially pre-dictable with membership queries, under plausible cryptographic assumptions; while strongly unambiguous Buchi automata, an acceptor that can also recognized all regular w—languages, are polynomially predictable with membership queries.

Considering the passive learning paradigm, we have shown that the common non~deterministic w~automata are not identifiable in the limit using polynomial time and data, while the subset of deterministic wautomata with an informative right congruence, can be identifiable in the limit using polynomial time and data, and moreover, a polynomial sized characteristic set for these automata can be constructed in polynomial time.

We presented the first polynomial time algorithm to learn nontrivial classes of languages of infinite trees. The method is a general polynomial time reduction of learning a class of derived wetree languages to learning the une derlying class of w-word languages, for any class of weword languages accepted by deterministic Buchi automata. It uses another interesting result showing that subset queries that return counterexamples can be implemented in polynomial time using subset queries that return no counterexamples for deterministic or nondeterministic finite word acceptors, and deterministic or non—deterministic Bijchi automata.

Because the performance of a learning algorithm is bounded as a function of the size of the representation of the target language, we investigate size comparisons between the automata models we have shown learnable, namely strongly unambiguous Buchi automata, families of DFAs, and mod-Z—multiplicity automata, and common weautomata representations. We provided both upper and lower bounds for translating one model to the other, and for the vast majority the lower bounds asymptotically match the upper bounds.