The Futures of Reactive Synthesis

The synthesis of reactive systems has been actively investigated since the inception of the problem by Alonzo Church more than sixty years ago. This talk gives an overview of the main results of the area and an outlook on potential future directions to be discussed in the seminar, including neural-symbolic computation and, more generally, machine learning techniques, template-based solving in the context of constraint programming, active learning algorithms, and connections to program synthesis and in particular Syntax Guided Synthesis.

This talk surveys the results on learning automata models for regular languages of infinite words. It discusses several positive and negative results across different learning paradigms. The positive results are mostly for automata models that are less common, in particular families of DFAs (FDFAs), strongly unambiguous Büchi automata (SUBAs) and mod-2 multiplicity automata (M2MA). These models have other good qualities, in particular the complexity of the boolean operations (intersection, union, complementation) and decision problems (emptiness, inclusion, equivalence) are good compared to the common omega-automata types. It is thus worth exploring whether they can also be usable for model checking and synthesis of reactive systems.

The distributed synthesis problem is to translate a logical specification of a distributed system into an implementation that is guaranteed to satisfy the specification. What makes the synthesis of distributed systems far more challenging than standard reactive synthesis is that each component only has partial knowledge of the global system state. Currently, there are no scalable algorithms for distributed synthesis. The challenge is to devise a compositional synthesis method, i.e., a method that constructs one component at a time. The fundamental difficulty is that the components often need to act upon information that is available only in another component. However, we do not know how that component encodes the information before we know its implementation; seemingly, it is impossible to build one component without knowing the implementation of the other. In this talk, I will present a compositional synthesis method based on the key idea of characterizing the necessary flow of information between the components as a hyperproperty. We introduce information flow assumptions, which are requirements that are necessary in order to realize a particular component. By formulating these assumptions as hyperproperties, we avoid referring to any particular encoding of the information. We develop methods that automatically derive information flow assumptions from the specification and a technique for the automatic synthesis of component implementations based on information flow assumptions. Together, these methods provide a compositional approach to the synthesis of distributed systems.

The talk gave an overview of several approaches to distributed reactive synthesis: Pnueli & Rosner model, controller synthesis for Zielonka automata and controller synthesis for lock-sharing systems. While partial information is a direct source of undecidability in the Pnueli & Rosner model, full causal information does not guarantee decidability either (cf. Gimbert 2022). Loose synchronization as in lock-sharing systems allows to recover decidability of controller synthesis at reasonable cost.

While reactive synthesis and syntax-guided synthesis (SyGuS) have seen enormous progress in recent years, combining the two approaches has remained a challenge. To overcome this obstacle, we introduced Temporal Stream Logic (TSL) [1], a new temporal logic that separates control and data. We developed a CEGAR-like synthesis approach for the construction of implementations that are guaranteed to satisfy a TSL specification for all possible instantiations of the data processing functions. However, specifications often involve interpreted functions: for example, arithmetic functions or string manipulations. We extended TSL to Temporal Stream Logic modulo theories (TSL-MT) [2], a framework that unites the two approaches to synthesize a single program. In our approach, reactive synthesis and SyGuS collaborate in the synthesis process, and generate executable code that implements both reactive and data-level properties. We demonstrate the applicability of our approach over a set of real-world benchmarks [3].

In classic program synthesis algorithms, such as counterexample-guided inductive synthesis (CEGIS), the algorithms alternate between a synthesis phase and an oracle (verification) phase. Many (most) synthesis algorithms use a white-box oracle based on satisfiability modulo theory (SMT) solvers to provide counterexamples. But what if a white-box oracle is either not available or not easy to work with?

In this talk, I will present a framework for solving a general class of oracle-guided synthesis problems which we term synthesis modulo oracles (SyMO). In this setting, oracles are black boxes with a query-response interface defined by the synthesis problem. This allows us to lift synthesis to domains where using an SMT solver as a verifier is not practical.

The Reactive Synthesis Competition (SYNTCOMP) is a competition for reactive synthesis tools. The competition’s goal is to collect benchmarks in a publicly available library and foster research in new tools for automatic synthesis of systems. SYNTCOMP is organized annually (since 2014) as a satellite event of CAV.

In this talk, the status of the competition (in particular the state of the benchmarks) and its evolution through the last couple of years is presented.

There has been an explosion of interest in the use of LLMs to generate code in recent years, complimenting a long history of formal methods-driven program synthesis. However, code generation remains a largely all-or-nothing problem – either users can take advantage of the flexibility and adaptivity of LLMs and generate code that might not be correct, or they can rely on more rigid program synthesis tools which are guaranteed to generate correct results, but are limited in their generative grammars. In this talk, we propose a strategy for the combination of these techniques – leveraging formal methods to generate structures of provable correct programs, and allowing the LLM to complete the details with more flexibility. We focus on the problem of generating reactive programs, where these types of programs consume streams of input and produce streams of output. These programs are critical across application domains, including circuit design, self-driving cars, mobile apps, and chatbots – all of which we have been able to synthesize using our synthesis procedure. We end with an outline of the challenges still facing the integration of reactive synthesis into code generation paradigms.

Neural-symbolic computing offers a broad and largely unexplored spectrum of integrating neural and algorithmic components for developing new solutions to the reactive synthesis problem. At one end of the spectrum are purely symbolic and algorithmic methods that defined the field from its very beginning. In this talk, we will move to the other end of the spectrum and discuss how far we can get by relying on pure deep learning methods to solve synthesis problems. In particular, three approaches are presented that trace the current developments in deep learning:

1. 1.

   training neural networks from scratch on data derived from specification patterns,

2. 2.

   fine-tuning language and code generation models,

3. 3.

   evaluating large language models and few-shot prompting on instances of parameterized specifications.

We specifically focus on representing the structure of synthesis problems in neural network architectures, the bundling of both algorithmic tools and neural networks, and we hope to spark discussions about approaches that are centred on the spectrum of neural-symbolic methods.

Feedback allows systems to seamlessly and instantaneously adapt their behavior to their environment and is thereby the fundamental principle of life and technology – it lets animals breathe, it stabilizes the climate, it allows airplanes to fly, and the energy grid to operate. During the last century, control technology excelled at using this power of feedback to engineer extremely stable, robust, and reliable technological systems. With the ubiquity of computing devices in modern technological systems, feedback loops become cyber-physical – the laws of physics governing technological, social or biological processes interact with (cyber) computing systems in a highly nontrivial manner, pushing towards higher and higher levels of autonomy and self-regulation. While stability, reliability and robustness remain to be of uppermost importance in these systems, a control-inspired utilization of cyber-physical feedback loops for this purpose is lacking far behind. In this talk, I will discuss how a control-inspired view on formal methods for reliable software design can enable us to utilize the power of feedback for robust and adaptable cyber-physical system design.

In this talk, I describe some recent efforts to combine functional and reactive synthesis. In the first part of the talk, I describe the Sketch program synthesis system, which allows users to write partial programs and solves for the missing details using an SMT solver. The talk focused on a new feature in Sketch that allows the user to write temporal specifications describing the behaviour of the program through its execution and showed how such constraints could be used to speed up the synthesis process and to give the user more control over the resulting program.

During the second part of the talk, I described a new effort to use a combination of reactive and functional synthesis to derive models of an environment from observations. The idea was implemented in a tool called Autumn, which focuses on pixel-world domains and is able to synthesize functional reactive programs from observations.

We present a multi-objective optimization approach for synthesizing interpretations of black-box models. Existing methods for synthesizing interpretations use a single objective function and are often optimized for a single class of interpretations. In contrast, we provide a more general and multi-objective synthesis framework that allows users to choose (1) the class of syntactic templates from which an interpretation should be synthesized, and (2) quantitative measures on both the correctness and explainability of an interpretation. For a given black-box, our approach yields a set of Pareto-optimal interpretations with respect to the correctness and explainability measures. We show that the underlying multi-objective optimization problem can be solved via a reduction to quantitative constraint solving, such as weighted maximum satisfiability. To demonstrate the benefits of our approach, we have applied it to synthesize interpretations for black-box neural-network classifiers. Our experiments show that there often exists a rich and varied set of choices for interpretations that are missed by existing approaches.

This working group is a follow-up of Antonio Casares’ session “Minimization of deterministic parity automata”. We studied the following functional problem:

input:

A deterministic transition-based (co)Büchi automaton $𝒜$.

output:

A deterministic transition-based (co)Büchi automaton which is equivalent to $𝒜$, and state-minimal.

Contrary to minimization of parity automata, we believe this problem to be polynomial-time computable. We mostly focused on a congruence-based approach.

We worked on understanding memory requirements in games with topologically open winning conditions. The question can be phrased as follows. Let $\mathrm{\Sigma }$ be an alphabet:

input:

$L$ a language of ${\mathrm{\Sigma }}^{\ast }$, say regular;

output:

minimal $k$ such that on any game graph with objective $L\subseteq {\mathrm{\Sigma }}^{\omega }$, if Eve wins then she wins with a $k$-states memory

We discussed a few examples and motivations and talked about the case where $L$ is a singleton which has a simple solution. We did not make substantial progress on the general case.

During this working session, we discussed the possibility of using graph neural networks (GNNs) to reduce the state space of automata used for synthesis from LTL specifications. The state of the art (in current LTL-synthesis solvers) concerns the syntactic recognition of subformulas that are treated with special transformations which may lead to minimal subautomata. Finally, the product of said automata is taken to obtain a final automaton. To further reduce the size of the final automaton, Spot /ltlsynt implements an approximation of an isomorphism check (rather, it resembles graded bisimulation). This option seems to be disabled by default as it takes too long. An alternative concerns guessing a bisimulation relation and checking (in logspace, using one step of the classical partition refinement algorithm for bisimulation) that it is indeed a bisimulation relation. This begs the question of whether machine learning can help us make such a guess.

On the GNN side, it was mentioned that they are a very hot topic in AI and that the main focus of current research concerns the proposal of new architectures to improve their “expressiveness”. GNNs can be seen as a “recolouring” function applied to a coloured graph. It is known that this recolouring function cannot colour nodes differently that the Weisfeiler-Leman (WL) algorithm would deem as equivalent. Conversely, for every coloured graph, there are weight matrices and bias vectors such that GNNs implement the WL algorithm. Guillermo A. Perez mentioned an unpublished result: GNNs can also implement the (coarsest) bisimulation relation.

Open questions:

1. 1.

   Can other relations of interest be implemented using different GNN architectures?

2. 2.

   To leverage GNNs in graphs that come from verification applications, one needs to obtain useful and meaningful features for the vertices. How can these be obtained easily or even automatically?

3. 3.

   For large graphs, recent works and libraries suggest sampling a number of neighbours of each node. Will this render GNNs useless for verification methods in large graphs?

Benchmark sets for existing and upcoming tracks of the reactive synthesis competition (SYNTCOMP) were discussed. The main points that were touched during the discussion can be summarized as follows.

1. 1.

   PDDL is a well-established family of languages in the planning community for describing tasks. In the short term, we can try to translate (non-deterministic) PDDL specifications to TLSF. In the long term, PDDL itself may become a reasonable format for some tracks, and we may further extend it with goals expressed in LTL over finite words.

2. 2.

   While reports of SYNTCOMP usually include graphs covering all benchmarks, it may be of more importance to highlight how well tools scale per parametric family of benchmarks as the parameter values increase. This is already present in the report for the 2018-2021 editions of the competition. A proposal is to include such graphs in the results of every forthcoming edition of the competition.

3. 3.

   PSL is a well-established extension of LTL that seems to be used in industry. We will survey the literature on PSL case studies and perhaps even approach IBM, Synopsys, and other companies to ask whether they have such specifications so that we can enrich the set of benchmarks.

4. 4.

   Regarding the output format of synthesis tools: The current one is quite succinct and it matches the input of model checking tools. Namely, SYNTCOMP requires output in AIGER format. However, semi-explicit representations such as HOA for Mealy/Moore machines may be easier to visualize. Hence, for future editions of the competition, an “explainable badge” will be awarded to tools that produce such semi- or fully explicit versions of their output (as an additional option, not as the official output for the competition).

5. 5.

   Finally, we noted that the parity game track is currently biased as it measures the time for parsing and minimization of the parity game together with the time it takes to actually solve the game. Instead, a proposal is to split this into preprocessing time and solving time. In the short term, tools will have to output a message and timestamp stating when preprocessing is finished so that we can split the two processes. In the long term, we can consider more succinct formats of a parity game to have parsing become faster (after using, perhaps, the BDD version of hoa-tools) and to be able to succinctly encode even larger games.

This talk is a teaser talk about a new SAT solver API – IPASIR-UP – that provides interactions with the solver during the solving process. Hence, instead of calling the solver incrementally, it is possible to interact with the solver during the solving process, i.e., whenever the solver makes a decision, propagates a variable, finds a conflict, finds a model, etc.

IPASIR-UP allows, among other things, implementing CEGAR approaches or theories quickly and cleanly. So far, this API is available in Cadical.

There has been a growing interest in the last few years in increasing the expressivity of reactive synthesis from propositional LTL into richer languages that can handle data. One impact-full line of research includes temporal stream logic (TSL) that has managed to synthesize sophisticated controllers. Another example was Raina Dimitrova’s work presented in this seminar. However, most attempts to increase the expressivity quickly render the realizability decision problem undecidable.

In the first part of this working session we discussed the recent work on realizability of “LTL modulo theory” that shows decidability of an extension of LTL where the propositions are replaced by literals from a first order theories. The Boolean abstraction method generates an equi-realizable propositional LTL specification as long as the first-order theory enjoys a decidable exists-forall (validity) decision problem. Moreover, the resulting specification remains in the same temporal class and is amenable of Boolean reactive synthesis. Then we discussed how the resulting (Boolean) controllers obtained using existing synthesis tools can be extended to “theory controllers”, thus obtaining a full LTL modulo theory synthesis algorithm.

However, current LTL modulo theory does not allow to transfer data across time (which is the main reason for undecidability of richer formalisms like TSL). We briefly discussed possibilities for enriching LTL modulo theories with controlled data transferred, particularly based on known decidability results from register automata. We concluded that a first promising approach should be based on specific characteristics of each theory and not (as for LTL modulo theories described above) agnostic to the theory in question.

In this working group, we discussed the following problem in reactive synthesis of Linear Temporal Logic on finite traces (LTLf):

Consider an autonomous system immersing in an environment, where there are multiple abstraction levels of how the environment behaves, depending on how much environment dynamics to be concerned:

• $\mathrm{■}$

  ${\text{Env}}_1$ (any possible env behaviours),

• $\mathrm{■}$

  ${\text{Env}}_2$,

• $\mathrm{■}$

  $\mathrm{\cdots }$

• $\mathrm{■}$

  ${\text{Env}}_m$ (most restricted env behaviours).

The system is given multiple tasks, ranging from most difficult to easiest:

• $\mathrm{■}$

  ${\text{Task}}_1$ (most difficult),

• $\mathrm{■}$

  ${\text{Task}}_2$,

• $\mathrm{■}$

  $\mathrm{\cdots }$

• $\mathrm{■}$

  ${\text{Task}}_n$ (easiest).

Question: How to achieve a good balance to achieve a more difficult task considering a more flexible environment?

We discussed different ways of dealing with this problem. A good direction might be looking at robust LTL [1]. Another interesting direction is MaxSAT or Weighted MaxSAT.