  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.
