SAT-based learning of computation tree logic
In Proceedings of the 12th international joint conference (IJCAR’24), nancy, france, july 3–6, 2024
Abstract The CTL learning problem consists in finding for a given sample of positive and negative Kripke structures a distinguishing CTL formula that is verified by the former but not by the latter. Further constraints may bound the size and shape of the desired formula or even ask for its minimality in terms of syntactic size. This synthesis problem is motivated by explanation generation for dissimilar models, e.g. comparing a faulty implementation with the original protocol.