Learning Branching-Time Properties in CTL and ATL via Constraint Solving

TL;DR

This paper presents a novel approach for learning branching-time temporal properties, specifically CTL and ATL formulas, from system behavior samples by encoding the problem into satisfiability and implementing it in Python.

Contribution

It introduces a method to learn CTL and ATL formulas from Kripke and game structures using constraint solving and symbolic encoding, filling a gap in existing temporal logic learning research.

Findings

Successfully learned common CTL and ATL formulas from examples.

Developed a Python prototype implementing the learning algorithms.

Validated the approach on practical system behavior samples.

Abstract

We address the problem of learning temporal properties from the branching-time behavior of systems. Existing research in this field has mostly focused on learning linear temporal properties specified using popular logics, such as Linear Temporal Logic (LTL) and Signal Temporal Logic (STL). Branching-time logics such as Computation Tree Logic (CTL) and Alternating-time Temporal Logic (ATL), despite being extensively used in specifying and verifying distributed and multi-agent systems, have not received adequate attention. Thus, in this paper, we investigate the problem of learning CTL and ATL formulas from examples of system behavior. As input to the learning problems, we rely on the typical representations of branching behavior as Kripke structures and concurrent game structures, respectively. Given a sample of structures, we learn concise formulas by encoding the learning problem into a satisfiability problem, most notably by symbolically encoding both the search for prospective formulas and their fixed-point based model checking algorithms. We also study the decision problem of checking the existence of prospective ATL formulas for a given sample. We implement our algorithms in an Python prototype and have evaluated them to extract several common CTL and ATL formulas used in practical applications.