Conflict-Aware Active Automata Learning

Formal methods have a long history of success in the analysis of critical systems through abstract models. These methods are rapidly expanding their range of applications and recent years saw an increase in industrial teams applying them to (large-scale) software [6, 9, 10, 12, 13, 25]. The applicability of such methods is limited by the availability of good models, which require time and expert knowledge to be hand-crafted and updated. To overcome this issue, a research area on automatic inference of models, called model learning [32], has gained popularity. Broadly, there are two classes of model learning: passive learning, which attempts to infer a formal model from a static log, and active learning, where interaction with the system is allowed to refine knowledge during the inference. In this paper, we focus on active learning, motivated by its successful use in verification tasks, e.g. in analyzing network protocol implementations, as TCP [18], SSH [19], and QUIC [15], or understanding the timing behavior of modern CPUs [34]. Current state-of-the-art active learning algorithms rely on the Minimally Adequate Teacher (MAT) framework [4], which formalizes a process with two agents: a learner and a teacher. The learner tries to infer a formal model of a system, and the teacher is omniscient of the system, being able to answer queries on potential behaviors and the correctness of the learned model. MAT assumes that the interactions between both agents are perfect and deterministic. Learning In Practice Interactions with the System Under Learning (SUL) are often non-deterministic in some way, e.g. the communications can be noisy (i.e.