Mutating Skeletons: Learning Timed Automata via Domain Knowledge

Formal verification techniques, such as model checking, can provide valuable insights and guarantees for (safety-critical) devices and their possible behavior. However, these guarantees only hold true as long as the model correctly reflects the system. Automata learning provides a huge advantage there as it enables not only the automatic creation of the needed models but also ensures their correct reflection of the system behavior. However, and this holds especially true for real-time systems, model learning techniques can become very time consuming. To combat this, we show how to integrate given domain knowledge into an existing approach based on genetic programming to speed up the learning process. In particular, we show how the genetic programming approach can take a (possibly abstracted, incomplete or incorrect) untimed skeleton of an automaton, which can often be obtained very cheaply, and augment it with timing behavior to form timed automata in a fast and efficient manner. We demonstrate the approach on several examples of varying sizes.