On Dependent Variables in Reactive Synthesis

TL;DR

This work introduces the notion of dependent variables in reactive LTL synthesis, defining when an output is uniquely determined by the history and other variables, and shows these dependencies are common in SYNTCOMP benchmarks. It presents an automata-based method to identify a subset-maximal dependent set $X$, projects these out to form $A'_\\varphi$, and synthesizes non-dependent outputs $O\\setminus X$ alongside a Boolean-functional-synthesis-based transducer for $X$, finally merging them into a complete strategy. Implemented as DepSynt atop Spot, the approach yields performance gains on benchmarks with few non-dependent outputs and demonstrates competitive results otherwise, suggesting a practical path to faster synthesis by exploiting dependencies. The results imply that integrating dependency-aware preprocessing can extend the reach of reactive synthesis techniques in realistic settings.

Abstract

Given a Linear Temporal Logic (LTL) formula over input and output variables, reactive synthesis requires us to design a deterministic Mealy machine that gives the values of outputs at every time step for every sequence of inputs, such that the LTL formula is satisfied. In this paper, we investigate the notion of dependent variables in the context of reactive synthesis. Inspired by successful pre-processing steps in Boolean functional synthesis, we define dependent variables as output variables that are uniquely assigned, given an assignment, to all other variables and the history so far. We describe an automata-based approach for finding a set of dependent variables. Using this, we show that dependent variables are surprisingly common in reactive synthesis benchmarks. Next, we develop a novel synthesis framework that exploits dependent variables to construct an overall synthesis solution. By implementing this framework using the widely used library Spot, we show that reactive synthesis using dependent variables can solve some problems beyond the reach of several existing techniques. Further, among benchmarks with dependent variables, if the number of non-dependent variables is low (at most 3 in our experiments), our method is able outperform all state-of-the-art tools for synthesis.

Figures (8)

• Figure 1: An Example NBA $A_1$
• Figure 2: Synthesis using dependencies
• Figure 3: Cumulative count of benchmarks for each unique value of Total Dependent Variables (left plot) and Dependency Ratio (right plot). The value of $F(x)$ on y-axis represents how many benchmarks have at most $x$ (on x-axis) dependent variables/dependency ratio.
• Figure 4: Cactus plot comparing DepSynt, LtlSynt, and Strix on 162 benchmarks with at most 3 non-dependent variables.
• Figure 5: Cactus plot comparing DepSynt, LtlSynt, and Strix on 138 benchmarks with more than 3 non-dependent variables.

Theorems & Definitions (18)

• theorem thmcountertheorem
• definition thmcounterdefinition: Variable Dependency in LTL
• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition
• theorem thmcountertheorem
• proof
• lemma thmcounterlemma
• corollary thmcountercorollary
• lemma thmcounterlemma