Automata Learning and Its Applications



报告时间:2020年7月3日 星期五 20:00-21:00

报告地点:腾讯会议ID:472 664 298

报告摘要: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.

报告人简介: Lijun Zhang is a research professor at State Key Laboratory of Computer Science, Institute of Software Chinese Academy of Sciences, and a visiting professor at Shenzhen University. 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.


Copyright © BDSC