Lazy Synthesis Techniques

The problem of reactive synthesis asks for the automated construction of systems that adhere to input logical specifications. In practice, it is commonly solved by a reduction to games that involves the determinisation of automata that encode the input specification. We will develop methods for avoiding the obstacles that slow down this process, proceeding in two orthogonal directions:

We will identify concrete special cases in which history determinism can be used in place of full determinism in the reduction to games, leading to asymptotically faster synthesis algorithms for the identified special cases. We will pay special attention to obtaining syntactic characterisations of these special cases, ensuring that they can be efficiently recognised.

We will also generalise existing game reduction methods by using succinct Emerson-Lei objectives in the resulting games rather than parity ones; by evaluating approximations to solutions of these games by means of lazy algorithms; by providing efficient back-end algorithms for quantitative (multi-valued) synthesis; and finally by lifting quasipolynomial worst-case guarantees from parity objectives to the general case of quantitative Emerson-Lei objectives.

Since these advancements in both directions aim at improved practical performance, we will also evaluate the developed algorithms and automata transformations with a prototypical implementation that will be benchmarked against existing hard example instances of the synthesis problem, comparing its performance with the currently leading tools (where they exist) and determine the scope and limitation of our results.