Miaomiao Zhang, Professor, School of Software, Tongji University

Zhongzhi Bai, Professor

Learning Deterministic One-Clock Timed Automata via Mutation Testing

11:00-12:00 October 22(Saturday), Tencent Meeting ID: 212-980-950

In active learning, an equivalence oracle is supposed to answer whether a hypothesis model is equivalent to the system under learning. Its implementation in real applications is considered a major bottleneck for active automata learning. The problem is especially difficult in the context of learning timed automata due to the infinitely large state space involved. In this work, following the framework of combining mutation analysis and random testing, we propose an implementation of equivalence oracle in the context of learning deterministic one-clock timed automata (DOTAs). This includes two learning-friendly mutation operators, a heuristic test-case generation method, and a score-based test-case selection method. We implemented a prototype applying our approach by extending an existing tool on active learning of DOTAs, and conducted extensive experiments. The results indicate that our method improves upon existing methods on rate of learning correct models, number of test cases required, and accumulated delay time in test cases.