Inferring Properties in Computation Tree Logic

TL;DR

This paper introduces a novel method for automatically inferring concise, language-minimal CTL specifications from finite state models, using counter-example guided and passive learning algorithms that encode model checking as SAT problems.

Contribution

It presents the first passive learning algorithm for CTL formulas from desirable and undesirable models, and a counter-example guided approach for inferring minimal, interpretable CTL specifications.

Findings

Developed a counter-example guided algorithm for CTL inference.

Created a passive learning algorithm encoding CTL model checking as SAT.

Achieved concise, language-minimal CTL formulas from finite models.

Abstract

We consider the problem of automatically inferring specifications in the branching-time logic, Computation Tree Logic (CTL), from a given system. Designing functional and usable specifications has always been one of the biggest challenges of formal methods. While in recent years, works have focused on automatically designing specifications in linear-time logics such as Linear Temporal Logic (LTL) and Signal Temporal Logic (STL), little attention has been given to branching-time logics despite its popularity in formal methods. We intend to infer concise (thus, interpretable) CTL formulas from a given finite state model of the system in consideration. However, inferring specification only from the given model (and, in general, from only positive examples) is an ill-posed problem. As a result, we infer a CTL formula that, along with being concise, is also language-minimal, meaning that it is rather specific to the given model. We design a counter-example guided algorithm to infer a concise and language-minimal CTL formula via the generation of undesirable models. In the process, we also develop, for the first time, a passive learning algorithm to infer CTL formulas from a set of desirable and undesirable Kripke structures. The passive learning algorithm involves encoding a popular CTL model-checking procedure in the Boolean Satisfiability problem.