11institutetext:  Indian Institute of Technology Bombay, Mumbai, India
22institutetext: The Open University of Israel, Israel

# On Dependent Variables in Reactive Synthesis††thanks: This is the full
version of a conference paper published in TACAS 2024.

S. Akshay 11 Eliyahu Basa 22 Supratik Chakraborty 11 Dror Fried 22

###### 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 ($\leq 3$
in our experiments), our method is able outperform all state-of-the-art tools
for synthesis.

###### Keywords:

Reactive synthesis Functionally dependent variablesBDDs

##  1 Introduction

Reactive synthesis concerns the design of deterministic transducers (often
Mealy or Moore machines) that generate a sequence of outputs in response to a
sequence of inputs such that a given temporal logic specification is
satisfied. Ever since Church introduced the problem [11] in 1962, there has
been a rich and storied history of work in this area over the past six
decades. Recently, it was shown that a form of pre-processing, viz.
decomposing a Linear Temporal Logic (LTL) specification, can lead to
significant performance gains in downstream synthesis steps [14]. The general
idea of pre-processing a specification to simplify synthesis has also been
used very effectively in the context of Boolean functional synthesis [4, 23,
3, 16]. Motivated by the success of one such pre-processing step, viz.
identification of uniquely defined outputs, in Boolean functional synthesis,
we introduce the notion of dependent outputs in the context of reactive
synthesis in this paper. We develop its theory and show by means of extensive
experiments that dependent outputs abound in reactive synthesis benchmarks,
and can be effectively exploited to obtain synthesis techniques with
orthogonal strengths vis-a-vis existing state-of-the-art techniques.

In the context of propositional specifications, it is not uncommon for a
specification to uniquely define an output variable in terms of the input
variables and other output variables. A common example of this arises when
auxiliary variables, called Tseitin variables, are introduced to efficiently
convert a specification not in conjunctive normal form (CNF) to one that is in
CNF [26]. Being able to identify such uniquely defined variables efficiently
can be very helpful, whether it be for checking satisfiability, for model
counting or synthesis. This is because these variables do not alter the basic
structure or cardinality of the solution space of a specification regardless
of whether they are projected out or not. Hence, one can often simplify the
reasoning about the specification by ignoring (or projecting out) these
variables. In fact, the remarkable practical success of Boolean functional
synthesis tools such as Manthan [16] and BFSS [4, 3] can be partly attributed
to efficient techniques for identifying a large number of uniquely defined
variables. We draw inspiration from these works and embark on an investigation
into the role of uniquely defined variables, or _dependent variables_ , in the
context of reactive synthesis. To the best of our knowledge, this is the first
attempt at directly using dependent variables for reactive synthesis.

We start by first defining the notion of dependent variables in LTL
specifications for reactive synthesis. Specifically, given an LTL formula
$\varphi$ over a set of input variables $I$ and output variables $O$, a set of
variables $X\subseteq O$ is said to be _dependent_ on a set of variables
$Y\subseteq I\cup(O\backslash X)$ in $\varphi$, if at every step of every
infinite sequence of inputs and outputs satisfying $\varphi$, the finite
history of the sequence together with the current assignment for $Y$ uniquely
defines the current assignment for $X$. The above notion of dependency
generalizes the notion of uniquely defined variables in Boolean functional
synthesis, where the value of a uniquely defined output at any time is
completely determined by the values of inputs and (possibly other) outputs at
that time. We show that our generalization of dependency in the context of
reactive synthesis is useful enough to yield a synthesis procedure with
improved performance vis-a-vis competition winning tools, for a non-trivial
number of reactive synthesis benchmarks.

We present a novel automata-based technique for identifying a subset-maximal
set of dependent variables in an LTL specification $\varphi$. Specifically, we
convert $\varphi$ to a language-equivalent non-deterministic Büchi automaton
(NBA) $A_{\varphi}$, and then deploy efficient path-finding techniques to
identify a subset-maximal set of outputs $X$ that are dependent on
$Y=I\cup(O\setminus X)$. We implemented our method to determine the prevalence
of dependent variables in existing reactive synthesis benchmarks. Our finding
shows that out of 1141 benchmarks taken from the SYNTCOMP [19] competition,
300 had at least one dependent output variable and 26 had all output variables
dependent.

Once a subset-maximal set, say $X$, of dependent variables is identified, we
proceed with the synthesis process as follows. Referring to the NBA
$A_{\varphi}$ alluded to above, we first transform it to an NBA
$A_{\varphi}^{\prime}$ that accepts the language $L^{\prime}$ obtained from
$L(\varphi)$ after removing (or projecting out) the $X$ variables. Our
experiments show that $A_{\varphi}^{\prime}$ is more compactly representable
compared to $A_{\varphi}$, when using BDD-based representations of transitions
(as is done in state-of-the-art tools like Spot [6]). Viewing
$A_{\varphi}^{\prime}$ as a new (automata-based) specification with output
variables $O\setminus X$, we now synthesize a transducer $T_{Y}$ from
$A^{\prime}$ using standard reactive synthesis techniques. This gives us a
strategy $f^{Y}:\Sigma_{I}^{*}\rightarrow\Sigma_{O\backslash X}$ for each non-
dependent variable in $O\setminus X$. Next, we use a novel technique based on
Boolean functional synthesis to directly construct a circuit that implements a
transducer $T_{X}$ that gives a strategy
$f_{X}:\Sigma_{Y}^{*}\rightarrow\Sigma_{X}$ for the dependent variables.
Significantly, this circuit can be constructed in time polynomial in the size
of the (BDD-based) representation of $A_{\varphi}$. The transducers $T_{Y}$
and $T_{X}$ are finally merged to yield an overall transducer $T$ that
describes a strategy $f:\Sigma_{I}^{*}\rightarrow\Sigma_{O}$ solving the
synthesis problem for $\varphi$.

We implemented our approach in a tool called DepSynt. Our tool was developed
in C++ using APIs from the widely used library Spot for representing and
manipulating non-deterministic Büchi automata. We performed a comparative
analysis of our tool with winning entries of the SYNTCOMP [19] competition to
evaluate how knowledge of dependent variables helps reactive synthesis. Our
experimental results show that identifying and utilizing dependent variables
results in improved synthesis performance when the count of non-dependent
variables is low. Specifically, our tool outperforms state-of-the-art and
highly optimized synthesis tools on benchmarks that have at least one
dependent variable and at most 3 non-dependent variables. This leads us to
hypothesize that exploiting dependent variables benefits synthesis when the
count of non-dependent variables is below a threshold. Given the preliminary
and un-optimized nature of our implementation, we believe there is significant
scope for improvement of our results.

##### Related work

Reactive Synthesis has been an extremely active research area for the last
several decades (see e.g. [11, 22, 8, 15, 14]). Not only is the theoretical
investigation of the problem rich, there are also several tools that are
available to solve synthesis problems in practice. These include solutions
like ltlsynt [21] based on Spot [6], Strix [20] and BoSY [13]. Our tool relies
heavily on Spot and its APIs, which we use liberally to manipulate non-
deterministic Büchi automata. Our synthesis approach is based on the standard
conversion of the converted NBA to a deterministic parity automata (DPA) (see
[7] for an overview of the challenges of reactive synthesis).

Our work may be viewed as lifting the idea of uniquely defined variables in
Boolean functional synthesis to the context of reactive synthesis. Viewed from
this perspective, our work is not the first to lift ideas from Boolean
functional Synthesis. Following a framework called ”back-and-forth” for
Boolean functional synthesis that uses a decomposition of a specification into
separate formulas on input variables and on output variables [10], the work in
[5] constructed a reactive synthesis tool for specific benchmarks that admit a
separation of the specification into formulas for only the environment
variables and formulas for only the system variables. In this sense, this
current work of ours is another step in bridging the gap between the Boolean
functional synthesis and the reactive synthesis communities.

The remainder of the paper is structured as follows. We introduce definitions
and notations in Section 2. In Section 3 we define dependent variables for LTL
formulas, and describe our framework to find it. In Section 4 we describe our
automata-based synthesis framework and discuss some of its implementation
details in Section 5. We describe our evaluation in Section 6 and conclude in
Section 7.

##  2 Preliminaries

Given a finite alphabet $\Sigma$, an infinite _word_ $w$ is a sequence
$w_{0}w_{1}w_{2}\cdots$ where for every $i$, the $i^{th}$ letter of $w$,
$w_{i}\in\Sigma$. The _prefix_ $w_{0}\cdots w_{i}$ of size $i+1$ of $w$ is
denoted by $w[0,i]$. Then $w[0,0]=w_{0}$. We denote $w[0,-1]$ to be the empty
word. The set of all infinite words over $\Sigma$ is denoted by
$\Sigma^{\omega}$. We call $L\subseteq\Sigma^{\omega}$ a _language_ over
infinite words in $\omega$. When the alphabet $\Sigma$ is combined from two
distinct alphabets, $\Sigma=\Sigma_{X}\times\Sigma_{Y}$ for some sets of
variables $X,Y$, we abuse notation and for a letter
$a=(a_{1},a_{2})\in\Sigma$, denote by $a.X$ the projection of $a$ on
$\Sigma_{X}$, that is, the letter $a_{1}\in\Sigma_{X}$. Similarly, $a.Y$
denotes the projection of $a$ on $\Sigma_{Y}$, that is the letter
$a_{2}\in\Sigma_{Y}$. We define by $w.X$ the word obtained from a word
$w\in\Sigma$ on $\Sigma_{X}$ i.e. $w.X=w_{0}.X\cdots$.

##### Linear Temporal Logic.

A Linear Temporal Logic (LTL) formula is constructed with a finite set of
propositional variables $V$, using Boolean operators such as $\vee,\wedge,$
and $\neg,$ and temporal operators such as next $X$, until $U$, etc. The set
$V$ induces an alphabet $\Sigma_{V}=2^{V}$ of all possible assignments
($true/false$) to the variables of $V$. The language of an LTL formula
$\varphi$, denoted $L(\varphi)$ is the set of all words in
$\Sigma_{V}^{\omega}$. The semantics of the operators and satisfiability
relation is defined as usual [18]. We denote the number of variables $V$ by
$|V|$, and size of formula $\varphi$, i.e., number of its subformulas by
$|\varphi|$. We sometimes abuse notation and identify the singleton set of a
variable $\\{z\\}$ with the variable $z$, and denote $E_{V}$ by $E$ when $V$
is clear from the context.

##### Nondeterministic Büchi Automata.

A Nondeterministic Büchi Automaton (NBA) is a tuple
$A=(\Sigma,Q,\delta,q_{0},F)$ where $\Sigma$ is the alphabet, $Q$ is a finite
set of states, $\delta:Q\times\Sigma\rightarrow 2^{Q}$ is a non-deterministic
transition function, $q_{0}$ is the initial state and $F\subseteq Q$ is a set
of accepting states. $A$ can be seen as a directed labeled graph with vertices
$Q$ and an edge $(q,q^{\prime})$ exists with a label $a$ if
$q^{\prime}\in\delta(q,a)$. We denote the set of incoming edges to $q$ by
$in(q)$ and the set of outgoing edges from $q$ by $out(q)$. A _path_ in $A$ is
then a (possibly infinite) sequence of states
$\rho=(q_{i_{0}},q_{i_{1}},\cdots)$ in which for every $j>0$,
$(q_{i_{j}},q_{i_{j+1}})$ is an edge in $A$. A _run_ is a path that starts in
$q_{0}$, and is _accepting_ if it visits a state in $F$ infinitely often. A
_word_ of the run $\rho$ is the sequence of labels seen along $\rho$, i.e.,
$w=\sigma_{i_{0}}\sigma_{i_{1}}\cdots$ where for every $j\geq 0$,
$q_{i_{j+1}}\in\delta(q_{i_{j}},\sigma_{i_{j}})$. As $A$ is nondeterministic a
word can have many runs, although every run has a single word. A word is
_accepting_ if it has an accepting run in $A$. The language $L(A)$ is the set
of all accepting words in $A$. Wlog, we assume that all states and edges that
are not a part of an accepting run are removed. Finally, every LTL formula
$\varphi$ can be transformed in exponential time in the length of $\varphi$,
to an NBA $A_{\varphi}$ for which $L(\varphi)=L(A_{\varphi})$ [27, 18]. When
$\varphi$ is clear from the context we omit the subscript and refer to
$A_{\varphi}$ as $A$. We denote by $|A|$ the size of an automaton, i.e., its
number of states and transitions.

##### Reactive Synthesis.

A _reactive LTL formula_ is an LTL formula $\varphi$ over a set of input
variables $I$ and output variables $O$, with $I\cap O=\emptyset$. In _reactive
synthesis_ we are given a reactive LTL formula $\varphi$, and the challenge is
to synthesize a function, called _strategy_ ,
$f:\Sigma_{I}^{*}\rightarrow\Sigma_{O}$ such that every word
$w\in(\Sigma_{I}\times\Sigma_{O})^{\omega}$ obtained by using this strategy is
in $L(\varphi)$. If such a strategy exists we say that $\varphi$ is
_realizable_. Otherwise, we say that $\varphi$ is _unrealizable_. In what
follows, we always consider only reactive LTL formulas and hence often omit
the prefix reactive while referring to them. The synthesized strategy
$f:\Sigma_{I}^{*}\rightarrow\Sigma_{O}$ that is given as output is typically
described (explicitly or symbolically) in a form of a _transducer_
$T=(\Sigma_{I},\Sigma_{O},S,s_{0},\delta,\lambda)$ in which $\Sigma_{I}$ and
$\Sigma_{O}$ are input and output alphabet respectively, $S$ is a set of
states with an initial state $s_{0}$, $\delta:S\times\Sigma_{I}\rightarrow S$
is a deterministic transition function, and
$\lambda:S\times\Sigma_{I}\rightarrow\Sigma_{O}$ is the output function. A
standard procedure in solving reactive synthesis is to transform the given LTL
formula $\varphi$ to an NBA $A_{\varphi}$ for which
$L(A_{\varphi})=L(\varphi)$. Then transform $A_{\varphi}$ to a Deterministic
Parity Automata (DPA) that turns to a parity game, which solution is described
as a transducer $T_{A_{\varphi}}$. It is known that this approach cannot
escape exponential blowups. More precisely,

###### Theorem 2.1

  1. 1.

Reactive synthesis can be solved in $O(2^{n\cdot 2^{n}})$, where $n$ is the
size of the LTL formula.

  2. 2.

Given an NBA $A$ with $n$ states, computing transducer $T_{A}$ takes
$\Omega(2^{n\log n})$.

##  3 Dependent variables in reactive LTL

In this section, we define dependent variables for (reactive) LTL formulas and
suggest a framework for finding a maximal set of dependent variables. Our
notion of dependent variables for LTL formulas, specifically suited to
reactive synthesis, asks that the dependency be maintained at every step of
the word satisfying the formula. While there are several notions of dependency
that can be considered, we describe the one that we use throughout the paper.
As mentioned earlier, our definition of dependency is restricted to output
variables, since having dependent input variables would imply that not all
input values are possible for these variables, which makes the formula
unrealizable.

######  Definition 1 (Variable Dependency in LTL)

Let $\varphi$ be an LTL formula over $V$ with input variables $I\subseteq V$
and output variables $O=V\backslash I$. Let $X,Y$ be sets of variables where
$X\subseteq O$. We say that $X$ is dependent on $Y$ in $\varphi$ if for every
pair of words $w,w^{\prime}\in L(\varphi)$ and $i\geq 0$ if
$w[0,i-1]=w^{\prime}[0,i-1]$ and $w_{i}.Y=w^{\prime}_{i}.Y$, then we have
$w_{i}.X=w^{\prime}_{i}.X$. Further, we say that $X$ is dependent in $\varphi$
if $X$ is dependent on $V\setminus{X}$ in $\varphi$, i.e., it is dependent on
all the remaining variables.

Note that two words in $L(\varphi)$ with different prefixes can still have
different values for $X$ for the same values for $Y$, and $X$ can still be
defined dependent on $Y$.

As an example, consider an LTL formula $\varphi$ with an input variable $y$,
an output variable $x$ and a language $L=\\{w^{1},w^{2},w^{3}\\}$ where
$w^{1}=(y,x)^{\omega}$, $w^{2}=(\neg y,x)^{\omega}$ and $w^{3}=(y,x)(\neg
y,x)(y,\neg x)^{\omega}$. Then $x$ is dependent on $y$ in $\varphi$.
Specifically note that $w^{1}[0,1]\neq w^{3}[0,1]$ and thus the dependency of
$x$ is not violated, although $w^{1}_{2}.y=w^{3}_{2}.y$ and
$w^{1}_{2}.x\not=w^{3}_{2}.x$. Observe that, if $X$ is dependent on $Y$ in
$\varphi$ for some $Y$, then it is also dependent in $\varphi$. We next show
how to find a maximal set of dependent variables.

###  3.1 Maximally dependent sets of variables

###### Definition 2

Given an LTL formula $\varphi(I,O)$, we say that a set $X\subseteq O$ is a
_maximal dependent set_ in $\varphi$ if $X$ is dependent in $\varphi$ and
every set that strictly contains $X$ is not dependent in $\varphi$.

As in the propositional case [25], finding maximum or minimum dependent sets
is intractable, hence we focus on subset-maximality. Given a variable $z$ and
set $Y$, checking whether $z$ is dependent on $Y$, can easily be used to
finding a maximal dependent set. Indeed, we would just need to start from the
empty set and iterate over output variables, checking for each if it is
dependent on the remaining variables. For completeness, we give the pseudocode
for this in Appendix 0.A.

Note that when all output variables are not dependent, the order in which
output variables are chosen may play a significant role in the size of the
maximal set obtained. We currently use a naive ordering (first appearance),
and leave the problem of better heuristics for getting larger maximal
independent sets to future work.

###  3.2 Finding dependent variables via automata

As explained above, the heart of the dependency check is to check if a given
output variable is dependent on a set of variables. We now develop an approach
for doing so based on the nondeterministic Büchi automaton $A_{\varphi}$ of
the original LTL formula $\varphi$. Our framework uses the notion of
compatible pairs of states of the automaton defined as follows.

###### Definition 3

Let $A=(\Sigma,Q,\delta,q_{0},F)$ be an NBA with states $s,s^{\prime}$ in $Q$.
Then the pair $(s,s^{\prime})$ is _compatible_ in $A$ if there are runs from
$q_{0}$ to $s$ and from $q_{0}$ to $s^{\prime}$ with the same word
$w\in\Sigma^{*}$.

Recall that in our definition, only states and edges that are part of an
accepting run exist in $A$. Then we have the following definition.

###### Definition 4

Let $\varphi$ be an LTL formula over $V$ with input variables $I\subseteq V$
and output variables $O=V\backslash I$. Let $X,Y$ be sets of variables where
$X\subseteq O$. Let $A_{\varphi}$ be an NBA that describes $\varphi$. We say
that $X$ is _automata dependent_ on $Y$ in $A_{\varphi}$, if for every pair of
compatible states $s,s^{\prime}$ and assignments $\sigma$, $\sigma^{\prime}$
for $V$, where $\sigma.Y=\sigma^{\prime}.Y$ and
$\sigma.X\neq\sigma^{\prime}.X$, $\delta(s,\sigma)$ and
$\delta(s,\sigma^{\prime})$ cannot both exist in $A_{\varphi}$. We say that
$X$ is automata dependent in $A_{\varphi}$ if $X$ is automata dependent on $Y$
in $A_{\varphi}$ and $Y=V\backslash X$.

$q_{0}$$q_{1}$0,110,001,111,100,110,001,110,00 Figure 1: An Example NBA
$A_{1}$

As an example, consider NBA $A_{1}$ from adjoining Figure 1, constructed from
some LTL formula with input $I=\\{i\\}$ and outputs $O=\\{o_{1},o_{2}\\}$.
Here $\Sigma_{I}=\\{0,1\\},\Sigma_{O}=\\{0,1\\}^{2}$ and edges are labeled by
values of $(i,o_{1}o_{2})$. It is immediate that,
$(q_{0},q_{0}),(q_{1},q_{1})$ are compatible pairs but so are
$(q_{0},q_{1}),(q_{1},q_{0})$ since they can both be reached from the initial
state on reading the length $2$ word $(0,00)(0,00)$. Now consider output
$o_{1}$. It is not dependent on $\\{i\\}$, i.e., only the input, since from
$q_{0}$ with $i=0$, we can go to different states with different values of
$o_{1}$. But $o_{1}$ is indeed dependent on $\\{i,o_{2}\\}$. To see this
consider every pair of compatible states – in this case all pairs. Then we can
see that if we fix the values of $i$ and $o_{2}$, there is a unique value of
$o_{1}$ that permits state transitions to happen from the compatible pair. For
example, regardless of which state we are in, if $i=0,o_{2}=0$, $o_{1}$ must
be $0$ for a state transition to happen. On the other hand, $o_{2}$ is not
dependent on either $\\{i\\}$ or $\\{i,o_{1}\\}$ (as can be seen from
$(q_{0},q_{1})$ with $i=1,o_{1}=1$).

The following shows us the relation between automata dependency and dependency
in LTL as defined earlier.

###### Theorem 3.1

Let $\varphi$ be an LTL formula with $V=I\cup O$ variables, where $X\subseteq
O$ and $Y\subseteq I\cup O$. Let $A_{\varphi}$ be an NBA that describes
$\varphi$. Then $X$ is dependent on $Y$ in $\varphi$ if and only if $X$ is
automata dependent on $Y$ in $A_{\varphi}$.

###### Proof

Assume that $X$ is dependent in $\varphi$ and let $s,s’$ be two compatible
states in $A$ with a joint history $w^{*}$. Assume for contradiction that
there is an assignment $y$ for $Y$, for which there are distinct assignments
$x,x’$ for $X$ for which both $\delta(s,xy)$ exists and $\delta(s’,x’y)$
exist. Then this means that $\delta(s,xy)$ and $\delta(s’,x’y)$ both continue
to some accepting runs $r,r$ respectively in $A$. Let $w$ be the label of the
$r$ and $w’$ the label of $r’$. Then $w,w’$ are in $L(\varphi)$ with a prefix
$w^{*}$, but $x=w_{i}.x\neg=w’_{i}.x=x’$ contradicting $X$ being relaxed
dependent in $\varphi$.

Next, assume that $X$ is automata dependent on $Y$ in $A_{\varphi}$. Let
$w,w^{\prime}$ be two words in $L(\varphi)$, and thus in $L(A_{\varphi})$.
Assume that there is $i\geq 0$ for which $u=w[0,i]=w^{\prime}[0,i]$. Let
$r,r^{\prime}$ be accepting runs of $w,w^{\prime}$ respectively and let
$s_{1},s_{2}$ be the states respectively in the run $r,r^{\prime}$ that has
the same history $w[0,i-1]$. Note that this makes $s_{1},s_{2}$ compatible.
Next assume $e_{1}=(s_{1},s_{1}^{\prime})$ with a label $\sigma_{1}$ is on $r$
, and $e_{2}=(s_{2},s_{2}^{\prime})$ with a label $\sigma_{2}$ is on
$r^{\prime}$. Further, assume $\sigma_{1}.y=\sigma_{2}.y$. Note that it means
that $w_{i+1}.Y=w^{\prime}_{i+1}.Y$. Then since $X$ is automata dependent in
$Y$, we have that $\sigma_{1}.X=\sigma_{2}.X$ as well, hence
$w_{i+1}.X=w^{\prime}_{i+1}.X$.∎

Thus, we can focus on algorithms for finding automata dependency. We start by
describing how to find compatible states.

##### Finding Compatible States

We find all compatible states in an automaton in Algorithm 1 as follows. We
maintain a list of in-process compatible pairs $C$ to which we start by adding
the initial pair $(q_{0},q_{0})$, which is of course compatible. At each step,
until $C$ becomes empty, for each pair $(s_{i},q_{j})\in C$, we add it to the
compatible pair set $P$, and remove it from $C$ (in line 4). Then (in lines
5-8), we check (in line 6) if outgoing transitions from $(s_{i},s_{j})$ lead
to a new pair $(s^{\prime}_{i},s^{\prime}_{j})$ not already in $P$ or $C$,
which can be reached on reading the same letter $\sigma$ and if so, we add
this pair to the in-process set $C$. All pairs that we put in $P,C$ are indeed
compatible, nothing is removed from $P$. And when the algorithm terminates,
$C$ is empty, which means all possible ways (from initial state pair) to reach
a possible compatible pair have been explored, thus showing correctness.

Algorithm 1 Find All Compatible States in NBA

Input NBA $A_{\varphi}=(\Sigma,Q,\delta,q_{0},F)$ of $\varphi$.
Output Set $P\subseteq Q\times Q$ of all compatible state pairs in
$A_{\varphi}$

1:$P\leftarrow\emptyset$; $C\leftarrow\\{(q_{0},q_{0})\\}$

2:while $C\neq\emptyset$ do

3: Let $(s_{i},s_{j})\in C$

4: $P\leftarrow P\cup\\{(s_{i},s_{j})\\}$; $C\leftarrow
C\setminus\\{(s_{i},s_{j})\\}$

5: for $(s_{i}^{\prime},s_{j}^{\prime})\in out(s_{1})\times out(s_{2})$ do

6: if $(s_{i}^{\prime},s_{j}^{\prime})\notin P\cup C$ and $\exists\sigma\in
2^{\Sigma}$ s.t. $s_{i}^{\prime}\in\delta(s_{i},\sigma)\wedge
s_{j}^{\prime}\in\delta(s_{j},\sigma)$ then

7: $C\leftarrow C\cup\\{(s_{i}^{\prime},s_{j}^{\prime})\\}$

8: end if

9: end for

10:end while

11:return $P$

Finally, we show how to check dependency using automata, by implementing the
following procedure isAutomataDependent, described in Algorithm 2.
isAutomataDependent works by trying to find a witness to $\\{z\\}$ being _not_
dependent on $Y$. If no such witness exists then it means that $\\{z\\}$ is
dependent on $Y$. Given a variable $x$ and a set
$Y=V\backslash\\{z\\}$,isAutomataDependent first uses Algorithm 1 to construct
a list $P$ of all compatible pairs in $A$ (line 4). Then for every pair
$(s,s^{\prime})\in P$ the algorithm checks through the procedure
AreStatesColliding (lines 1-2) whether there exists an assignment
$\sigma,\sigma^{\prime}$ for which both $\delta(s,\sigma)$ and
$\delta(s^{\prime},\sigma^{\prime})$ exist, $\sigma.Y=\sigma^{\prime}.Y$ and
$\sigma.\\{z\\}\neq\sigma^{\prime}.\\{z\\}$. If so, then the algorithm returns
_false_ : $\\{z\\}$ is not dependent on $Y$ (line 7). At the end of checking
all the pairs, the algorithm returns _true_.

Algorithm 2 Check Dependency Based Automaton

Input NBA $A_{\varphi}=(\Sigma,Q,\delta,q_{0},F)$ from $\varphi$, Candidate
dependent variable $\\{z\\}$, Candidate dependency set $Y$.
Output Is $\\{z\\}$ dependent on $Y$ by Definition 4

1:procedure AreStateColliding($p,q$)

2: return $\exists\sigma_{p},\sigma_{q}\in 2^{\Sigma}$ s.t.
$\delta(p,\sigma_{p})\neq\emptyset\wedge\delta(q,\sigma_{q})\neq\emptyset\wedge\sigma_{p}.Y=\sigma_{q}.Y\wedge\sigma_{p}.\\{z\\}\neq\sigma_{q}.\\{z\\}$

3:end procedure

4:$P\leftarrow FindAllCompatibleStates(A_{\varphi})$

5:for $(s_{1},s_{2})\in P$ do

6: if $AreStateColliding(s_{1},s_{2})$ then

7: return False

8: end if

9:end for

10:return True

###### Lemma 1

Algorithm 2 returns _True_ if and only if $\\{z\\}$ is automata-dependent on
$V\backslash\\{z\\}$ in $A_{\varphi}$.

Thus using the above algorithm to perform dependency check we can compute
maximal sets of dependent variables (as explained earlier), which we will use
next to improve synthesis. Note that all the above algorithms run in time
polynomial (in fact, quadratic) in size of the NBA.

###### Corollary 1

Given NBA $A_{\varphi}$, computing compatible pairs, checking dependency,
building maximal dependent sets can be done in time polynomial in the size of
$A_{\varphi}$.

Note that if all output variables are dependent, then regardless of the order
in which the outputs are considered, for every finite history of inputs, there
is a unique value for each output that can cause the specification to be
satisfied. Therefore, there is a unique winning strategy for the
specification, assuming it is realizable.

##  4 Exploiting Dependency in Reactive Synthesis

$\varphi$1\. LTL to NBA$A_{\varphi}$2\. Identify Dep3\. $Proj_{dep}$4\. Syn-
Nondep $T_{Y}$5\. Syn-Dep $T_{X}$6\. Syn-Comb
$T$$f$$A_{\varphi},X,Y$$A^{\prime}_{\varphi},Y$$A_{\varphi},X$$f_{Y}$$f_{X}$

Figure 2: Synthesis using dependencies

In this section, we explain how dependencies can be beneficially exploited in
a reactive synthesis pipeline. Our approach can be described at a high level
as shown in Figure 2. This flow-chart has the following 6 steps:

  1. 1.

Given an LTL formula $\varphi$ over a set of variables $V$ with input
variables $I\subseteq V$ and output variables $O=V\backslash I$, we first
construct a language-equivalent NBA
$A_{\varphi}=(\Sigma_{I}\cup\Sigma_{O},S,s_{0},\delta,F)$ by standard means,
e.g [27].

  2. 2.

Then, as described in Section 3, we find in $A_{\varphi}$ a maximal set of
output variables $X$ that are dependent in $\varphi$. For notational
convenience, in the remainder of the discussion, we use $Y$ for
$I\cup(O\backslash X)$ and $\Sigma_{Y}$ for
$\Sigma_{I}\times\Sigma_{O\setminus X}$.

  3. 3.

Next, we construct an NBA $A^{\prime}_{\varphi}$ from $A_{\varphi}$ by
projecting out (or eliminating) all $X$ variables from labels of transitions.
Thus, $A_{\varphi}^{\prime}$ has the same sets of states and transitions as
$A_{\varphi}$. We simply remove valuations of variables in $X$ from the label
of every state transition in $A_{\varphi}$ to obtain $A_{\varphi}^{\prime}$.
Note that after this step, $L(A_{\varphi}^{\prime})=\\{w\mid\exists u\in
L(A_{\varphi})\mbox{ s.t. }w=u.Y\\}\subseteq\Sigma_{Y}^{\omega}$.

  4. 4.

Treating $A^{\prime}_{\varphi}$ as a (automata-based) specification with
inputs $I$ and outputs $O\setminus X$, we next use existing reactive synthesis
techniques (e.g., [7]) to obtain a transducer $T_{Y}$ that describes a
strategy $f_{Y}:\Sigma_{I}^{*}\rightarrow\Sigma_{O\backslash X}$ for
$L(A^{\prime}_{\varphi})$.

  5. 5.

We also construct a transducer $T_{X}$ that describes a function
$f_{X}:(\Sigma_{Y}^{*}\rightarrow\Sigma_{X})$ with the following property: for
every word $w^{\prime}\in L(A^{\prime}_{\varphi})$ there exists a unique word
$w\in L(\varphi)$ such that $w.Y=w^{\prime}$ and for all $i$,
$w_{i}.X=f_{X}(w^{\prime}[0,i])$.

  6. 6.

Finally, we compose $T_{X}$ and $T_{Y}$ to construct a transducer $T$ that
defines the final strategy $f:\Sigma_{I}^{*}\rightarrow\Sigma_{O}$. Recall
that transducer $T_{Y}$ has $I$ as inputs and $O\setminus X$ as outputs, while
transducer $T_{X}$ has $I$ and $O\setminus X$ as inputs and $X$ as outputs.
Composing $T_{X}$ and $T_{Y}$ is done by simply connecting the outputs
$O\setminus X$ of $T_{Y}$ to the corresponding inputs of $T_{X}$.

In the above synthesis flow, we use standard techniques from the literature
for Steps 1 and 4, as explained above. Hence we do not dwell on these steps in
detail. Step 2 was already described in detail in Section 3. Step 3 is easy
when we have an explicit representation of the automata. As we will discuss in
the next section, it has interesting consequences when we use symbolic
representations of automata. Step 6, as explained above, is also easy to
implement. Hence, in the remainder of this section, we focus on Step 5, which
is also a key contribution of this paper. In the next section, we will discuss
how steps 2, 3 and 5 are implemented using symbolic representations (viz.
ROBDDs).

####  4.0.1 Constructing transducer $T_{X}$

Let $A=(\Sigma_{I}\times\Sigma_{O},Q,\delta,q_{0},F)$ be the NBA $A_{\varphi}$
obtained in step 1 of the pipeline shown above. Since each letter in
$\Sigma_{O}$ can be thought of as a pair $(\sigma,\sigma^{\prime})$, where
$\sigma\in\Sigma_{O\setminus X}$ and $\sigma^{\prime}\in\Sigma_{X}$, the
transition function $\delta$ can be viewed as a map from
$Q\times(\Sigma_{I}\times\Sigma_{O\setminus X}\times\Sigma_{X})$ to $2^{Q}$.
The transducer $T_{X}$ we wish to construct is a deterministic Mealy machine
described by the $6$-tuple
$(\Sigma_{Y},\Sigma_{X}\cup\\{\bot\\},Q^{X},q^{X}_{0},\delta^{X},\lambda^{X})$,
where $\Sigma_{Y}=\Sigma_{I}\times\Sigma_{(O\setminus X)}$ is the input
alphabet, $\Sigma_{X}$ is the output alphabet with $\bot\not\in\Sigma_{X}$
being a special symbol that is output when no symbol of $\Sigma_{X}$ suffices,
$Q^{X}=2^{Q}$, that is the powerset of $Q$ is the set of states of $T_{X}$,
$q_{0}^{X}=\\{q_{0}\\}$ is the initial state,
$\delta^{X}:Q^{X}\times\Sigma_{I}\times\Sigma_{(O\setminus X)}\rightarrow
Q^{X}$ is the state transition function, and
$\lambda^{X}:Q^{X}\times\Sigma_{I}\times\Sigma_{(O\setminus
X)}\rightarrow\Sigma_{X}$ is the output function. The state transition
function $\delta^{X}$ is defined by the Rabin-Scott subset construction
applied to the automaton $A_{\varphi}$ [17]. Formally, for every $U\subseteq
Q$, $\sigma_{I}\in\Sigma_{I}$ and $\sigma\in\Sigma_{(O\setminus X)}$, we
define $\delta^{X}\big{(}U,(\sigma_{I},\sigma)\big{)}=\\{q^{\prime}\mid
q^{\prime}\in Q,\,\exists q\in U$ and $\exists\sigma^{\prime}\in\Sigma_{X}$
s.t.
$q^{\prime}\in\delta\big{(}q,(\sigma_{I},\sigma,\sigma^{\prime})\big{)}\\}$.
Before defining the output function $\lambda^{X}$, we state an important
property of $T^{X}$ that follows from the definition of $\delta^{X}$ above.

###### Lemma 2

If $X$ is automata dependent in $A_{\varphi}$, then every state $U$ reachable
from $q^{X}_{0}$ in $T_{X}$ satisfies the property: $\forall q,q^{\prime}\in
U$, $(q,q^{\prime})$ is compatible in $A_{\varphi}$.

###### Proof

We prove by induction on the number of steps, say $k$, needed to reach a state
$U$ from $q^{X}_{0}$ in $T_{X}$. The base case follows from the fact that
$q^{X}_{0}$ is a singleton set, and every singleton set trivially satisfies
the desired property. Therefore the claim holds for $k=0$.

Suppose the claim holds for all states $U$ reachable from $q^{X}_{0}$ in $k$
or fewer steps, for $k\geq 0$. Hence, $(q,q^{\prime})$ is compatible in
$A_{\varphi}$ for all $q,q^{\prime}\in U$. We wish to prove that if
$U^{\prime}=\delta^{X}\big{(}U,(\sigma_{I},\sigma)\big{)}$ for any
$(\sigma_{I},\sigma)\in\Sigma_{I}\times\Sigma_{O\setminus X}$, then
$(s,s^{\prime})$ is also compatible in $A_{\varphi}$ for every
$s,s^{\prime}\in U^{\prime}$.

Since $X$ is automata dependent in $A_{\varphi}$, it follows from Definition 4
that for every $(q,q^{\prime})\in U\times U$, if
$\delta\big{(}q,(\sigma_{I},\sigma,\sigma_{X})\big{)}\neq\emptyset$ and
$\delta\big{(}q^{\prime},(\sigma_{I},\sigma,\sigma_{X}^{\prime})\big{)}\neq\emptyset$
for some $\sigma_{X},\sigma_{X}^{\prime}\in\Sigma_{X}$, then
$\sigma_{X}=\sigma_{X}^{\prime}$. From the definition of $\delta^{X}$, it now
follows that if $U^{\prime}=\delta^{X}\big{(}U,(\sigma_{I},\sigma)\big{)}$ and
if $U^{\prime}\neq\emptyset$, then there exists a unique
$\sigma_{X}\in\Sigma_{X}$ s.t. $U^{\prime}=\\{q^{\prime}\mid\exists q\in
U\mbox{ s.t.
}q^{\prime}\in\delta\big{(}q,(\sigma_{I},\sigma,\sigma_{X})\big{)}\\}$. This
shows that for every $s,s^{\prime}\in U^{\prime}$, the pair $(s,s^{\prime})$
is compatible in $A_{\varphi}$.∎

We are now ready to define the output function $\lambda^{X}$ of $T_{X}$. Let
$U$ be a state reachable from $q^{X}_{0}$ in $T_{X}$ and let
$U^{\prime}=\delta^{X}\big{(}U,(\sigma_{I},\sigma)\big{)}$, where
$(\sigma_{I},\sigma)\in\Sigma_{Y}$. If $U^{\prime}\neq\emptyset$, we know from
the proof of Lemma 2 that there is a unique $\sigma_{X}\in\Sigma_{X}$ s.t.
$U^{\prime}=\\{q^{\prime}\mid\exists q\in U\mbox{ s.t.
}q^{\prime}\in\delta\big{(}q,(\sigma_{I},\sigma,\sigma_{X})\big{)}\\}$. We
define $\lambda^{X}\big{(}U,(\sigma_{I},\sigma)\big{)}=\sigma_{X}$ in this
case. If, on the other hand, $U^{\prime}=\emptyset$, we define
$\lambda^{X}\big{(}U,(\sigma_{I},\sigma)\big{)}=\bot$.

###### Theorem 4.1

If $\varphi$ is realizable, the transducer $T$ obtained by composing $T_{X}$
and $T_{Y}$ as in step 6 of Fig. 2 solves the synthesis problem for $\varphi$.

An interesting corollary of the above result is that for realizable
specifications with all output variables dependent, we can solve the synthesis
problem in time $O(2^{k})$ instead of $\Omega(2^{k\log k})$, where
$k=|A_{\varphi}|$. This is because the subset construction on $A_{\varphi}$
suffices to obtain $T_{X}$, while $A_{\varphi}$ must be converted to a
deterministic parity automaton to solve the synthesis problem in general.

##  5 Symbolic Implementation

In this section, we describe symbolic implementations of each of the non-
shaded blocks in the synthesis flow depicted in Fig. 2. Before we delve into
the details, a note on the representation of NBAs is relevant. We use the same
representation as used in Spot [6] – a state-of-the-art platform for
representing and manipulating LTL formulas and $\omega$-automata.
Specifically, the transition structure of an NBA $A$ is represented as a
directed graph, with nodes representing states of $A$, and directed edges
representing state transitions. Furthermore, every edge from state $s$ to
state $s^{\prime}$ is labeled by a Boolean function $B_{(s,s^{\prime})}$ over
$I\cup O$. The Boolean function can itself be represented in several forms. We
assume it is represented as a Reduced Ordered Binary Decision Diagram (ROBDD)
[9], as is done in Spot. Each such labeled edge represents a set of state
transitions from $s$ to $s^{\prime}$, with one transition for each satisfying
assignment of $B_{(s,s^{\prime})}$.

##### Implementing Algorithms 1 and 2:

Since states of the NBA $A_{\varphi}$ are explicitly represented as nodes of a
graph, it is straightforward to implement Algorithms 1 and 2. The check in
line 6 of Algorithm 1 is implemented by checking the satisfiability of
$B_{(s_{i},s_{i}^{\prime})}(I,O)\,\wedge\,B_{(s_{j},s_{j}^{\prime})}(I,O)$
using ROBDD operations. Similarly, the check in line 2 of Algorithm 2 is
implemented by checking the satisfiability of $\bigvee_{(s,s^{\prime})\in
out(p)\times out(q)}B_{(p,s)}(I,O)\wedge
B_{(q,s^{\prime})}(I^{\prime},O^{\prime})\wedge\bigwedge_{y\in
Y}(y\leftrightarrow y^{\prime})\wedge(z\leftrightarrow\neg z^{\prime})$ using
ROBDD operations. In the above formula, $I^{\prime}$ (resp. $O^{\prime}$)
denotes a set of fresh, primed copies of variables in $I$ (resp. $O$).

##### Implementing transformation of $A_{\varphi}$ to $A_{\varphi}^{\prime}$:

To obtain $A_{\varphi}^{\prime}$, we simply replace the ROBDD for
$B_{(s,s^{\prime})}$ on every edge $(s,s^{\prime})$ of the NBA $A_{\varphi}$
by an ROBDD for $\exists X\,B_{(s,s^{\prime})}$. While the worst-case
complexity of computing $\exists X\,B_{(s,s^{\prime})}$ using ROBDDs is
exponential in $|X|$, this doesn’t lead to inefficiencies in practice because
$|X|$ is typically small. Indeed, our experiments reveal that the total size
of ROBDDs in the representation of $A_{\varphi}^{\prime}$ is invariably
smaller, sometimes significantly, compared to the total size of ROBDDs in the
representation of $A_{\varphi}$. Indeed, this reduction can be significant in
some cases, as the following proposition shows.

###### Proposition 1

There exists an NBA $A_{\varphi}$ with a single dependent output such that the
ROBDD labeling its edge is exponentially (in number of inputs and outputs)
larger than that labeling the edge of $A_{\varphi}^{\prime}$.

###### Proof

Let $I=\\{i_{1},\ldots i_{n}\\}$ and $O=\\{o_{1},\ldots o_{n+1}\\}$ be sets of
input and output variables. Consider the LTL formula
$\mathsf{G}\big{(}o_{n+1}\leftrightarrow f(i_{1},\ldots i_{n},o_{1},\ldots
o_{n})\big{)}$, where $f$ is a Boolean function that gives the value of the
$n^{th}$ least significant bit (or middle bit) in the product obtained by
multiplying the unsigned integers represented by the $i_{1},\ldots i_{n}$ and
$o_{1},\ldots o_{n}$. The automaton $A_{\varphi}$ has a single state, which is
also an accepting state, with a self loop labeled by an ROBDD representing
$o_{n+1}\leftrightarrow f(i_{1},\ldots i_{n},o_{1},\ldots o_{n})$. It is known
that this ROBDD has size in $\Omega(2^{n})$ regardless of the variable
ordering. However, once we detect that $o_{n+1}$ is dependent on
$\\{i_{1},\ldots i_{n}\\}\cup\\{o_{1},\ldots o_{n}\\}$, we can project away
$o_{n+1}$, and the ROBDD after projection is simply a single node representing
$\mathsf{True}$. This is because for every combination of values of
$\\{i_{1},\ldots i_{n}\\}\cup\\{o_{1},\ldots o_{n}\\}$, there is a value of
$o_{n+1}$ that matches $f(i_{1},\ldots i_{n},o_{1},\ldots o_{n})$.

##### Implementing transducer $T_{X}$:

We now describe how to construct a Mealy machine corresponding to the
transducer $T_{X}$. As explained in the previous section, the transition
structure of the Mealy machine is obtained by applying the subset construction
to $A_{\varphi}$. While this requires $O(2^{|A_{\varphi}|})$ time if states
and transitions are explicitly represented, we show below that a sequential
circuit implementing the Mealy machine can be constructed directly from
$A_{\varphi}$ in time polynomial in $|X|$ and $|A_{\varphi}|$. This reduction
in construction complexity crucially relies on the fact that all variables in
$X$ are dependent on $I\cup(O\setminus X)$.

Let $S=\\{s_{0},\ldots s_{k-1}\\}$ be the set of states of $A_{\varphi}$, and
let $\mathsf{in}({s_{i}})$ denote the set of states that have an outgoing
transition to $s_{i}$ in $A_{\varphi}$. To implement the desired Mealy
machine, we construct a sequential circuit with $k$ state-holding flip-flops.
Every state $U~{}(\subseteq S)$ of the Mealy machine is represented by the
state of these $k$ flip-flops, i.e. by a $k$-dimensional Boolean vector.
Specifically, the $i^{th}$ component is set to $1$ iff $s_{i}\in U$. For
example, if $S=\\{s_{0},s_{1},s_{2}\\}$ and $U=\\{s_{0},s_{2}\\}$, then $U$ is
represented by the vector $\langle 1,0,1\rangle$. Let $n_{i}$ and $p_{i}$
denote the next-state input and present-state output of the $i^{th}$ flip-
flop. The next-state function $\delta^{X}$ of the Mealy machine is implemented
by a circuit, say $\Delta^{X}$, with inputs $\\{p_{0},\ldots
p_{k-1}\\}\,\cup\,I\,\cup\,(O\setminus X)$ and outputs $\\{n_{0},\ldots
n_{k-1}\\}$. For $i\in\\{0,\ldots k-1\\}$, output $n_{i}$ of this circuit
implements the Boolean function
$\bigvee_{s_{j}\,\in\,\mathsf{in}({s_{i}})}\big{(}p_{j}\wedge\exists
X\,B_{(s_{j},s_{i})}\big{)}$. To see why this works, suppose $\langle
p_{0},\ldots p_{k-1}\rangle$ represents the current state $U\subseteq S$ of
the Mealy machine. Then the above function sets $n_{i}$ to true iff there is a
state $s_{j}\in U$ (i.e. $p_{j}=1$) s.t. there is a transition from $s_{j}$ to
$s_{i}$ on some values of outputs $X$ and for the given values of
$I\cup(O\setminus X)$ (i.e. $\exists X\,B_{(s_{j},s_{i})}\,=\,1$). This is
exactly the condition for $s_{i}$ to be present in the state
$U^{\prime}\subseteq S$ reached from $U$ for the given values of
$I\cup(O\setminus X)$ in the Mealy machine obtained by subset construction.

It is known from the knowledge compilation literature (see e.g. [12, 3, 1])
that every ROBDD can be compiled in linear time to a Boolean circuit in
Decomposable Negation Normal Form (DNNF), and that every DNNF circuit admits
linear time projection of variables, yielding a resultant DNNF circuit. Hence,
a Boolean circuit for $\exists X\,B_{(s_{j},s_{i})}$ can be constructed in
time linear in the size of the ROBDD representation of $B_{(s_{j},s_{i})}$.
This allows us to construct the circuit $\Delta^{X}$, implementing the next-
state transition logic of our Mealy machine, in time (and space) linear in
$|X|$ and $|A_{\varphi}|$.

Next, we turn to constructing a circuit $\Lambda^{X}$ that implements the
output function $\lambda^{X}$ of our Mealy machine. It is clear that
$\Lambda^{X}$ must have inputs $\\{p_{0},\ldots p_{k-1}\\}\cup
I\cup(O\setminus X)$ and outputs $X$. Since $X$ is automata dependent on
$I\cup(O\setminus X)$ in $A_{\varphi}$, the following proposition is easily
seen to hold.

###### Proposition 2

Let $B_{(s,s^{\prime})}$ be a Boolean function with support $I\cup O$ that
labels a transition $(s,s^{\prime})$ in $A_{\varphi}$. For every
$(\sigma_{I},\sigma)\in\Sigma_{I}\times\Sigma_{O\setminus X}$, if
$(\sigma_{I},\sigma)\models\exists X\,B_{(s,s^{\prime})}$, then there is a
unique $\sigma^{\prime}\in\Sigma_{X}$ such that
$(\sigma_{I},\sigma,\sigma^{\prime})\models B_{(s,s^{\prime})}$.

Considering only the transition $(s,s^{\prime})$ referred to in Proposition 2,
we first discuss how to synthesize a vector of Boolean functions, say
$F^{(s,s^{\prime})}=\langle F_{1}^{(s,s^{\prime})},\ldots
F_{|X|}^{(s,s^{\prime})}\rangle$, where each component function has support
$I\cup(O\setminus X)$, such that
$F^{(s,s^{\prime})}[I\mapsto\sigma_{I}][O\setminus
X\mapsto\sigma]=\sigma^{\prime}$. Generalizing beyond the specific assignment
of $I\cup O$, our task effectively reduces to synthesizing an
$|X|$-dimensional vector of Boolean functions $F^{(s,s^{\prime})}$ s.t.
$\forall I\cup(O\setminus X)\,\big{(}\exists
XB_{(s,s^{\prime})}~{}\rightarrow~{}B_{(s,s^{\prime})}[X\mapsto
F^{(s,s^{\prime})}]\big{)}$ holds. Interestingly, this is an instance of
_Boolean functional synthesis_ – a problem that has been extensively studied
in the recent past (see e.g. [10, 3, 1, 2, 5]). In fact, we know from [1, 24]
that if $B_{(s,s^{\prime})}$ is represented as an ROBDD, then a Boolean
circuit for $F_{(s,s^{\prime})}$ can be constructed in
$\mathcal{O}\big{(}|X|^{2}.|B_{(s,s^{\prime})}|\big{)}$ time, where
$|B_{(s,s^{\prime})}|$ denotes the size of the ROBDD for $B_{(s,s^{\prime})}$.
For every $x_{i}\in X$, we use this technique to construct a Boolean circuit
for $F_{i}^{(s,s^{\prime})}$ for every edge $(s,s^{\prime})$ in $A$. The
overall circuit $\Lambda^{X}$ is constructed such that the output for
$x_{i}\in X$ implements the function
$\bigvee_{trans.~{}(s,s^{\prime})~{}in~{}A}\big{(}p_{s}\wedge(B_{(s,s^{\prime})}[X\mapsto
F^{(s,s^{\prime})}])\wedge F_{i}^{(s,s^{\prime})}\big{)}$.

###### Lemma 3

Let $U\subseteq S$ be a non-empty set of pairwise compatible states of $A$.
For $(\sigma_{I},\sigma)\in\Sigma_{I}\times\Sigma_{O\setminus X}$, if
$\delta^{X}\big{(}U,(\sigma_{I},\sigma)\big{)}\neq\emptyset$, then the outputs
$X$ of $\Lambda^{X}$ evaluate to
$\lambda^{X}\big{(}U,(\sigma_{I},\sigma)\big{)}$. In all other cases, every
output of $\Lambda^{X}$ evaluates to $0$.

Note that $\delta^{X}\big{(}U,(\sigma_{I},\sigma)\big{)}=\emptyset$ iff all
outputs $n_{i}$ of the circuit $\Delta^{X}$ evaluate to $0$. This case can be
easily detected by checking if $\bigvee_{i=0}^{k-1}n_{i}$ evaluates to $0$. We
therefore have the following result.

###### Theorem 5.1

The sequential circuit obtained with $\Delta^{X}$ as next-state function and
$\Lambda^{X}$ as output function is a correct implementation of transducer
$T_{X}$, assuming (a) the initial state is $p_{0}=1$ and $p_{j}=0$ for all
$j\in\\{1,\ldots k-1\\}$, and (b) the output is interpreted as $\bot$ whenever
$\bigvee_{i=0}^{k-1}n_{i}$ evaluates to $0$.

##  6 Experiments and Evaluation

We implemented the synthesis pipeline depicted in Figure 2 in a tool called
DepSynt, using symbolic approach of Section 5. For steps 1., 4., of the
pipeline, i.e., construction of $A_{\varphi}$ and synthesis of $T_{Y}$, we
used the tool Spot [6], a widely used library for representing and
manipulating NBAs. We then experimented 111The experiment results can be
accessed at https://eliyaoo32.github.io/DepSynt with all available reactive
synthesis benchmarks from the SYNTCOMP [19] competition, a total of 1,141 LTL
specifications over 31 benchmark families.

All our experiments were run on a computer cluster, with each problem instance
run on an Intel Xeon Gold 6130 CPU clocking at 2.1 GHz with 2GB memory and
running Rocky Linux 8.6. Our investigation was focussed on answering two main
research questions:
RQ1: How prevalent are dependent outputs in reactive synthesis benchmarks?
RQ2: Under what conditions, if any, is reactive synthesis benefited by our
approach, i.e., of identifying and separately processing dependent output
variables?

###  6.1 Dependency Prevalence

To answer RQ1, we implemented the algorithm in Section 3 and executed it with
a timeout of 1 hour. Within this time, we were able to find 300 benchmarks out
of 1,141 SYNTCOMP benchmarks, that had at least 1 dependent output variable
(as per Definition 4). Out of the 1,141 benchmarks, 260 had either timeout (41
total) or out-of-memory (219 total), out of which 227 failed because of the
NBA construction (adapted from Spot), i.e, Step 1 in our pipeline, did not
terminate. We found that all the benchmarks with at least 1 dependent variable
in fact belong to one of 5 benchmark families, as seen in Table 1. In order to
measure the prevalence of dependency we evaluated (1) the number of dependent
variables and (2) the $\text{dependency ratio}=\frac{\text{Total dependent
vars}}{\text{Total output vars}}$.

Benchmark Family | Total | Completed | Found Dep | Avg Dep Ratio
---|---|---|---|---
ltl2dpa | 24 | 24 | 24 | $.434$
mux | 12 | 12 | 4 | $1$
shift | 11 | 4 | 4 | $1$
tsl-paper | 118 | 117 | 115 | $.46$
tsl-smart-home-jarvis | 189 | 167 | 153 | $.33$
Table 1: Summary for 5 benchmark families, indicating the no. of benchmarks,
where the dependency-finding process was completed, the total count of
benchmarks with dependent variables, and the average dependency ratio among
those with dependencies.

Out of those depicted, Mux (for multiplexer) and shift (for shift-operator
operator) were two benchmark families where dependency ratio was 1. In total,
among all those where our dependency checking algorithm terminated, we found
26 benchmarks with all the output variables dependent. Of these 4 benchmarks
were from Shift, 4 benchmarks from mux, 14 benchmarks from tsl-paper, and 4
from tsl-smart-home-jarvis. Note that in Mux, total dependency was found only
for 4 out of 11, where the input was a power of 2. Looking beyond total
dependency, among the 300 benchmarks with at least 1 dependent variable, we
found a diverse distribution of dependent variables and ratio as shown in
Figure 3.

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.

###  6.2 Utilizing Dependency for Reactive Synthesis: Comparison with other
tools

Despite a large 1 hr time out, we noticed that most dependent variables were
found within 10-12 seconds. Hence, in our tool DepSynt, we limited the time
for dependency-check to an empirically determined 12 seconds, and declared
unchecked variables after this time as non-dependent. Since synthesis of non-
dependents $T_{Y}$ (Step 5. of the pipeline) is implemented directly using
Spot APIs, the difference between our approach and Spot is minimal when there
are a large number of non-dependent variables. This motivated us to divide our
experimental comparison, among the 300 benchmarks where at least one dependent
variables was found, into benchmarks with at most 3 non-dependent variables
(162 benchmarks) and more than 3 non-dependent variables (138 benchmarks). We
compared DepSynt with two state-of-the-art synthesis tools, that won in
different tracks of SYNTCOMP23’ [19]: (i) Ltlsynt (based on Spot)[6] with
different configurations ACD, SD, DS, LAR, and (ii) Strix[20] with the
configuration of BFS for exploration and FPI as parity game solver (the
overall winning configuration/tool in SYNTCOMP’23). All the tools had a total
timeout of 3 hours per benchmark. As can be seen from Figure 5, indeed for the
case of $\leq 3$ non-dependent variables, DepSynt outperforms the highly
optimized competition-winning tools. Even for $>3$ case, as shown in Figure 5,
the performance of DepSynt is comparable to other tools, only beaten
eventually by Strix. DepSynt uniquely solved 2 specifications for which both
Strix and Ltlsynt timed out after 3600s, the benchmarks are mux32, and mux64,
and solved in 2ms, and 4ms respectively.

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.

###  6.3 Analyzing time taken by different parts of the pipeline

Figure 6: Normalized time distribution of DepSynt sorted by total duration
over benchmarks that could be solved successfully by DepSynt. Each color
represents a different phase of DepSynt. The pink is searching for dependency,
the green is the NBA build, the blue is the non-dependent variables and the
yellow is the dependent variables synthesis. Figure 7: This figure illustrates
the total BDD sizes of the NBA edges before and after the projection of the
dependent variables from the NBA edges, the left figure is over the benchmark
with at most 3 non-dependent variables and the right figure is over the
benchmarks with 4 or more non-dependent variables. The solid line presents the
projected BDD size and the dotted line presents the original BDD size. The
y-axis is presented in a symmetric log-scale. The benchmarks are sorted by the
projected NBA’s BDD total size.

In order to better understand where DepSynt spends its time, we plotted in
Figure 6 the normalized time distribution of DepSynt. We can see that
synthesizing a strategy for dependent variables is very fast (the gray
portion)- justifying its theoretical linear complexity bound, and so is the
red-region depicting searching for dependency (again, a poly-time algorithm),
especially compared to the white region synthesizing a strategy for the non-
dependent variables. This also explains why having high dependency ratio alone
does not help our approach, since even with high ratio, number of non-
dependent variables could be large, resulting in worse performance overall.

###  6.4  Analysis of the Projection step (Step 3.) of Pipeline

The rationale for projecting variables from the NBA is to reduce the number of
output non-dependent variables in the synthesis of the NBA, which is the most
expensive phase as Figure 6 shows. To see if this indeed contributes to our
better performance, we asked if projecting the dependent variables reduces the
BDDs’ sizes, in terms of total nodes, (the BDD represents the transitions).
Figure 7 shows that the BDDs’ sizes are reduced significantly where the total
of non-dependent variables is at most 3, in cases of total dependency, the BDD
just vanishes and is replaced by the constant true/false. For the case of
total non-dependent is 4 or more, the BDD size is reduced as well.

###  6.5 An ablation experiment with Spot

As a final check, that dependency was causing the improvements seen, we
conducted a control/ablation experiment where in DepSynt we gave zero-timeout
to find dependency, and classifies all output variables are classified as non-
dependent, and called this SpotModular. As can be seen in Figure 8, in the
left plot, for the case of benchmarks with at least 1 dependent and at most 3
non-dependent variables, the benefit of dependency-checking, while the plot on
the right, shows that for the remaining cases we do not see this.

Figure 8: Cactus plot comparing DepSynt and SpotModular on 162 benchmarks with
at most 3 non-dependent variables (left) and 138 benchmarks with more than 3
non-dependent variables (right).

###  6.6 Summary

Overall, we answered both the research questions we started with. Indeed there
are several benchmarks with dependent variables, and using our pipeline does
give performance benefits when no. of non-dependent variables is low. Our
recipe would be to first run our poly-time check to see if there are
dependents and if there aren’t too many non-dependents, use our approach and
otherwise switch to any existing method.

To summarize our comparison against other tools, we state the following. When
comparing with Strix, we found 252 benchmarks that had dependent variables in
which DepSynt took less time than Strix. Out of which, in 126 benchmarks
DepSynt took at least 1 second less than Strix. Among these, there are 10
benchmarks (shift16, LightsTotal_d65ed84e, LightsTotal_9cbf2546,
LightsTotal_06e9cad4, Lights2_f3987563, Lights2_0f5381e9,
FelixSpecFixed3.core_b209ff21, Lights2_b02056d6, Lights2_06e9cad4,
LightsTotal_2c5b09da) for which the time taken by DepSynt was at least 10
seconds less than that taken by Strix. These are the examples that are easier
to solve by DepSynt than by Strix. For shift16, the difference was more than
1056 seconds in favor of DepSynt. Interestingly, shift16 also has all output
variables dependent.

When comparing with Ltlsynt, we found 193 benchmarks that had dependent
variables in which DepSynt took less time than Ltlsynt. Among these, in 27
benchmarks DepSynt took at least 1 second less than Ltlsynt. Of these, there
is one benchmark (ModifiedLedMatrix5X) for which the time taken by DepSynt was
at least 10 seconds less than that taken by Ltlsynt. Specifically, DepSynt
took 5 seconds and Ltlsynt took 55 seconds.

##  7 Conclusion

In this work, we have introduced the notion of dependent variables in the
context of reactive synthesis. We showed that dependent variables are
prevalent in reactive synthesis benchmarks and suggested a synthesis approach
that may utilize these dependency for better synthesis. As part of future
work, we wish to explore heuristics for choosing ”good” maximal subsets of
dependent variables. We also wish to explore integration of our method in
other reactive synthesis tools such as Strix.

## References

  * [1] Akshay, S., Arora, J., Chakraborty, S., Krishna, S.N., Raghunathan, D., Shah, S.: Knowledge compilation for boolean functional synthesis. In: Barrett, C.W., Yang, J. (eds.) 2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22-25, 2019. pp. 161–169. IEEE (2019)
  * [2] Akshay, S., Chakraborty, S.: Synthesizing skolem functions: A view from theory and practice. In: Sarukkai, S., Chakraborty, M. (eds.) Handbook of Logical Thought in India, pp. 1–36. Springer (2022)
  * [3] Akshay, S., Chakraborty, S., Goel, S., Kulal, S., Shah, S.: What’s hard about boolean functional synthesis? In: Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10981, pp. 251–269. Springer (2018)
  * [4] Akshay, S., Chakraborty, S., Goel, S., Kulal, S., Shah, S.: Boolean functional synthesis: hardness and practical algorithms. Formal Methods Syst. Des. 57(1), 53–86 (2021). https://doi.org/10.1007/s10703-020-00352-2, https://doi.org/10.1007/s10703-020-00352-2
  * [5] Amram, G., Bansal, S., Fried, D., Tabajara, L.M., Vardi, M.Y., Weiss, G.: Adapting behaviors via reactive synthesis. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I. Lecture Notes in Computer Science, vol. 12759, pp. 870–893. Springer (2021)
  * [6] Blahoudek, F., Duret-Lutz, A., Strejček, J.: Seminator 2 can complement generalized Büchi automata via improved semi-determinization. In: Proceedings of the 32nd International Conference on Computer-Aided Verification (CAV’20). Lecture Notes in Computer Science, vol. 12225, pp. 15–27. Springer (Jul 2020)
  * [7] Bloem, R., Chatterjee, K., Jobstmann, B.: Graph games and reactive synthesis. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 921–962. Springer (2018)
  * [8] Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911–938 (2012)
  * [9] Bryant, R.E.: Binary decision diagrams and beyond: Enabling technologies for formal verification. In: Proceedings of IEEE International Conference on Computer Aided Design (ICCAD). pp. 236–243. IEEE (1995)
  * [10] Chakraborty, S., Fried, D., Tabajara, L.M., Vardi, M.Y.: Functional synthesis via input-output separation. Formal Methods Syst. Des. 60(2), 228–258 (2022)
  * [11] Church, A.: Logic, arithmetic, and automata. In: International Congress of Mathematicians. p. 23–35 (1962)
  * [12] Darwiche, A.: Decomposable negation normal form. J. ACM 48(4), 608–647 (2001)
  * [13] Faymonville, P., Finkbeiner, B., Tentrup, L.: Bosy: An experimentation framework for bounded synthesis. In: Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II. pp. 325–332. Springer (2017)
  * [14] Finkbeiner, B., Geier, G., Passing, N.: Specification decomposition for reactive synthesis. In: NASA Formal Methods - 13th International Symposium, NFM 2021, Virtual Event, May 24-28, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12673, pp. 113–130. Springer (2021)
  * [15] Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transf. 15(5-6), 519–539 (2013)
  * [16] Golia, P., Slivovsky, F., Roy, S., Meel, K.S.: Engineering an efficient boolean functional synthesis engine. 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD) pp. 1–9 (2021)
  * [17] Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Publishing Company (1979)
  * [18] Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, USA (2004)
  * [19] Jacobs, S., Perez, G.A., Abraham, R., Bruyere, V., Cadilhac, M., Colange, M., Delfosse, C., van Dijk, T., Duret-Lutz, A., Faymonville, P., Finkbeiner, B., Khalimov, A., Klein, F., Luttenberger, M., Meyer, K., Michaud, T., Pommellet, A., Renkin, F., Schlehuber-Caissier, P., Sakr, M., Sickert, S., Staquet, G., Tamines, C., Tentrup, L., Walker, A.: The reactive synthesis competition (syntcomp): 2018-2021 (2022)
  * [20] Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: Explicit reactive synthesis strikes back! In: Computer Aided Verification: 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. pp. 578–586. Springer (2018)
  * [21] Michaud, T., Colange, M.: Reactive synthesis from ltl specification with spot. In: Proceedings of the 7th Workshop on Synthesis, SYNT@ CAV (2018)
  * [22] Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 179–190 (1989)
  * [23] Rabe, M.N., Seshia, S.A.: Incremental determinization. In: Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings. pp. 375–392 (2016)
  * [24] Shah, P., Bansal, A., Akshay, S., Chakraborty, S.: A normal form characterization for efficient boolean skolem function synthesis. In: 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021. pp. 1–13. IEEE (2021). https://doi.org/10.1109/LICS52264.2021.9470741, https://doi.org/10.1109/LICS52264.2021.9470741
  * [25] Soos, M., Meel, K.S.: Arjun: An efficient independent support computation technique and its applications to counting and sampling. In: ICCAD (Nov 2022)
  * [26] Tseitin, G.S.: On the complexity of derivation in propositional calculus. Automation of reasoning: 2: Classical papers on computational logic 1967–1970 pp. 466–483 (1983)
  * [27] Vardi, M., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994). https://doi.org/https://doi.org/10.1006/inco.1994.1092, https://www.sciencedirect.com/science/article/pii/S0890540184710923

##  Appendix 0.A Additional material for defining dependency

To find a maximal dependent set of variables we describe Algorithm 3 called
FindDependent as follows. FindDependent gets as input an LTL formula $\varphi$
over the set of variables $V=I\cup O$, and initializes the set $X$ that
includes the dependent variables found so far to be empty (line $1$). Then at
every step (line $2$) we choose a variable $z\in O$ that was not tested before
and check if $z$ is dependent of the remaining variables, excluding those that
were already found dependent (line 3). This is done through a procedure called
isDependent() which we discuss next. If so then $x$ is added $X$ (line 4). At
the end of the process, we have that $X$ is returned as an output of
FindDependent. The heart of the framework is naturally in the procedure
isDependent that takes a variable $z$ and a set $Y$ and returns true iff
$\\{z\\}$ is dependent on $Y$ in $\varphi$ according to definition 1.

To prove that FindDependent returns a maximal dependent set, we assume that
$isDependent$ is well defined. That is, for a variable $z$ and a set $Y$
$isDependent$ returns $true$ if and only if $\\{z\\}$ is dependent on $Y$ in
$\varphi$. The automata variant of FindDependent, that we use in this paper,
makes use of the automata variant of $isDependent$, called
$isAutomataDependent$, in which this assumption is verified.

###### Theorem 0.A.1

Given an LTL formula $\varphi$ over the set of variables $V$, FindDependent
returns a maximal dependent set in $\varphi$.

Algorithm 3 Find Dependent Variables

Input LTL Formula $\varphi$ with variables $V=I\cup O$
Output A set $X\subseteq O$ which is maximal dependent in $\varphi$

1:$X\leftarrow\emptyset$

2:for $z\in O$ do

3: if isDependent($z,V\backslash(X\cup\\{z\\})$) then

4: $X\leftarrow X\cup\\{z\\}$

5: end if

6:end for

7:return $X$

To prove Theorem 0.A.1, we first make the following claim.

###### Claim

Let $X^{\prime}$ be a set of output variables and $X\subseteq X^{\prime}$. If
$X^{\prime}$ is dependent in $\varphi$, then so is $X$.

###### Proof

Set $w,w^{\prime}\in L(\varphi)$ with the same prefix $w[0,i]=w^{\prime}[0,i]$
for some $i\geq 0$. Assume $w_{i}.(V\backslash X)=w^{\prime}_{i}.(V\backslash
X)$. Then since $V\backslash X^{\prime}\subseteq V\backslash X$ we have that
$w_{i}.V\backslash X^{\prime}=w^{\prime}_{i}.V\backslash X^{\prime}$.
Therefore $w_{i}.X^{\prime}=w_{i}.X^{\prime}$, which means that
$w_{i}.X=w_{i}.X$ as well.

We now provide the proof for Theorem 0.A.1.

######  Proof (Proof of Theorem 0.A.1)

Denote by $X^{i}$ the set $X$ in the $i$’th step of the loop obtained in line
5. We show by induction that $X^{i}$ is dependent on $V\backslash X^{i}$ in
$\varphi$. For step $0$, we have that the empty set is naturally dependent on
$V$. Assume by induction that $X^{i-1}$ is dependent on $V\backslash X^{i-1}$.
Then at step $i$, if no element was added to $X^{i-1}$ then $X^{i}=X^{i-1}$
and we are done. Otherwise, we have $X^{i}=X^{i-1}\cup\\{z\\}$. Then let
$j\geq 0$ be such that for two words $w,w^{\prime}$ in $L(\varphi)$,
$w[0,j-1]=w^{\prime}[0,j-1]$ and $w_{j}.V\backslash
X^{i}=w^{\prime}_{j}.V\backslash X^{i}$. Then since $z$ was just added, it
follows that $w_{j}.\\{z\\}=w^{\prime}_{j}.\\{z\\}$. But then since
$X^{i}=X^{i-1}\cup\\{z\\}$ is follows that $w_{j}.V\backslash
X^{i-1}=w^{\prime}_{j}.V\backslash X^{i-1}$ and by induction
$w^{\prime}_{j}.X^{i-1}=w^{\prime}_{j}.X^{i-1}$. hence in total
$w_{j}.X^{i}=w^{\prime}_{j}.X^{i}$. Note that it also follows that at the end
of the algorithm $X$ is dependent on $V\backslash X$ in $\varphi$ and hence
$X$ is dependent in $\varphi$.

To see that $X$ is maximal, assume for contradiction that it is not and let
$X^{\prime}\subseteq O$ be a dependent set that strictly contains $X$. Let
$z\in X^{\prime}\backslash X$. Then $\\{z\\}\subseteq X^{\prime}$ hence, from
the Claim above we have that $z$ is dependent in $V\backslash\\{z\\}$. So $z$
should have been picked up as a member of $X^{i}$ and therefore in $X$ in some
round $i$ of the algorithm, a contradiction.∎