Prof. Lijun Zhang

Title: Omega-automata learning algorithms and its applications

Biography

Lijun Zhang is a research professor at State Key Laboratory of Computer Science, Institute of Software Chinese Academy of Sciences. Before this he was an associate professor at Language-Based Technology section, DTU Compute, Technical University of Denmark. Before this he was a postdoctoral researcher at University of Oxford. He gained a Diploma Degree and a PhD (Dr. Ing.) at Saarlandes University. His research interests include: probabilistic models, simulation reduction, decision algorithms for probabilistic simulation preorders, abstraction and model checking. Recently, he is working in combining automata learning techniques with model checking. He is leading the development of the model checker IscasMC.

Abstract

Learning-based automata inference techniques have received significant attention from the community of formal system analysis. In general, the primary applications of automata learning in the community can be categorized into two: improving efficiency and scalability of verification and synthesizing abstract system model for further analysis. Most of the results in the literature focus on checking safety properties or synthesizing finite behavior models of systems/programs. On the other side, Büchi automaton is the standard model for describing liveness properties of distributed systems. Unlike the case for finite automata learning, learning algorithms for Büchi automata are very rarely used in our community. In this talk, we present algorithms to learn a Büchi automaton from a teacher who knows an omega-regular language. The algorithm is based on learning a formalism named family of DFAs (FDFAs) recently proposed by Angluin and Fisman. The main catch is that we use a classification tree structure instead of the standard observation table structure. The worst case storage space required by our algorithm is quadratically better than the table-based algorithm. We implement the first publicly available library ROLL (Regular Omega Language Learning), which consists of all omega-regular learning algorithms available in the literature and the new algorithms proposed in this paper. Further, with our tool, we demonstrate how our algorithm can be exploited in classical automata operations such as complementation checking and in the model checking context.

Course material:

* Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987)

* Kearns, M.J., Vazirani, U.V.: An Introduction to Computational Learning Theory. MIT Press, Cambridge (1994)

* Li Y., Chen YF., Zhang L., Liu D. (2017) A Novel Learning Algorithm for Büchi Automata Based on Family of DFAs and Classification Trees. TACAS 2017. LNCS vol 10205.