LTL Reactive Synthesis with a Few Hints

TL;DR

This paper introduces a novel LTL reactive synthesis method that incorporates user-provided execution examples to guide the synthesis process, improving efficiency and practicality.

Contribution

It presents a two-phase synthesis algorithm that generalizes user examples and guarantees completeness with polynomial complexity, extending classical LTL synthesis techniques.

Findings

The approach can learn any Mealy machine realizing the specification with few examples.

The synthesis process is polynomial in the size of examples and symbolic solution representations.

Practical experiments demonstrate the method's effectiveness on real examples.

Abstract

We study a variant of the problem of synthesizing Mealy machines that enforce LTL specifications against all possible behaviours of the environment including hostile ones. In the variant studied here, the user provides the high level LTL specification {\phi} of the system to design, and a set E of examples of executions that the solution must produce. Our synthesis algorithm works in two phases. First, it generalizes the decisions taken along the examples E using tailored extensions of automata learning algorithms. This phase generalizes the user-provided examples in E while preserving realizability of {\phi}. Second, the algorithm turns the (usually) incomplete Mealy machine obtained by the learning phase into a complete Mealy machine that realizes {\phi}. The examples are used to guide the synthesis procedure. We provide a completeness result that shows that our procedure can learn any Mealy machine M that realizes {\phi} with a small (polynomial) set of examples. We also show that our problem, that generalizes the classical LTL synthesis problem (i.e. when E = {\emptyset}), matches its worst-case complexity. The additional cost of learning from E is even polynomial in the size of E and in the size of a symbolic representation of solutions that realize {\phi}. This symbolic representation is computed by the synthesis algorithm implemented in Acacia-Bonzai when solving the plain LTL synthesis problem. We illustrate the practical interest of our approach on a set of examples.