An extended abstract of this article appeared in the Proceedings of the 33rd
Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018.

# Sequential Relational Decomposition

Dror Fried  Department of Computer Science, The Open University of Israel,
Israel<EMAIL_ADDRESS>,  Axel Legay  Department of Computer Science,
Université Catholique de Louvain, Belgium<EMAIL_ADDRESS>,  Joël
Ouaknine  Max Planck Institute for Software Systems, Saarland Informatics
Campus, Germany  Department of Computer Science, Oxford University, UK
<EMAIL_ADDRESS>and  Moshe Y. Vardi  Department of Computer Science, Rice
University, USA<EMAIL_ADDRESS>
###### Abstract.

The concept of _decomposition_ in computer science and engineering is
considered a fundamental component of _computational thinking_ and is
prevalent in design of algorithms, software construction, hardware design, and
more. We propose a simple and natural formalization of _sequential
decomposition_ , in which a task is decomposed into two sequential sub-tasks,
with the first sub-task to be executed before the second sub-task is executed.
These tasks are specified by means of input/output relations. We define and
study _decomposition problems_ , which is to decide whether a given
specification can be sequentially decomposed. Our main result is that
decomposition itself is a difficult computational problem. More specifically,
we study decomposition problems in three settings: where the input task is
specified explicitly, by means of Boolean circuits, and by means of automatic
relations. We show that in the first setting decomposition is NP-complete, in
the second setting it is NEXPTIME-complete, and in the third setting there is
evidence to suggest that it is undecidable. Our results indicate that the
intuitive idea of decomposition as a system-design approach requires further
investigation. In particular, we show that adding a human to the loop by
asking for a decomposition hint lowers the complexity of decomposition
problems considerably.

###### Key words and phrases:

Decomposition, Composition, Automatic Relations, Positivity, Synthesis

##  1\. Introduction

Over the past decade, it became apparent that the conceptual way of analyzing
problems through computer-science techniques can be considered as a general
approach to analysis, design, and problem solving, known as _computational
thinking_ [46, 47]. A key element of this approach is the taming of complexity
by decomposing a complex problem into simpler problems. Quoting Wing [46]:
“Computational thinking is using abstraction and decomposition when attacking
a large complex task or designing a large complex system.” While abstraction
helps to tame complexity by simplifying away irrelevant details of a complex
problem, decomposition helps to tame complexity by breaking down complex
problems into simpler ones. In fact, decomposition is a generic project-
management technique: project managers quite often face challenges that
require decomposition – a large project that is divided among team members to
make the problem less daunting and easier to solve as a set of smaller tasks,
where team members work on tasks that are in their specific fields of
expertise. As computer scientists and engineers, the concept of decomposition
is prevalent in the design of algorithms, in software construction, in
hardware design, and so on. For example, a classical paper in software
engineering studies criteria to be used in decomposing systems into modules
[38]. Yet, in spite of the centrality of the concept of decomposition in
computational thinking, it has yet to be studied formally in a general
theoretical setting (see related work). Such a study is the focus of this
work.

There are many different types of decomposition that can be considered. Based
on her understanding of the problem, the _decomposer_ has to make a decision
on how to decompose a given problem, for example, by meeting certain
constraints on the size of the sub-problems, or constraints on the way that
solved sub-problems ought to be recomposed. A simple and natural way of
decomposition is _sequential_ decomposition in which a task is decomposed into
two sub-tasks, where the first sub-task is to be carried out before the second
sub-task can be executed. A formal model for sequential decomposition is the
subject of this work. We assume that the given problem is specified by means
of an input/output relation. It is widely accepted that such relations are the
most general way to specify programs, whether for terminating programs [20],
where input and output should be related values, or for nonterminating
programs [39], where input and output are streams of values. The
_decomposition problem_ is to decompose a given input/output relation $R$,
between an input domain $\mathcal{I}$ and an output domain $\mathcal{O}$, into
two relations $R_{1}$ and $R_{2}$, such that $R$ can be reconstructed from
$R_{1}$ and $R_{2}$ using relational composition (defined in Section 3). To
avoid trivial solutions, where either $R_{1}$ or $R_{2}$ is the identity
relation, we assume that the intermediate domain, that is, the co-domain of
$R_{1}$, which is also the domain of $R_{2}$, is specified. Intuitively,
specifying the intermediate domain amounts to constraining the manner in which
the first task can “communicate” with the second task. Such a restriction can
be viewed as a form of _information hiding_ , which is one of the major
criteria for decomposition in [38]. As we show, sequential decomposition is
nontrivial only when the channel of communication between the first and second
task has a small ”bandwidth”, appropriately defined.

We study sequential decomposition in three settings: _explicit_ , _symbolic_ ,
and _automatic_. In the explicit setting, the input/output relation $R$ is
specified explicitly. In the symbolic setting, the domains and $R$ are finite
but too large to be specified explicitly, so $R$ is specified symbolically as
a Boolean circuit. In the automatic setting, the domains and $R$ may be
infinite, so the domains are specified by means of an alphabet, over which $R$
is specified by means of a deterministic finite-state automaton.

Our general finding is that sequential decomposition, viewed as a
computational problem, is itself a challenging problem. In the explicit
setting, the decomposition problem is NP-complete. This escalates to NEXPTIME-
complete for the symbolic setting. For the automatic setting the decomposition
problem is still open, but we provide evidence and conjecture that it is
undecidable. Specifically, we show that even a very simple variant of the
automatic setting can be viewed as equivalent to the Positivity problem, whose
decidability is well known to be open [44, 35]. We do show, however, that a
“strategic” variant of the automatic setting, in which the required relations
are described as transducers is in EXPTIME. These findings, that decomposition
is an intractable problem, can be viewed as a “No-Free-Lunch” result, as it
says that decomposition, which is a tool to combat complexity, is itself
challenged by computational complexity. This means that while decomposition is
an essential tool, the application of decomposition is an art, rather than
science, and requires human intuition.

As such, we explore decomposition with ”a human in the loop”, where the role
of the human is to offer a hint, suggesting one of the terms of the
decomposition, and the role of the decomposition algorithm is to check if a
valid decomposition can be found based on the hint. Table 1 summarizes our
complexity results with and without hints. We show that in most cases
decomposition with a hint is easier than decomposition with no hint.

Table 1. Computational complexity of decomposition without and with hints. | Without hints | With hint $R_{1}$ | With hint $R_{2}$
---|---|---|---
Explicit | NP-complete | PTIME | PTIME
Symbolic | NEXPTIME-complete | $\Pi_{3}^{P}$ | $\Pi_{3}^{P}$
Automatic | undecidabe? | EXPSPACE | EXPSPACE
Strategic | EXPTIME | EXPTIME | PTIME

##  2\. Related work

In this paper we introduce a new framework to study _decomposition_ of system-
level specifications into component-level specifications. In contrast, most
existing approaches in software engineering focus on _composition_ , that is,
developing systems from independently developed components, or proving system-
level properties from component-level properties, for example [15]. This
compositional approach is a fundamental approach in computer science to taming
complexity.

We now give a few examples of the composition-based approach to system
development. The _contract-theory_ approach of Benveniste et al. [6] uses
assumption/guarantee to describe both the implementation and the environment
of a given component; that is, the implementation of the component should work
with any other component whose implementation satisfies the assumption.
Components are then composed in a bottom up fashion to produce a large-size
system. The same approach is pursued also in the _interface theories_ of de
Alfaro et al. [12], the _modal automata_ of Larsen [32], and the _I/O
automata_ of Lynch [34].

Operations such as _quotient_ (adjoint of composition) or contextual equation
solving [31, 13] allow one to synthesize a component that can be composed with
another one in order to refine a large size specification. This gets close to
the problem of decomposition with _hints_ , described below, but is still
focused on synthesizing an implementation. The BIP approaches of Sifakis [5]
proposes to specify complex systems by aggregating smaller components using a
very expressive algebra. Recently in [10], the approach has been extended to
synthesize the order of communication between components, but the focus there
is not on decomposing specification. Similarly, Lustig and Vardi have shown
[33] how to synthesize reactive systems satisfying given linear-temporal
properties by composing components from a given library of reactive
components. Closer to our work is an approach studied in model-driven software
engineering. The Fragmenta tool [3] provides algebraic descriptions of models
and fragments based on graph morphism. While the tool eases the decomposition
task, it does not specifically handle the problem of actually providing such a
decomposition.

A major weakness of composition-based approaches to system development is that
they consider only the problem of simplifying the implementation work, but
ignore the task of decomposing the often very complex system-level technical
specifications into smaller/simpler ones. For example, there is no technique
to explain how smaller assumption/guarantee contracts can be obtained from
larger ones. This operation has to be conducted manually by developers using
their intuition and understanding of complex system-level specifications.
Thus, our work here on decomposition complements existing approaches on
composition-based development. In addition, we believe that our work is also
relevant to _architectural design_ , e.g., as a complement of [7].

A classical paper of Parnas in software engineering studies criteria to be
used in decomposing systems into modules [38]. Parnas’s framework, however,
assumes that the starting point for decomposition consists of an architectural
specification of the system, while our starting point is quite more abstract,
as we assume that we are provided with a relational specification. Another
related work is that of [41], which describes an approach for extracting
sequential components from a system specification. Unlike, however, our work
here, which starts from a highly abstract relational specification, the
approach of [41] assumes that the system’s specification is provided by means
of an interface specification of the components. Thus, this approach is more
in the sense of a factorization rather then a decomposition.

Decomposition has been studied in the context of linear algebra. A matrix
decomposition or matrix factorization is a factorization of a matrix into a
product of matrices. There are many different matrix factorizations. Certain
Boolean matrix-factorization problems are known to be NP-complete [23]. Our
NP-completeness result for explicit relations can be viewed as a special case
of Boolean matrix-factorization. In addition, our formulation for the explicit
case can be viewed as a reformulation of the combinatorial definition of the
nondeterministic communication complexity (see Chapters 1-2 in [29]). In that
sense, this paper extends these works to more general representations of
relations.

##  3\. Preliminaries

###  3.1. Relations

Let $A,B,C$ be sets. For a binary relation $R\subseteq A\times B$, let
$Dom(R)$, and $Img(R)$ be the domain of $R$, and the image (sometimes called
co-domain) of $R$, defined as follows. $Dom(R)=\\{a\in A\mid\exists b\in
B\text{ s.t }(a,b)\in R\\}$, and $Img(R)=\\{b\in B\mid\exists a\in A\text{ s.t
}(a,b)\in R\\}$. For $a\in A$, let $Img_{a}(R)=\\{b\in B\mid(a,b)\in R\\}$.
The relation $R$ is called a function if for every $a\in A,b,b^{\prime}\in B$
we have $(a,b),(a,b^{\prime})\in R\implies b=b^{\prime}$. Given binary
relations $R_{1}\subseteq A\times B$, and $R_{2}\subseteq B\times C$, the
composition of $R_{1}$ and $R_{2}$ is a binary relation $R_{1}\circ
R_{2}\subseteq A\times C$ where $R_{1}\circ R_{2}=\\{(a,c)\mid\exists b\in
B\text{ s.t. }(a,b)\in R_{1}\text{ and }(b,c)\in R_{2}\\}$.

###  3.2. Automata

A Nondeterministic Finite Automaton (NFA) is a tuple
$\mathcal{A}=(\Sigma,Q,q,\delta,F)$, where $\Sigma$ is a finite alphabet, $Q$
is a finite state set with an initial state $q$, $\delta:Q\times\Sigma\to
2^{Q}$ is a transition function, and $F$ is an accepting-state set. A run of
$\mathcal{A}$ over a word $w=a_{1}a_{2}\cdots a_{n}$ for some $n$ is a state
sequence $r=q_{0},q_{1},\cdots,q_{n}$ such that
$q_{i+1}\in\delta(q_{i},a_{i})$ for $i\geq 0$, where $q_{0}=q$ is the initial
state. A run is accepting if its final state is accepting. A word is accepted
if it has an accepting run. The language of $\mathcal{A}$, $L(\mathcal{A})$,
is the set of all accepted words of $\mathcal{A}$ and is called a regular
language. A language is also regular if and only if it can be described by a
regular expression. We define the size of the automaton $\mathcal{A}$ as
$|Q|+|\Sigma|+|\delta|$ and denote this size by $|\mathcal{A}|$. For NFAs
$\mathcal{A}_{1}=(\Sigma_{1},Q_{1},q^{1},\delta_{1},F_{1})$ and
$\mathcal{A}_{2}=(\Sigma_{2},Q_{2},q^{2},\delta_{2},F_{2})$, we define the
product automaton of $\mathcal{A}_{1}$ and $\mathcal{A}_{2}$ as the automaton
$\mathcal{A}_{1}\times\mathcal{A}_{2}=(\Sigma_{1}\times\Sigma_{2},Q_{1}\times
Q_{2},q^{1}\times q^{2},\delta,F_{1}\times F_{2})$ where
$(p,p^{\prime})\in\delta((q,q^{\prime}),(l,l^{\prime}))$ iff
$p\in\delta_{1}(q,l)$ and $p^{\prime}\in\delta_{2}(q^{\prime},l^{\prime})$. An
NFA $\mathcal{A}$ is deterministic (called DFA) if for every state $q$ and
letter $a$, $|\delta(q,a)|\leq 1$. Every NFA can be determinized to a DFA that
describes the same language by using the subset construction, possibly with an
exponential blow-up [21]. It is often more convenient for users to specify
regular languages by means of regular expressions, which can be converted to
DFA, possibly with an exponential blow-up as well [21]. We assume here that
all regular languages are specified by means of DFAs, as we wish to study the
inherent complexity of decomposition.

Finally, a transducer (we work here with Moore machines) is a deterministic
finite-state machine with no accepting states, but with additional output
alphabet and an additional function from the set of states to the output
alphabet. Formally in our setting a transducer is a tuple
$T=(\Sigma,\Sigma^{\prime},Q,\delta,q_{0},Out)$ where $\Sigma$ is a finite
alphabet and $\Sigma^{\prime}$ is a finite output alphabet, $Q$ is a finite
set of states with an initial state $q_{0}\in Q$, $\delta:Q\times\Sigma\to Q$
is the transition function and $Out:Q\to\Sigma^{\prime}$ is the output
function. Transducers describe finite-state functions from input words in
$\Sigma^{*}$ to output words in $\Sigma^{\prime*}$. We define
$\delta(\varepsilon)=q_{0}$ and $T(\varepsilon)=Out(q_{0})$. Inductively,
$\delta(wa)=\delta(\delta(w),a)$ and $T(wa)=T(w)\cdot Out(\delta(wa))$, for
$\in\Sigma*$ and $a\in\Sigma$.

##  4\. Problem definition

The concept of decompositions that we explore here is related to systems that
can be defined by their given input and produced output. We model these as an
input domain $\mathcal{I}$ and an output domain $\mathcal{O}$, not necessarily
finite. Our description of a system is a specification that associates inputs
to outputs, and is modeled as a relation
$R\subseteq\mathcal{I}\times\mathcal{O}$ [20, 39]. In addition we assume a
constraint in form of a domain with a specific size that directs the
decomposition to be more concise and is given as an intermediate domain
$\mathcal{B}$. The objective is to decompose $R$ into relations
$R_{1}\subseteq\mathcal{I}\times\mathcal{B}$, and
$R_{2}\subseteq\mathcal{B}\times\mathcal{O}$ such that the composition
$R_{1}\circ R_{2}$ has either of the following properties: (i) no input-output
association is added or lost - this problem is called the Total Decomposition
Problem (TDP), or (ii) a more relaxed version, called the Partial
Decomposition Problem (PDP) in which no input-output association is added, but
we are allowed to lose some of the output as long as each input can be
resolved.

To make the paper more fluent to read we use the notation TDP/PDP for
statements that are valid to the TDP and the PDP variants respectively. Since
the size of the intermediate domain $\mathcal{B}$ can be significantly smaller
than the size of the input or output domains, the problem becomes non-trivial
as some sort of compression is required in order to solve the TDP/PDP. The
actual problems of TDP/PDP are appropriately defined for each section as
decision problems. We first define the TD/PD conditions as follows.

(TD/PD conditions) Given binary relations
$R\subseteq\mathcal{I}\times\mathcal{O}$,
$R_{1}\subseteq\mathcal{I}\times\mathcal{B}$, and
$R_{2}\subseteq\mathcal{B}\times\mathcal{O}$ for some domains
$\mathcal{I},\mathcal{O},\mathcal{B}$, we say that $(R_{1},R_{2})$ meets the
TD condition if $Img(R_{1})\subseteq Dom(R_{2})$ and $R_{1}\circ R_{2}=R$. We
say that $(R_{1},R_{2})$ meets the PD condition if $Img(R_{1})\subseteq
Dom(R_{2})$, $Dom(R_{1}\circ R_{2})=Dom(R)$, and $R_{1}\circ R_{2}\subseteq
R$.

The decision problem of TDP/PDP, formally defined for diverse settings, is:
given a description of domains and a relevant relation $R$, find whether there
exist $(R_{1},R_{2})$ that meets the TD/PD condition.

Since the type of domains and relations that we explore varies between an
explicit and a more implicit description of relations, the formal definitions
of the problem change according to these representations, and so are the
sought decomposed relations. It is important to note that the TD/ PD
conditions are properties of the actual relations, and not of the description
in which the relations are represented.

Note that PDP without the restriction of $Dom(R_{1}\circ R_{2})=Dom(R)$
becomes trivial, as one can take the empty sets as $R_{1}$ and $R_{2}$.

The following technical fact can help prove TD/PD conditions in various
settings.

Assume $Img(R_{1})\subseteq Dom(R_{2})$. Then $Dom(R_{1}\circ
R_{2})=Dom(R_{1})$ (and therefore $Dom(R)=Dom(R_{1})$).

###### Proof.

Let $i\in Dom(R_{1}\circ R_{2})$. Then there is $o\in\mathcal{O}$ such that
$(i,o)\in R_{1}\circ R_{2}$. Which means there is $b\in\mathcal{B}$ such that
$(i,b)\in R_{1}$ and $(b,o)\in R_{2}$. Specifically there is $b\in\mathcal{B}$
such that $(i,b)\in R_{1}$, therefore $i\in Dom(R_{1})$. Next let $i\in
Dom(R_{1})$. Then there is $b\in\mathcal{B}$ such that $(i,b)\in R_{1}$. Since
$Img(R_{1})\subseteq Dom(R_{2})$, we have that $b\in Dom(R_{2})$ therefore
there is $o\in\mathcal{O}$ such that $(b,o)\in R_{2}$. Therefore since
$(i,b)\in R_{1}$ and $(b,o)\in R_{2}$ then $(i,o)\in R_{1}\circ R_{2}$ which
makes $i\in Dom(R_{1}\circ R_{2})$. ∎

Finally see that the decomposed relations that meet the TD conditions, also
meet the PD conditions on the same input, therefore a positive answer to TDP
implies a positive answer to PDP.

##  5\. Decomposition is hard

Decomposition has been advocated as the first step in the design of complex
systems, with the intuition that it is easier to design components separately,
rather than design a complex monolithic system. We show in this section
several settings in which finding a sequential decomposition is
computationally hard. This means that while sequential decomposition could be
used to simplify the complexity of the initial specification, such
decomposition itself is intractable, thus can be viewed as a ”No-Free-Lunch”.

###  5.1. Explicit relations

The simplest case of decomposition is when the domains
$\mathcal{I},\mathcal{O}$ and $\mathcal{B}$ are finite and given explicitly as
a part of the input, and the relation $R$ is given explicitly as a table in
$\mathcal{I}\times\mathcal{O}$.

######  Problem 1.

(TDP/PDP on explicit relations) We are given a tuple
$I=(\mathcal{I},\mathcal{O},\mathcal{B},R)$ where
$\mathcal{I},\mathcal{O},\mathcal{B}$ are finite domains and
$R\subseteq\mathcal{I}\times\mathcal{O}$. The problem is whether there exist
relations $R_{1}\subseteq\mathcal{I}\times\mathcal{B}$ and
$R_{2}\subseteq\mathcal{B}\times\mathcal{O}$ such that $(R_{1},R_{2})$ meet
the TD/PD conditions.

If $|\mathcal{B}|\geq|\mathcal{I}|$ or $|\mathcal{B}|\geq|\mathcal{O}|$ then
TDP has a positive solution (and therefore PDP as well) and the relations that
solve TDP can be found in a linear time to the size of the input.

######  Proof 5.1.

Assume that $|\mathcal{B}|\geq|\mathcal{O}|$ (the other case is analogue).
Then we can define $R_{2}=\\{(g(o),o)\mid o\in\mathcal{O}\\}$ where
$g:\mathcal{O}\to\mathcal{B}$ is any injection. Then for TDP,
$R_{1}=\\{(i,b)\mid(i,o)\in R\text{ and }b=g(o)\\}$ is a relation that
satisfies $R_{1}\circ R_{2}=R$.

Therefore TDP/PDP become non-trivial when $|\mathcal{B}|$ is strictly smaller
than $|\mathcal{I}|$ and $|\mathcal{O}|$.

Let $\mathcal{I}=\\{i_{1},i_{2}\\},\mathcal{B}=\\{b\\}$, and
$\mathcal{O}=\\{o_{1},o_{2}\\}$. Let $R=\\{(i_{1},o_{1}),(i_{2},o_{2})\\}$.
Then the answer to TDP is negative as every non-empty composition of relations
$R_{1}\circ R_{2}$ with $Dom(R_{1}\circ R_{2})=Dom(R)$, must also include
$(i_{1},o_{2})$ or $(i_{2},o_{1})$.

We next show that even for the explicit setting, TDP/PDP are computationally
hard, that is NP-complete. On a positive note, being in NP, solutions for
TDP/PDP can be sought by various techniques such as reduction to SAT, then
using SAT solvers.

######  Theorem 2.

TDP/PDP on explicit relations are NP-complete.

######  Proof 5.2.

TDP on explicit relations is NP-complete. To see that TDP is in NP, guess
$R_{1},R_{2}$ and verify the TD conditions. We show hardness by a reduction
from the NP-complete problem: Covering by Complete Bipartite Subgraphs (CCBS)
(Problem GT18 at [18]). In the CCBS we are given a bipartite graph $G$ and
$k>0$, and the problem is whether $G$ can be covered by $k$ complete bipartite
subgraphs.

Given a CCBS instance $G=(V_{1},V_{2},E)$ and $k>0$ we define a TDP instance
with $\mathcal{I}=V_{1}$ and $\mathcal{O}=V_{2}$ (w.l.o.g. every vertex in
$V_{1}$ and in $V_{2}$ has an incident edge). Set $R=E$ and add the
$\mathcal{B}$ elements $\mathcal{B}=\\{u_{1},\cdots u_{k}\\}$. Suppose there
is a solution $(R_{1},R_{2})$ to TDP. For every $1\leq i\leq k$ let
$V_{1}^{i}=\\{v\in V_{1}|(v,u_{i})\in R_{1}\\}$, and let $V_{2}^{i}=\\{v\in
V_{2}\mid(u_{i},v)\in R_{2}\\}$. From the TD conditions it follows that
$(v,v^{\prime})\in R$ for every $v\in V_{1}^{i},v^{\prime}\in V_{2}^{i}$.
Furthermore, for every $(v,v^{\prime})\in R$ there is $1\leq i\leq k$ such
that $v\in V_{1}^{i},v^{\prime}\in V_{2}^{i}$. Since $E=R$, then
$\\{(V_{1}^{i},V_{2}^{i})\mid 1\leq i\leq k\\}$ is a collection of complete
bipartite subgraphs that covers $G$.

Next, assume there is a solution $\\{(V_{1}^{i},V_{2}^{i})\mid 1\leq i\leq
k\\}$ to the CCBS. Then define $R_{1}=\bigcup_{i\leq k}\\{(v,u_{i})\mid v\in
V_{1}^{i}\\}$ and $R_{2}=\bigcup_{i\leq k}\\{(u_{i},v)\mid v\in V_{2}^{i}\\}$.
Then $R_{1}\subseteq\mathcal{I}\times\mathcal{B}$,
$R_{2}\subseteq\mathcal{B}\times\mathcal{O}$ and $Img(R_{1})\subseteq
Dom(R_{2})$. To see that $R_{1}\circ R_{2}=R$, let $(v,v^{\prime})\in
R_{1}\circ R_{2}$. Then there is $u_{i}$ such that $(v,u_{i})\in
R_{1},(u_{i},v)\in R_{2}$, so $(v,v^{\prime})\in(V_{1}^{i},V_{2}^{i})$,
therefore $(v,v^{\prime})\in R$. On the other hand let $(v,v^{\prime})\in R$.
Since the solution to CCBS covers $G$, there is $i\leq k$ such that
$(v,v^{\prime})\in(V_{1}^{i},V_{2}^{i})$, so $(v,u_{i})\in R_{1}$ and
$(u_{i},v^{\prime})\in R_{2}$, hence $(v,v^{\prime})\in R_{1}\circ R_{2}$.

PDP on explicit relations is NP-complete. Membership in NP is easily shown. We
show hardness by reduction from Set Cover (Problem SP5 in [18]). In Set Cover
we are given a set of elements $S=\\{a_{1},\cdots a_{n}\\}$, a set of subsets
of $S$, $C=\\{c_{1},\cdots c_{m}\\}$ and $k\geq 0$. The problem is whether
there are $k$ sets from $C$ whose union covers $S$. We assume w.l.o.g. that
every member of $S$ belongs to at least one member of $C$. Given an instance
$I=(S,C,k)$ of Set Cover, define a PDP instance $I^{\prime}$ where
$\mathcal{I}=S$, $\mathcal{O}=C$ , $R=\\{(a,c)\mid a\in c\\}$ and add the
intermediate domain elements to be $\mathcal{B}=\\{b_{1},\cdots b_{k}\\}$.
Assume that there is a set cover $\\{c_{i_{1}},\cdots c_{i_{k}}\\}\subseteq C$
for $S$. Then construct $R_{1},R_{2}$ as follows. For every element $a$ and
$j\leq k$, set $(a,b_{j})\in R_{1}$ iff $c_{i_{j}}$ is the first set for which
$a\in c_{i_{j}}$. In addition set $(b_{j},c_{i_{j}})\in R_{2}$. Then
$R_{1}\subseteq\mathcal{I}\times\mathcal{B}$,
$R_{2}\subseteq\mathcal{B}\times\mathcal{O}$ and $Img(R_{1})\subseteq
Dom(R_{2})$. Since the set cover for $S$ covers all elements of $S$, we have
that $Dom(R_{1}\circ R_{2})=Dom(R)$. To see that $R_{1}\circ R_{2}\subseteq
R$, let $(a,c_{i_{j}})\in R_{1}\circ R_{2}$ for some $j\leq k$. Then
$(a,b_{j})\in R_{1}$ and $(b_{j},c_{i_{j}})\in R_{2}$. By definition of
$R_{1}$, $a\in c_{i_{j}}$, therefore we have that $(a,c_{i_{j}})\in R$.

Next, assume $I^{\prime}$ has a PDP solution with relations $(R_{1},R_{2})$.
Define a set cover as follows. For every $b_{j}\in Img(R_{1})$ (and therefore
$b_{j}\in Dom(R_{2})$), choose a single element $c_{i_{j}}\in
Img_{b_{j}}(R_{2})$ and set $c_{i_{j}}\in C^{\prime}$. Then $|C^{\prime}|\leq
k$. To see that $C^{\prime}$ is a set cover for $S$, let $a\in\mathcal{I}$.
Then since $a\in Dom(R)$ and $Dom(R_{1}\circ R_{2})=Dom(R)$, there is
$c\in\mathcal{O}$ such that $(a,c)\in R_{1}\circ R_{2}$. Therefore there is
$b_{j}\in\mathcal{B}$ such that $(a,b_{j})\in R_{1}$ and by definition
$(b_{j},c_{i_{j}})\in R_{2}$, which means $(a,c_{i_{j}})\in R_{1}\circ R_{2}$
as well. Since $R_{1}\circ R_{2}\subseteq R$ then $(a,c_{i_{j}})\in R$ which
means $a\in c_{i_{j}}$. As $c_{i_{j}}\in C^{\prime}$ our proof is complete.

###  5.2. Symbolic relations

In Section 5.1, the input relation is described explicitly. In many cases,
however, although finite, the relation is too large to be described
explicitly, and it makes more sense to describe it symbolically. Specifically,
the domains are given as the set of all truth assignments over sets of Boolean
variables, and the relation is described symbolically. Such representations
have been studied in the literature, where they are often referred to as
succinct representations, since they allow for a polynomial-size description
of exponential-size domains and relations. In this section we explore a
standard encoding in which the relation is described as a Boolean circuit, as
in [11, 4]. Other symbolic encodings studied in the literature are Boolean
formulas [45], and BDDs [14].

In general, a succinct representation (also called circuit description in our
setting) of a binary word $w$ is a boolean circuit that on input $i$ in binary
emits two boolean values $x,y$ as an output: $x=1$ iff $i\leq|w|$, and if
$x=1$ then $y$ is the $i$’th bit of $w$ [4]. In that sense the circuit
description of an integer $k$ is a boolean circuit that on input $i$ in binary
emits $1$ iff $i\leq k$, and the circuit description of a binary relation $R$
of natural numbers is a boolean circuit $C_{R}$ that on input $(i,j)$ in
binary decided whether $(i,j)$ belongs to $R$. As such, the circuit
description of a language $A$ is defined to be the set of all circuits that
succinctly describe words in $A$ [4]. For more about circuit description, see
[17, 4, 37].

######  Problem 3.

(TDP/PDP for symbolic relations) We are given a tuple
$I=(n_{\mathcal{I}},n_{\mathcal{O}},n_{\mathcal{B}},C_{R})$ where
$n_{\mathcal{I}},n_{\mathcal{O}},n_{\mathcal{B}}$ are natural numbers, and
$C_{R}$ is a circuit description of a relation
$R\subseteq\mathcal{I}\times\mathcal{O}$ where $\mathcal{I}=\\{0,1\\}^{n_{I}}$
and $\mathcal{O}=\\{0,1\\}^{n_{O}}$. The problem is whether there exist
relations $R_{1}\subseteq\mathcal{I}\times\mathcal{B}$ and
$R_{2}\subseteq\mathcal{B}\times\mathcal{O}$, where
$\mathcal{B}=\\{0,1\\}^{n_{\mathcal{B}}}$, such that $(R_{1},R_{2})$ meet the
TD/PD conditions.

Note that since the domains $\mathcal{I},\mathcal{B},\mathcal{O}$ are finite,
the requirement for TDP/PDP for symbolic relation can equivalently be to find
whether there exists circuits $C_{R_{1}},C_{R_{2}}$ that describe relations
$R_{1}\subseteq\mathcal{I}\times\mathcal{B}$ and
$R_{2}\subseteq\mathcal{B}\times\mathcal{O}$, such that $(R_{1},R_{2})$ meet
the TD/PD conditions.

For TDP/PDP, as in Claim 5.1, the problem becomes trivial when
$n_{\mathcal{B}}\geq\min\\{n_{\mathcal{I}},n_{\mathcal{O}}\\}$. Note that a
variant of PDP, in which the required relations in the solution are functions
can be viewed as an instance of the problem of Boolean functional synthesis,
e.g. [16, 9].

We next show that TDP/PDP are NEXPTIME-complete. We obtain this result by
applying the computational-complexity theory of succinct-circuit
representations for ”logtime” reductions [4] to the NP-hardness reductions
described in Section 5.1. We describe this in details.

A reduction from a language $A\subseteq\Sigma^{*}$ to a language
$B\subseteq\Sigma^{*}$, for a finite alphabet $\Sigma$, is a function
$f:A\rightarrow B$ such that $x\in A$ iff $f(x)\in B$. The function $f$ is
called a logtime reduction if the $i$-th symbol of $f(x)$ can be computed in a
time logarithmic in the size of $x$. This is done by using a so called
“direct-input-access” Turing machine, which has a specific “index” tape in
which a binary index $i$ is written and then the $i$-th symbol of the input
string $x$ is computed. See [4], which also states a generalization of the
following:

######  Theorem 4.

_(Balcazar, Lozano, Toran[4])_ For every language $B\subseteq\Sigma^{*}$, if
$B$ is NP-hard under logtime reducibility, then the succinct representation of
$B$ is
NEXPTIME-hard under polynomial-time reducibility.

Since ”standard” NP-hard problems (under polynomial-time reducibility) tend to
be NP-hard also under logtime reducibility, the crux of Theorem 4 is that a
succinct representation of a given problem in a form of a circuit does not
necessarily ease the complexity of solving the problem.

From Theorem 4 we get:

######  Theorem 5.

TDP/PDP for symbolic relations are NEXPTIME-complete.

######  Proof 5.3.

First see that an equivalent formulation of the TDP/PDP on symbolic relation
is the following: We are given a circuit $C_{I}$ that describes a word that
encodes a tuple $I=(n_{\mathcal{I}},n_{\mathcal{O}},n_{\mathcal{B}},R)$ where
$n_{\mathcal{I}},n_{\mathcal{O}},n_{\mathcal{B}}$ are natural numbers, and $R$
is a relation $R\subseteq\mathcal{I}\times\mathcal{O}$ where
$\mathcal{I}=\\{0,1\\}^{n_{I}}$ and $\mathcal{O}=\\{0,1\\}^{n_{O}}$. The
problem is then whether there exist relations
$R_{1}\subseteq\mathcal{I}\times\mathcal{B}$ and
$R_{2}\subseteq\mathcal{B}\times\mathcal{O}$, where
$\mathcal{B}=\\{0,1\\}^{n_{\mathcal{B}}}$, such that $(R_{1},R_{2})$ meet the
TD/PD conditions. Note that such a formulation is a succinct representation of
TDP/PDP for explicit relation in which the domains are
$\mathcal{I}=\\{0,1\\}^{n_{\mathcal{I}}}$, and
$\mathcal{O}=\\{0,1\\}^{n_{\mathcal{O}}}$. Membership in NEXPTIME is easily
shown since the explicit variant can be obtained from the circuit
representation in exponential time and both explicit TDP/PDP are in NP. In
addition, as we next show, we can use this formulation to prove hardness by
showing that each of the reductions in a chain of reductions from SAT to
explicit TDP or to explicit PDP, is a logtime reduction, and then use Theorem
4 to show NEXPTIME hardness for succinct TDP/PDP. For self containment of the
paper we added in Appendix A the definitions of the languages mentioned below
along with the relevant reductions and references.

For languages $A$ and $B$, we use the notations $A\leq^{P}_{m}B$ to denote
that $A$ is polynomial-time reduced to $B$. We have that
$SAT\leq^{P}_{m}3SAT\leq^{P}_{m}KCOLORABILITY\leq^{P}_{m}\newline
PARTITIONCLIQUES\leq^{P}_{m}CCBS\leq^{P}_{m}TDP$, where all the reductions are
described in Appendix A apart from the last reduction which is Theorem 2 from
this paper. Similarly, we have that
$SAT\leq^{P}_{m}CLIQUE\leq^{P}_{m}VC\leq^{P}_{m}SC\leq^{P}_{m}PDP$ where all
the reductions are described in Appendix A, the last reduction is again from
Theorem 2.

As every problem $A$ is a set of binary strings (words) $x$, and as every
reduction from $A$ to $B$ is a function $f$ such that $x\in A$ iff $f(x)\in
B$, we have that the reductions described above are standard in the sense that
only a few bits are required from $x$ in order to determine the identity of
the $j$’th bit of $f(x)$. For example, in the reduction from $3SAT$ to
$CLIQUE$, the output is a binary string that represents an adjacency matrix of
a graph of size polynomial to the size of the input (and this size can be
found in logarithmic time, see [4]). The content of every cell $(i,j)$ of that
matrix can be determined by whether two satisfying assignments to 3SAT, one
for a certain clause $c$ and one for a certain clause $c^{\prime}$ in the
input share the same variable (see [24] for more details). In this reduction,
the output formula is standard, in the sense that the location of the clauses
$c,c^{\prime}$ in the input string is easily found. As such, determining a
certain output bit requires only a small (logarithmic) access to the input
string, followed by a small (also logarithmic) comparison of the obtained
input process. Similarly, the Cook-Levin reduction from any NP problem to
$SAT$ is standard in that sense as well, and therefore the output as the SAT
formula can be obtained from logarithmic input and comparison. See [18] for
more details.

To show that the reductions from $CCBS$ to $TDP$ and from $SC$ to $PDP$ are
logtime reductions, we need to be more accurate in the encoding of TDP/PDP.
Indeed we can encode all problems as an adjacency matrix of the relation
$R\subseteq\mathcal{I}\times\mathcal{O}$ in addition to $k\geq 0$ (in unary)
that describes the size of the intermediate domain $\mathcal{B}$. The input
for $CCBS$ is encoded as an adjacency matrix and some $k\geq 0$. A standard
encoding for $SC$ is also as an adjacency matrix (where the cell $(i,j)=1$ iff
the element $a_{i}$ is a member of the set $c_{j}$) and some $k\geq 0$. As
such, these reductions leave the input as is, since the difference between the
instances of TDP/PDP, $CCBS$ and $SC$ is only in the semantics.

All in all we have that (i) $SAT$ is NP-hard under logtime reductions, and
(ii) every reduction described above is a logtime reduction. The Conversion
Lemma from [4] states that if a language $A$ is logtime reduced to a language
$B$ then the circuit representation of $A$ is polynomial-time reduced to the
circuit representation of $B$. Therefore although the composition of two
logtime reductions is not necessarily a logtime reduction, by using the
Conversion Lemma from [4] we have that this chain of reductions for the
succinct versions of the languages holds under polynomial-time reduction.
Therefore by transitivity of polynomial-time reductions we get that TDP/PDP is
NEXPTIME hard.

As a side note, that may also serve as a suggestion as an alternative proog,
see that the definitions of logtime reductions and the Conversion Lemma from
[4] can be easily extended to poly-logtime reduction, that preserve
transitivity and as can serve as an alternative proof.

###  5.3. Automatic relations

In many applications we need to consider input and output as streams of
symbols, with some desired relation between the input stream and the output
stream. The most basic description for such systems, the one that we explore
in this work, is when the domains are (possibly infinite) sets of finite words
over finite alphabets, and the given relation is a regular language, given as
a deterministic finite automaton (DFA), over the product alphabet of the input
and output domains. The setting that we consider in this paper is of automatic
relations, which are relations that are described by automata as defined
below. Automatic relations provide a context for a rich theory of automatic
structures, cf. [25, 42], with a solvable decision for first-order logic. We
follow here the convention in _regular model checking_ , cf. [8], where
_length-preserving_ automatic relations, with input and output symbols
interleaved, are used as input/output specifications for each step of reactive
systems. (Thus, unlike the definitions in [25, 42], we do not allow padding.)

Given finite alphabets $\Sigma,\Sigma^{\prime}$ with domains
$D\subseteq\Sigma^{*}$, $D^{\prime}\subseteq\Sigma^{\prime*}$, and a relation
$R\subseteq D\times D^{\prime}$, we say that a DFA $\mathcal{A}_{R}$ over the
alphabet $(\Sigma\times\Sigma^{\prime})$ describes $R$ if:
$(\vec{d},\vec{d}^{\prime})\in L(\mathcal{A}_{R})$ if and only if
$(\vec{d},\vec{d}^{\prime})\in R$ . Note the slight abuse of notation as
$L(\mathcal{A}_{R})$ describes words in $(\Sigma\times\Sigma^{\prime})^{*}$
while $R$ describes words in $\Sigma^{*}\times\Sigma^{\prime*}$. Thus, we
assume that input and output streams have the same lengths, that is,
$(\vec{d},\vec{d}^{\prime})\in R$ implies that $|\vec{d}|=|\vec{d^{\prime}}|$.

######  Problem 6.

(TDP/PDP for automatic relations) We are given a tuple
$I=(\Sigma_{\mathcal{I}},\Sigma_{\mathcal{B}},\Sigma_{\mathcal{O}},\mathcal{A}_{R})$,
where $\Sigma_{\mathcal{I}}$, $\Sigma_{\mathcal{B}}$, and
$\Sigma_{\mathcal{O}}$ are finite alphabets, and $\mathcal{A}_{R}$ is a DFA
that describes a relation
$R\subseteq\Sigma_{\mathcal{I}}^{*}\times\Sigma_{\mathcal{O}}^{*}$. The
problem is whether there exist DFAs $\mathcal{A}_{R_{1}},\mathcal{A}_{R_{2}}$
that describe relations
$R_{1}\subseteq\Sigma_{\mathcal{I}}^{*}\times\Sigma_{\mathcal{B}}^{*}$ and
$R_{2}\subseteq\Sigma_{\mathcal{B}}^{*}\times\Sigma_{\mathcal{O}}^{*}$ such
that $(R_{1},R_{2})$ meet the TD/PD conditions.

As in the explicit and symbolic cases, the problem becomes non trivial for
TDP/PDP only when
$|\Sigma_{\mathcal{B}}|<\min\\{|\Sigma_{\mathcal{I}}|,|\Sigma_{\mathcal{O}}|\\}$.
While TDP/PDP in the symbolic setting can be solved by reduction to the
explicit setting, this cannot be done here as the domains are possibly
infinite. Indeed, automatic-relation TDP/PDP seems to be a challenging
problem. We next conjecture that automatic-relation TDP/PDP is undecidable and
explain the motivation for this conjecture and why an automata-theoretic
approach may not be helpful for TDP/PDP. We then show that even for the most
basic case, in which the given relation is the equality relation, TDP/PDP can
already be viewed as an algorithmic problem in automata that is equivalent to
the Positivity Problem whose decidability is still open [44, 35]. Then, we
show that for an intermediate alphabet that is of size of power of $2$,
TDP/PDP on automatic relations can be reduced to TDP/PDP on binary
intermediate alphabet. Finally we show by an automata-theoretic approach that
a “strategic” variant of PDP, in which the required relations are in form of
transducers, is decidable, and in fact is in EXPTIME.

####  5.3.1. An undecidability conjecture for TDP/PDP

A notable positive result about automatic relations is the decidability of
their first-order theories [25, 42]. TDP/PDP are essentially second-order
problems–we ask for the existence of $R_{1}$ and $R_{2}$ under the TDP/PDP
conditions. Since there are second-order problems over automatic relations
that are known to be undecidable; for example, checking the existence of an
Hamiltonian path in an automatic graph [30], our conjecture is that this
problem is undecidable as well. We provide here intuition to justify this
conjecture.

######  Conjecture 7.

TDP/PDP for automatic relations is undecidable.

To support the claim of how non-trivial the decomposition problem is, we
consider a more simple and abstract variant of automatic TDP. We consider a
very simple case in which the given automatic relation is trivial, and the
intermediate alphabet is binary. We do not even require the decomposed
relations $R_{1},R_{2}$ to be realized by automata, although we do require the
length of every matching words in $R_{1}$ and $R_{2}$ to be the same.
Specifically, given a regular language $L$ over $\Sigma_{\mathcal{I}}^{*}$,
let $R^{=}_{L}\subseteq(\Sigma_{\mathcal{I}}\times\Sigma_{\mathcal{I}})^{*}$
be the equality relation over $L$. i.e. $R^{=}_{L}=\\{(w,w)\mid w\in L\\}$.
Given $L$ over $\Sigma_{\mathcal{I}}^{*}$ and
$\Sigma_{\mathcal{B}}=\\{0,1\\}$, we ask whether there are relations
$(R_{1},R_{2})$ that meet the TD conditions with respect to $R^{=}_{L}$.

First see that we can assume w.l.o.g. that $(R_{1},R_{2})$ are functions since
existence of such relations leads to existence of such functions. Next, note
that $R_{1}$ cannot relate two distinct words in $L$ to the same word in
$\Sigma_{\mathcal{B}}^{*}$. This is because otherwise a word from
$\Sigma_{\mathcal{B}}^{*}$ has to meet two distinct $\Sigma_{\mathcal{I}}^{*}$
elements, thus either break the equality property or break the TDP property.
Therefore we have that $R_{1}$ is an injection from $L$ to
$\Sigma_{\mathcal{B}}^{*}$. As such, finding an $R_{1}$ that is such an
injection also gives us $R_{2}=R_{1}^{-1}$.

Let $L_{n}$ be the words in $L$ of size $n$. Note that if there is $n$ for
which $|L_{n}|>2^{n}$ then no such $R_{1}$ can be found. If, however, for
every $n$ we have $|L_{n}|\leq 2^{n}$ then a function $R_{1}$ can be simply
realized by ordering the words in every $L_{n}$ in lexicographic order and
relating each one to the $\Sigma_{\mathcal{B}}^{n}$ word that encodes the
index in binary.

Therefore the problem of TDP in this setting is reduced to the following
problem: given a regular language $L$ over a finite alphabet $\Sigma$, where
for every $n$, $L_{n}$ is the set of words in $L$ of size $n$, does
$|L_{n}|\leq 2^{n}$ for every $n$? We call this problem the _The Exponential-
Bound Problem_ (EBP). The following theorem, however, shows that EBP is
equivalent to the problem of Positivity, described below, whose decidability
has been famously open for decades [44, 35]. By equivalent, we mean that there
is a many-to-one reduction from EBP to Positivity and vica versa. Although
this is not a direct reduction to automatic TDP, this relation indicates the
hardness of solving automatic TDP on even a simple relation.

A _linear recurrence sequence_ (LRS) is a sequence of integers $\langle
u_{n}\rangle_{n=0}^{\infty}$ satisfying a recurrence relation: there exist
integer constants $a_{1},a_{2},\ldots,a_{d}$ such that, for all $n\geq 0$,
$u_{n+d}=a_{1}u_{n+d-1}+a_{2}u_{n+d-2}+\ldots+a_{d}u_{n}$ (we say that such a
sequence has _order_ $d$.) If the initial values $u_{0},\ldots,u_{d-1}$ of the
sequence are provided, the recurrence relation defines the rest of the
sequence uniquely. Given a linear recurrence sequence (LRS) $\langle
u_{n}\rangle_{n=0}^{\infty}$, the _Positivity Problem_ asks whether all terms
of the sequence are non-negative. We next show that EBP and Positivity are
equivalent. Thus the decidability of one problem implies the decidability of
the other.

We begin by recalling a useful technical result about LRSs, whose proof can be
found in [2]:

######  Proposition 8 (Cor. 4, [2]).

Let $\langle u_{n}\rangle_{n=0}^{\infty}$ be an integer LRS of order $d$. Then
there exists a rational stochastic matrix $M$, of dimension $4d+5$, such that
for all $n\geq 0$, we have

$u_{n}\leq 0\quad\mbox{iff}\quad(M^{2n+1})_{1,2}\leq\frac{1}{4}\,.$

Moreover, as noted in the comments following Corollary 4 in [2], $M$ can be
chosen so that its entries are dyadic rationals, i.e., having denominator some
power of $2$.

(Technically speaking, the proof of Corollary 4 in [2] constructs a dyadic-
rational stochastic matrix $\widetilde{Q}$ such that $u_{n}\leq 0$ iff
$(\widetilde{Q}^{2n+1})_{1,4d+3}\leq 1/4$. The desired matrix $M$ is then
immediately obtained from $\widetilde{Q}$ by interchanging rows $2$ and
$4d+3$, and interchanging columns $2$ and $4d+3$.)

We are now in a position to proceed with our equivalence:

######  Theorem 9.

EBP is Equivalent to Positivity.

######  Proof 5.4.

We first show that Positivity reduces to EBP. Let $\langle
u_{n}\rangle_{n=0}^{\infty}$ be an LRS of order $d$; we show how positivity
for the sequence $\langle-u_{n}\rangle_{n=0}^{\infty}$ can be formulated as an
EBP problem. To this end, we invoke Prop. 8 to obtain a stochastic matrix $M$
of dimension $4d+5$, all of whose entries are dyadic rationals, and such that,
for all $n\geq 0$,

$(M^{2n+1})_{1,2}\leq\frac{1}{4}\quad\mbox{iff}\quad u_{n}\leq
0\quad\mbox{iff}\quad-u_{n}\geq 0\,.$ (1)

In other words the positivity of $\langle-u_{n}\rangle_{n=0}^{\infty}$ is
violated iff there is some $n$ such that the $(1,2)$-_th_ entry of $M^{2n+1}$
is strictly larger than $1/4$.

Let $2^{p}$ be the largest power appearing among the denominators of the
entries of $M$. Write $J=2^{p}M$ and $N=(2^{p}M)^{2}$. Then $J$ and $N$ are
square matrices with non-negative integer coefficients, and hence there is
some DFA $\mathcal{A}$ such that $(J\cdot N^{n})_{1,2}$ is the number of words
of length $n+1$ accepted by $\mathcal{A}$. More precisely, $\mathcal{A}$ has
initial state $s$, and $4d+5$ further states $q_{1},\ldots,q_{4d+5}$. The
single accepting state is $q_{2}$. To define the transition function, if the
$(1,j)$-_th_ entry of $J$ is $\ell$, then we postulate $\ell$ transitions
going from state $s$ to state $q_{j}$, each labelled with a new (fresh)
letter. Likewise, if the $(i,j)$-_th_ entry of $N$ is $\ell$, then we include
$\ell$ transitions going from $q_{i}$ to $q_{j}$, again for each one using a
new letter as label. In this way, $J$ and $N$ can be viewed as the adjacency
matrices of the underlying directed multigraph of $\mathcal{A}$, and $(J\cdot
N^{n})_{1,2}$ counts the number of paths in $\mathcal{A}$ going from $s$ to
$q_{2}$ in $n+1$ steps. Since by construction, different paths give rise to
different words, $(J\cdot N^{n})_{1,2}$ does indeed correspond to the number
of words of length $n+1$ accepted by $\mathcal{A}$.

Writing $L(\mathcal{A})=L$, Eq. (1) becomes, for all $n\geq 0$,

$L_{n+1}\leq\frac{2^{p}2^{2pn}}{4}=\frac{2^{2p(n+1)}}{2^{p+2}}\quad\mbox{iff}\quad-
u_{n}\geq 0\,.$ (2)

We now modify the automaton $\mathcal{A}$ by lengthening every transition in
$\mathcal{A}$ by a factor of $2p$; more precisely, for every transition
$q\rightarrow q^{\prime}$, create $2p-1$ fresh non-accepting states
$r_{1},\ldots,r_{2p-1}$ and replace $q\rightarrow q^{\prime}$ by the sequence
$q\rightarrow r_{1}\rightarrow r_{2}\rightarrow\ldots\rightarrow
r_{2p-1}\rightarrow q^{\prime}$, all labelled with the same letter as the
original transition. The initial and accepting states otherwise remain
unchanged. Let us call the resulting DFA $\mathcal{A}^{\prime}$, with accepted
language $L(\mathcal{A}^{\prime})=L^{\prime}$. In moving from $\mathcal{A}$ to
$\mathcal{A}^{\prime}$, the net effect has been to increase the length of
every accepted word by a factor of $2p$; note also that if $m$ is not a
multiple of $2p$, then $L^{\prime}_{m}=0$.

Combining the above with Eq. (2), we conclude that the LRS $\langle-
u_{n}\rangle_{n=0}^{\infty}$ is positive iff for all $m\geq 0$,
$L^{\prime}_{m}\leq\frac{2^{m}}{2^{p+2}}$, i.e., $2^{p+2}L^{\prime}_{m}\leq
2^{m}$.

Inflating the alphabet size of $\mathcal{A}^{\prime}$ by a factor of
$2^{p+2}$, we can easily manufacture a DFA $\mathcal{A}^{\prime\prime}$ with
accepted language $L(\mathcal{A}^{\prime\prime})=L^{\prime\prime}$ having the
property that, for all $m\geq 0$,
$L^{\prime\prime}_{m}=2^{p+2}L^{\prime}_{m}$. It therefore follows that the
LRS $\langle-u_{n}\rangle_{n=0}^{\infty}$ is positive iff for all $m\geq 0$,
$L^{\prime\prime}_{m}\leq 2^{m}$, which completes the reduction of Positivity
to EBP.

Finally, since the sequence obtained from the number of distinct words of
length $n$ accepted by a given automaton is an LRS [36], we have that EBP also
reduces to Positivity, and therefore that the two problems are indeed
equivalent.

####  5.3.2. Reduction to binary alphabet

Since the size of the intermediate alphabet plays a crucial role in the
solution of TDP/PDP, one may ask whether it suffices to search for solutions
for only the binary case. We show that the answer is positive for intermediate
alphabet that is of size of power or $2$. Specifically we show by reduction
that for every automatic TDP/PDP instance
$I=(\Sigma_{\mathcal{I}},\Sigma_{\mathcal{B}},\Sigma_{\mathcal{O}},\mathcal{A}_{R})$,
where $|\Sigma_{\mathcal{B}}|=2^{m}$ for some $m>0$, there is a TDP/PDP
instance
$I^{\prime}=(\Sigma_{\mathcal{I}},\\{0,1\\},\Sigma_{\mathcal{O}},\mathcal{A}_{R^{\prime}})$
for some relation $R^{\prime}$ such that $I$ has a solution if and only if
$I^{\prime}$ has a solution.

To show our reduction, we first need to reason over automatic decomposition in
the regular expressions representation level. Therefore we give below the
following lemma that characterizes a possible TDP/PDP solution as regular
expressions.

######  Lemma 10.

A TDP/PDP for automatic relations instance
$I=(\Sigma_{\mathcal{I}},\Sigma_{\mathcal{B}},\Sigma_{\mathcal{O}},\mathcal{A}_{R})$
has a solution if and only if there is a regular expression
$S\subseteq(\Sigma_{\mathcal{I}}\times\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}})^{*}$
such that the following happens:

  1. (1)

(Only for the TDP variant) For every $(\vec{i},\vec{o})\in R$ there is
$\vec{b}\in\Sigma_{\mathcal{B}}^{*}$ such that $(\vec{i},\vec{b},\vec{o})\in
L(S)$.

  2. (2)

(Only for the PDP variant) For every $\vec{i}\in Dom(R)$ there are
$\vec{b}\in\Sigma_{\mathcal{B}}^{*}$, and $\vec{o}\in\Sigma_{\mathcal{O}}^{*}$
such that $(\vec{i},\vec{b},\vec{o})\in L(S)$.

  3. (3)

(For both variants) For every
$(\vec{i},\vec{b},\vec{o}),(\vec{i}^{\prime},\vec{b}^{\prime},\vec{o^{\prime}})\in
L(S)$, if $\vec{b}=\vec{b}^{\prime}$ then
$(\vec{i},\vec{o^{\prime}}),(\vec{i}^{\prime},\vec{o})\in R$.

######  Proof 5.5.

Assume the instance $I$ has a TDP/PDP solution
$(\mathcal{A}_{R_{1}},\mathcal{A}_{R_{2}})$. Let $\mathcal{A}^{\prime}$ be the
product automata of $\mathcal{A}_{R_{1}}$ and $\mathcal{A}_{R_{2}}$ followed
by eliminating the edges $(i,b,b^{\prime},o)$ where $b\not=b^{\prime}$, and
then eliminating the first alphabet of $\Sigma_{\mathcal{B}}$. Therefore
$\mathcal{A}^{\prime}$ is over the alphabet
$(\Sigma_{\mathcal{I}}\times\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}})$.
Let $S$ be the regular expression that describes $\mathcal{A}^{\prime}$. First
verify (3): let
$(\vec{i},\vec{b},\vec{o}),(\vec{i}^{\prime},\vec{b},\vec{o^{\prime}})\in
L(S)$. Then $(\vec{i},\vec{b}),(\vec{i^{\prime}},\vec{b})\in R_{1}$ and
$(\vec{b},\vec{o}),(\vec{b},\vec{o^{\prime}})\in R_{2}$ which makes
$(\vec{i},\vec{o^{\prime}}),(\vec{i}^{\prime},\vec{o})\in R_{1}\circ R_{2}$,
hence both for TDP/PDP we have
$(\vec{i},\vec{o^{\prime}}),(\vec{i}^{\prime},\vec{o})\in R$. For TDP we
verify (1): Let $(\vec{i},\vec{o})\in R$, then there is $\vec{b}$ such that
$(\vec{i},\vec{b})\in R_{1}$ and $(\vec{b},\vec{o})\in R_{2}$ therefore
$(\vec{i},\vec{b},\vec{o})\in L(S)$. For PDP we verify (2): let $\vec{i}\in
Dom(R)$, then there is $\vec{o}$ such that $(\vec{i},\vec{o})\in R$. Then as
before there is $\vec{b}$ such that $(\vec{i},\vec{b})\in R_{1}$ and
$(\vec{b},\vec{o})\in R_{2}$ therefore $(\vec{i},\vec{b},\vec{o})\in L(S)$.

Next, assume $S$ is a regular expression over
$(\Sigma_{\mathcal{I}}\times\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}})^{*}$
that meets conditions (1)-(3) for the TDP/PDP instance $I$. Let
$\mathcal{A}^{\prime}$ be the automaton that describes $S$. Let
$\mathcal{A}_{1}$ be the automaton obtained from $A^{\prime}$ by eliminating
the $\Sigma_{\mathcal{O}}$ letters and determinizing. Same let
$\mathcal{A}_{2}$ be the automaton obtained from $A^{\prime}$ by eliminating
the $\Sigma_{\mathcal{I}}$ letters and determinizing. Let $R_{1},R_{2}$ be the
regular relations that $\mathcal{A}_{1},\mathcal{A}_{2}$ respectively
describe. We see that $(R_{1},R_{2})$ meet the TD/PD conditions. Let
$\vec{b}\in Img(R_{1})$. Then there is $\vec{i}$ such that $(\vec{i},\vec{b})$
is an accepting word for $\mathcal{A}_{1}$, therefore there exists $\vec{o}$
such that $(\vec{i},\vec{b},\vec{o})$ is accepting for $\mathcal{A}^{\prime}$.
Therefore $(\vec{b},\vec{o})$ is accepting for $\mathcal{A}_{2}$ so
$\vec{b}\in Dom(R_{2})$. For TDP let $(\vec{i},\vec{o})\in R$. Then from
condition (1) there is $\vec{b}\in\Sigma_{\mathcal{B}}^{*}$ such that
$(\vec{i},\vec{b},\vec{o})\in L(S)$, so $(\vec{i},\vec{b},\vec{o})$ is
accepting for $\mathcal{A}^{\prime}$, therefore $(\vec{i},\vec{b})\in R_{1}$,
and $(\vec{b},\vec{o})\in R_{2}$ so $(\vec{i},\vec{o})\in R_{1}\circ R_{2}$.
For PDP, let $\vec{i}\in Dom(R)$. Then from condition (2) there are
$\vec{b},\vec{o}$ such that $(\vec{i},\vec{b},\vec{o})\in L(S)$, so
$(\vec{i},\vec{b},\vec{o})$ is accepting for $\mathcal{A}^{\prime}$, therefore
$(\vec{i},\vec{b})\in R_{1}$, and $(\vec{b},\vec{o})\in R_{2}$ so $\vec{i}\in
Dom(R_{1}\circ R_{2})$. Finally for both TDP/PDP assume $(\vec{i},\vec{o})\in
R_{1}\circ R_{2}$. Then there is $\vec{b}$ such that $(\vec{i},\vec{b})\in
R_{1}$, and $(\vec{b},\vec{o})\in R_{2}$. Then there are
$\vec{i^{\prime}},\vec{o^{\prime}}$ such that
$(\vec{i},\vec{b},\vec{o^{\prime}})$ and $(\vec{i^{\prime}},\vec{b},\vec{o})$
are accepting for $\mathcal{A}^{\prime}$ and therefore in $L(S)$. Then from
condition (3), $(\vec{i},\vec{o})\in R$.

Using Lemma 10, we prove the following theorem.

######  Theorem 11.

Given an instance
$I=(\Sigma_{\mathcal{I}},\Sigma_{\mathcal{B}},\Sigma_{\mathcal{O}},\mathcal{A}_{R})$
where $|\Sigma_{\mathcal{B}}|=2^{m}$ for some $m>0$, there is an instance
$I^{\prime}=(\Sigma_{\mathcal{I}},\\{0,1\\},\Sigma_{\mathcal{O}},\mathcal{A}_{R^{\prime}})$,
constructed from $I$, such that $I$ has a TDP/PDP solution if and only if
$I^{\prime}$ has a TDP/PDP solution.

######  Proof 5.6.

The idea behind the reduction is to encode every letter in
$\Sigma_{\mathcal{B}}$ in binary, and use this encoding for the construction
of $I^{\prime}$. $\mathcal{A}_{R^{\prime}}$ is therefore constructed from
$\mathcal{A}_{R}$ by replacing every edge labeled $(i,o)$ with a path of $m$
edges, each with the same label $(i,o)$.

Let $bin$ be a function in which $bin(b)$ is a binary encoding of the letter
$b\in\Sigma_{\mathcal{B}}$ in $m$ bits, and let $bin_{j}(b)$ be the $j$’th bit
in $bin(b)$. Since $\Sigma_{B}$ is of size $2^{m}$, the function $bin$ is a
bijection. Assume that $I$ has a solution
$(\mathcal{A}_{R_{1}}$,$\mathcal{A}_{R_{2}})$. We first construct an automaton
$\mathcal{A}_{R^{\prime}_{1}}$ over alphabet
$(\Sigma_{\mathcal{I}}\times\\{0,1\\})$ from $\mathcal{A}_{R_{1}}$ by
replacing every edge labeled $(i,b)$ with an $m$-edges path with edge labels
$(i,bin_{0}(b)),\cdots(i,bin_{m-1}(b))$, thus such a path describes the word
$(i^{m},bin(b))$ (where $i^{m}$ is the letter $i$ concatenated $m$ times).
Same, we construct an automaton $\mathcal{A}_{R^{\prime}_{2}}$ over the
alphabet $(\\{0,1\\}\times\Sigma_{\mathcal{O}})$ from $\mathcal{A}_{R_{2}}$ by
replacing every edge labeled $(b,o)$ with an $m$-edges path with edge labels
that describes the word $(bin(b),o^{m})$. Then since $(R_{1},R_{2})$ solve
TDP/PDP for the instance $I$, we have that $(R^{\prime}_{1},R^{\prime}_{2})$
solve TDP/PDP for the instance $I^{\prime}$.

The other side of the proof is more involved since suppose we assume
$(\mathcal{A}_{R^{\prime}_{1}}$, $\mathcal{A}_{R^{\prime}_{2}})$ solve
$I^{\prime}$. Then we cannot guarantee that these automata have an ”$m$-path”
structure that can reverse the construction we have just described. For that,
we define by induction an homomorphism
$h:(\Sigma_{\mathcal{I}}\times\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}})^{*}\to({\Sigma_{\mathcal{I}}}^{m}\times\\{0,1\\}^{m}\times{\Sigma_{\mathcal{O}}}^{m})^{*}$
as follows. For every letter $(i,b,o)$, we define
$h((i,b,o))=(i^{m},bin(b),o^{m})$. For a word
$\sigma\in(\Sigma_{\mathcal{I}}\times\Sigma_{B}\times\Sigma_{\mathcal{O}})^{*}$
and a letter
$x\in(\Sigma_{\mathcal{I}}\times\Sigma_{B}\times\Sigma_{\mathcal{O}})$ we
define $h(\sigma x)=h(\sigma)h(x)$. By definition, $h$ is an homomorphism,
note that $h$ is also an injection.

Now assume that there is a TDP/PDP solution to
$I^{\prime}=(\Sigma_{\mathcal{I}},\\{0,1\\},\Sigma_{\mathcal{O}},\mathcal{A}_{R^{\prime}})$,
and recall that $\mathcal{A}_{R^{\prime}}$ is obtained from $\mathcal{A}_{R}$
by replacing every letter $(i,o)$ with a word $(i^{m},o^{m})$. Let
$S^{\prime}$ be the regular expression obtained from Lemma 10 w.r.t.
$I^{\prime}$, and let $L(S^{\prime})$ be the regular language of $S^{\prime}$.
Since every word in $L(S^{\prime})$ is a concatenation of strings of the form
$(i^{m},t,o^{m})$ for some $i\in\Sigma_{\mathcal{I}}$, $t\in\\{0,1\\}^{m}$ and
$o\in\Sigma_{\mathcal{O}}$, we have that
$L(S^{\prime})\subseteq({\Sigma_{\mathcal{I}}}^{m}\times\\{0,1\\}^{m}\times{\Sigma_{\mathcal{O}}}^{m})^{*}$.
Moreover, since $bin$ is a bijection we have that for every such
$(i^{m},t,o^{m})$, $(i,bin^{-1}(t),o)$ is well defined and
$h(i,bin^{-1}(t),o)=(i^{m},t,o^{m})$, therefore the homomorphism $h$ is onto
$L(S^{\prime})$. Since the pre-image under homomorphisms of a regular language
is a regular language as well (see [26]), we have that there is a regular
language $L(S)$ of a regular expression $S$ over
$(\Sigma_{\mathcal{I}}\times\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}})^{*}$
such that $L(S)=h^{-1}(L(S^{\prime}))$.

Since $S^{\prime}$ satisfies conditions (1)-(3) of Lemma 10 w.r.t the instance
$I^{\prime}$ and since $h$ is a bijection from $L(S)$ to $L(S^{\prime})$, it
is easy to check that $S$ satisfies the conditions (1)-(3) of Lemma 10 w.r.t
the instance $I$, which means that $I$ has a TDP/PDP solution.

Theorem 11 is stated only for an alphabet $\Sigma_{\mathcal{B}}$ whose size is
some power of $2$. When this is not the case then the proof for Theorem 11
does not hold. The reason is that if $m$ is such that
$|\Sigma_{\mathcal{B}}|>2^{m}$, then some letters in $\Sigma_{B}$ may not be
represented via the translation function $bin$, thus the first part of the
proof does not hold. If on the other hand $m$ is such that
$|\Sigma_{\mathcal{B}}|<2^{m}$ then $bin^{-1}$ may “add” additional letters to
$|\Sigma_{\mathcal{B}}|$, thus the second part of the proof does not hold.
Since we do not yet know the solution for this general case, we make the
following conjecture.

######  Conjecture 12.

There is a reduction for TDP/PDP from an intermediate alphabet of arbitrary
size to the binary alphabet.

Corollary 18 shows that TDP/PDP on automatic relations with unary intermediate
alphabet is solvable.

###  5.4. Strategic automatic PDP

A specific version of PDP on automatic relations, that captures essential
concepts in synthesis [28, 16, 40], is when we require the solution to consist
of strategies. For that, we define Strategic automatic PDP, or Strategic PDP
in short, as PDP on automatic relations in which the required relations
$R_{1}$ and $R_{2}$ are functions (defined in Section 3) that can be
represented by finite-state transducers $T_{1}$ and $T_{2}$, respectively.

Strategic PDP can be viewed as a game of incomplete information. Since the
information “flows” in one direction, the key to proving decidability for this
problem is to view the problem as a one-way chain communication of distributed
synthesis from [28] to synthesize the required transducers. The construction
here is rather technical, and we assume familiarity with the techniques
developed in [28].

######  Theorem 13.

Strategic PDP is in EXPTIME.

######  Proof 5.7.

The proof for Theorem 13 relies heavily on definitions and terminology from
[28]. To ease the reading of the proof we bring the definitions from [28] in
Appendix B.

We first describe the intuition of the proof by providing a high-level
outline. Note that the required transducer $T_{1}$ is a finite-state
realization of a function
$f_{1}:\Sigma_{\mathcal{I}}^{+}\rightarrow\Sigma_{\mathcal{B}}$, and the
required transducer $T_{2}$ is a finite-state realization of a function
$f_{2}:\Sigma_{\mathcal{B}}^{+}\rightarrow\Sigma_{\mathcal{O}}$. We first
consider trees of the form
$\tau:\Sigma_{\mathcal{I}}^{*}\rightarrow\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}}$.
Such a tree represents simultaneously both $f_{1}$ and $f_{2}$. (The label of
the root is ignored here.) A branch of this tree can be viewed as a word
$w\in(\Sigma_{I}\times\Sigma_{B}\times\Sigma_{O})^{\omega}$. By running the
DFA $\mathcal{A}_{R}$ on $w$, ignoring $\Sigma_{B}$, we can check that every
prefix of $w$ is consistent with $R$. Thus, we can construct a deterministic
automaton $\mathcal{A}_{R}^{t}$ on infinite trees that checks that all
prefixes of all branches in $\tau$ are consistent with $R$.

Note, however, that in $\tau$ the $\Sigma_{\mathcal{O}}$ values depend not on
the $\Sigma_{\mathcal{B}}$ values but on the $\Sigma_{\mathcal{I}}$ values,
while in $f_{2}$ the domain is $\Sigma_{\mathcal{B}}^{+}$. So it is possible
that the $\Sigma_{\mathcal{O}}$ values do not depend functionally on the
$\Sigma_{\mathcal{B}}$ values. So next we consider a tree
$\tau_{2}:\Sigma_{\mathcal{B}}^{*}\rightarrow\Sigma_{\mathcal{O}}$. We can now
simulate $\mathcal{A}_{R}^{t}$ on $\tau_{2}$ (cf., [28]). The idea is to match
each branch of $\tau$ with a branch of $\tau_{2}$ according to the
$\mathcal{B}$-values. This means that we have several branches of the run of
$\mathcal{A}_{R}^{t}$ running on one branch of $\tau_{2}$. We thus obtain an
alternating tree automaton $\mathcal{A}_{2}$, whose size is polynomial in the
size of $\mathcal{A}_{R}$. We can now check in exponential time non-emptiness
of $\mathcal{A}_{2}$, to see if a function $f_{2}$ exists. If
$\mathcal{A}_{2}$ is non-empty, then we can obtain a witness transducer
$T_{2}$ whose size is exponential in $\mathcal{A}_{R}$.

Finally, we consider a tree
$\tau_{1}:\Sigma_{\mathcal{I}}^{*}\rightarrow\Sigma_{\mathcal{B}}$ that
represents $f_{1}$. We simulate both $\mathcal{A}_{R}$ and $T_{2}$ on each
branch of $\tau_{1}$, where $T_{2}$ generates the $\mathcal{O}$-values that
were present in $\tau$ but not in $\tau_{1}$. Using these values
$\mathcal{A}_{R}$ checks that each prefix is consistent with $R$. We have
obtained a deterministic tree automaton $\mathcal{A}_{1}$, whose size is
exponential in $\mathcal{A}_{R}$. We can now check non-emptiness of
$\mathcal{A}_{1}$ in time that is linear in the size of $\mathcal{A}_{1}$, and
obtain a witness transducer $T_{1}$. Thus, we can solve Strategic PDP for
automatic relations in exponential time.

We now describe the proof of Theorem 13 in detail. Recall that $R$ is the
given automatic relation for the Strategic PDP problem. Let the DFA for $R$ be
$\mathcal{A}_{R}=(\Sigma_{\mathcal{I}}\times\Sigma_{\mathcal{O}},Q,q_{0},\delta,F)$;
assume without loss of generality that $q_{0}\in F$. We use $\mathcal{A}_{R}$
to construct a deterministic Büchi tree automaton $\mathcal{A}_{R}^{t}$, over
infinite trees
$\tau:\Sigma_{\mathcal{I}}^{*}\rightarrow\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}}$,
that checks that all prefixes of all branches in an input tree $\tau$ are
consistent with $R$. More precise, Let $a_{1},\ldots,a_{m}$ be a nonempty
sequences of input symbols from $\Sigma_{I}$, and let
$\tau(a_{1},\ldots,a_{i})=(b_{i},c_{i})$. Then we want the word pair
$(a_{1}\cdots a_{i},c_{1}\cdots c_{i})$ to be in $R$.

We define this tree automaton as follows:
$\mathcal{A}_{R}^{t}=(\Sigma_{\mathcal{I}},\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}},Q^{\prime},q_{0},\delta^{t},\alpha)$
is a $(\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}})$-labeled
$\Sigma_{\mathcal{I}}$-tree deterministic automaton, with
$Q^{\prime}=\\{q_{0}\\}\cup(\Sigma_{\mathcal{I}}\times Q)$, and
$\alpha=Q^{\prime}$ as the acceptance condition. Intuitively, this tree
automaton $\mathcal{A}_{R}^{n}$ carries with it the last letter in
$\Sigma_{\mathcal{I}}$, to enable it to simulate $\mathcal{A}_{R}$. For the
transition function, we have as follows:

  * •

$\delta^{t}(q_{0})=\bigwedge_{i\in\Sigma_{\mathcal{I}}}\langle
i,(i,q_{0})\rangle$ (i.e., the successor state in direction $i$ is the state
$(i,q_{0})$). (Note that in $\delta^{t}(q_{0})$ there is no input letter,
which means that we are ignoring the label of the root.)

  * •

$\delta^{t}((i,q),(b,o))=\bigwedge_{i^{\prime}\in\Sigma_{\mathcal{I}}}\langle
i^{\prime},(i^{\prime},\delta(q,(i,o)))\rangle$, for $q\not=q_{0}$, if $q\in
F$, and $\delta^{t}((i,q),(b,o))=false$, if $q\not\in F$.

(The notation $\langle i^{\prime},(i^{\prime},\delta(q,(i,o)))\rangle$ means
that the state $(i^{\prime},\delta(q,(i,o)))$ is sent in direction
$i^{\prime}$.) Intuitively, $\mathcal{A}_{R}^{t}$ is a deterministic tree
automaton that checks that all prefixes of all branches of an input tree
$\tau$ are consistent with $R$, by simulating $\mathcal{A}_{R}$ along all
branches of $\tau$. While the syntax used here is that of alternating
automata, $\mathcal{A}_{R}^{t}$ send at most one successor state in each tree
direction, so it is a deterministic automaton. Note also that the size of
$A_{R}^{t}$ is quadratic in the size of $A_{R}$.

Next we convert $\mathcal{A}_{R}^{t}$ into a nondeterministic tree automaton
$\mathcal{A}^{n}_{R}$ that gets an unlabeled $\Sigma_{\mathcal{I}}$-tree as
input, guesses a $\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}}$ labeling,
and checks that an input tree with the guessed label is accepted by
$\mathcal{A}_{R}^{t}$. Formally,
$\mathcal{A}_{R}^{n}=(\Sigma_{\mathcal{I}},Q,q_{0},\delta^{n},\alpha)$ is a
nondeterministic automaton on unlabeled $\Sigma_{\mathcal{I}}$-trees, with
$\alpha=Q$ as the acceptance condition. The transition function is:

  1. (1)

$\delta^{n}(q_{0})=\bigwedge_{i\in\Sigma_{\mathcal{I}}}\bigvee_{b\in\Sigma_{\mathcal{B}}}\bigvee_{o\in\Sigma_{\mathcal{O}}}\langle
i,\delta(q_{0},(i,o))\rangle$

  2. (2)

$\delta^{n}(q)=\bigwedge_{i\in\Sigma_{\mathcal{I}}}\bigvee_{b\in\Sigma_{\mathcal{B}}}\bigvee_{o\in\Sigma_{\mathcal{O}}}\langle
i,\delta(q,(i,o)))\rangle$, for $q\not=q_{0}$ if $q\in F$

  3. (3)

$\delta^{n}(q)=false$ for $q\not=q_{0}$ if $q\not\in F$.

Note that an accepting run of $\mathcal{A}^{n}_{R}$ induces a
$(\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}})$-labeling of the
$\Sigma_{\mathcal{I}}$-tree, due to the nodeterministic guesses in the
transitions.

For a function
$h:\Sigma_{\mathcal{I}}\rightarrow\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}}$,
let $h(i)_{1},h(i)_{2}$ denote the first and second components of $h(i)$
respectively. Then note that we can rewrite the first two clauses of the
transition function as follows, where $\eta$ ranges over functions from
$\Sigma_{\mathcal{I}}$ to $\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}}$.

  1. (1)

$\delta^{n}(q_{0})=\bigvee_{\eta:\Sigma_{\mathcal{I}}\rightarrow(\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}})}\bigwedge_{i\in\Sigma_{\mathcal{I}}}\langle
i,\delta(q_{0},(i,\eta(i)_{2})\rangle$

  2. (2)

$\delta^{n}(q)=\bigvee_{\eta:\Sigma_{\mathcal{I}}\rightarrow(\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}})}\bigwedge_{i\in\Sigma_{\mathcal{I}}}\langle
i,\delta(q,(i,\eta(i)_{2})\rangle$, for $q\not=q_{0}$.

We next use $\mathcal{A}_{R}^{n}$ to construct the Strategic PDP solution
transducers $T_{1},T_{2}$ that describe trees $\tau_{1},\tau_{2}$
respectively. We first construct $T_{2}$ by obtaining an alternating tree
automaton $\mathcal{A}_{2}$. Every tree in $L(\mathcal{A}_{2})$ is a partial
solution for Strategic PDP.

We obtain $\mathcal{A}_{2}$ by simulating $A^{n}_{R}$ on
$\Sigma_{\mathcal{O}}$-labeled $\Sigma_{\mathcal{B}}$ trees, using an
alternating automaton
$\mathcal{A}_{2}=(\Sigma_{\mathcal{B}},\Sigma_{\mathcal{O}},Q^{\prime},q_{0},\delta_{2},\alpha_{2})$,
where $Q^{\prime}=\\{q_{0}\\}\cup(Q\times\Sigma_{\mathcal{O}}))$,
$\alpha_{2}=Q^{\prime\prime}$, and the transition function is defined as
follows:

  * •

$\delta^{2}(q_{0})=\
\bigvee_{\eta:\Sigma_{\mathcal{I}}\rightarrow(\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}})}\bigwedge_{b\in\Sigma_{\mathcal{B}}}\bigwedge_{i\in\Sigma_{\mathcal{I}}~{}\mbox{and}~{}b=\eta(i)_{1}}\langle
b,(\delta(q_{0},(i,\eta(i)_{2})),\eta(i)_{2})\rangle$

  * •

$\delta^{2}((q,o^{\prime}),o)=\bigvee_{\eta:\Sigma_{\mathcal{I}}\rightarrow(\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}})}\bigwedge_{b\in\Sigma_{\mathcal{B}}}\bigwedge_{i\in\Sigma_{\mathcal{I}}~{}\mbox{and}~{}b=\eta(i)_{1}}\langle
b,(\delta(q,(i,\eta(i)_{2})),\eta(i)_{2})\rangle$ if $q\in F$ and
$o=o^{\prime}$,

  * •

$\delta^{2}((q,o^{\prime}),o)=false$ if $q\not\in F$ or
$o^{\prime}\not=o^{\prime}$.

In this simulation, every
$(\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}})$-labeled branch of $\tau$
maps to a branch of $\tau_{2}$ with the same
$(\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}})$-labeling. Note, however,
that in $\tau$ the $\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}}$ letter
pairs are all node labels, while in $\tau_{2}$ the
$\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}}$ letter pairs come from tree
directions ($\Sigma_{\mathcal{B}}$) and node labels ($\Sigma_{\mathcal{O}}$).

As shown in [28], if $\tau_{2}$ is accepted by $A_{2}$, then an accepting run
of $A_{2}$ on $\tau_{2}$ yields a tree $\tau$ where the $\Sigma_{\mathcal{O}}$
labeling depends only on the $\Sigma_{\mathcal{B}}$ labeling. In particular,
if $\mathcal{A}_{2}$ is nonempty, it is witnessed by a finite-state transducer
$T_{2}$. We thus have to check that $\mathcal{A}_{2}$ is nonempty. For this we
use standard techniques in tree-automata theory [19], according to which
nonemptiness of $\mathcal{A}_{2}$ can be checked in exponential time. A subtle
point here is that the transition function of $\mathcal{A}_{2}$ is of
exponential size, due to the disjunction
$\bigvee_{\eta:\Sigma_{\mathcal{I}}\rightarrow(\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}})}$.
But in the nonemptiness algorithm this disjunction of exponential size turns
into an alphabet of exponential size, and this affects the computational
complexity multiplicatively, so the algorithm is still exponential with
respect to $\mathcal{A}_{R}$.

If the nonemptiness algorithm returns “nonempty”, it returns also as a witness
a finite-state transducer that generates a tree accepted by $\mathcal{A}_{2}$.
The transducer is
$T_{2}=(\Sigma_{\mathcal{B}},\Sigma_{\mathcal{O}},S,s_{0},\beta)$, where $S$
is a finite state set, $s_{0}\in S$ is the initial state, and
$\beta:S\times\Sigma_{I}\rightarrow S\times\Sigma\mathcal{O}$ is the
transition function that yields, for a state $s\in S$ and input letter
$b\in\Sigma_{\mathcal{B}}$, a pair $\beta(s,b)$ of a successor state and an
output letter. The state set $S$ is, in general, of size that is exponential
in $|Q|$.

We can now combine $A_{R}^{n}$ with $T_{2}$ to construct a nondeterministic
tree automaton $\mathcal{A}_{1}$ for $\tau_{1}$, which is now an unlabeled
$\Sigma_{\mathcal{I}}$-tree. Formally,
$\mathcal{A}_{1}=(\Sigma_{\mathcal{I}},Q\times
S,(q_{0},s_{0}),\delta_{1},\alpha_{1})$, where $\alpha_{1}=(Q\times S)$, and
the transition function $\delta_{2}$ is obtained by combining $\delta^{n}$
with $\beta$:

  1. (1)

$\delta_{2}((q_{0},s_{0}))=\bigvee_{\zeta:\Sigma_{\mathcal{I}}\rightarrow\Sigma_{\mathcal{B}}}\bigwedge_{i\in\Sigma_{\mathcal{I}}}\langle
i,(\delta(q_{0},(i,\beta(s_{0},\zeta(i))_{2}),\beta(s_{0},\zeta(i))_{1})\rangle$

  2. (2)

$\delta_{2}((q,s))=\bigvee_{\zeta:\Sigma_{\mathcal{I}}\rightarrow\Sigma_{\mathcal{B}}}\bigwedge_{i\in\Sigma_{\mathcal{I}}}\langle
i,(\delta(q,(i,\beta(s,\zeta(i))_{2}),\beta(s,\zeta(i))_{1})\rangle$

Nonemptiness of $\mathcal{A}_{1}$ can be checked in time that is linear in the
size of $\mathcal{A}_{1}$ [19], so it is exponential in the size of
$\mathcal{A}_{R}$. Again, the nonemptiness algorithm returns a finite-state
transducer $T_{1}$ that induces a strategy mapping $\Sigma_{\mathcal{I}}^{+}$
to $\Sigma_{\mathcal{B}}$.

This concludes the proof that Strategic PDP can be solved in EXPTIME.

##  6\. Decomposition with a hint

Our results so far indicate that fully automated decomposition is a hard
problem. Can we ameliorate this difficulty by including a “human in the loop”?
Indeed, in some decomposition scenarios, a part of a decomposition is already
given, and the challenge is to find the complementary component. This can be
thought of as a partial solution that is offered by a human intuition, e.g. a
domain expert. In the context of our framework we have that a candidate to
either $R_{1}$ or $R_{2}$ is given (in the relevant description formalism) as
a “hint”. The question then is whether, given one possible component, a
complementary component indeed exists, and can be constructed, such that both
relations together meet the TD/PD conditions.

We discuss first TDP/PDP problems with a hint $R_{1}$ followed by a discussion
with similar arguments for TDP/PDP problems with hint $R_{2}$.

###  6.1. TDP/PDP with hint $R_{1}$

TDP/PDP problem with a hint $R_{1}$ is formally defined as follows.

In the TDP/PDP problem with a hint $R_{1}$ we are given input, output and
intermediate domain $\mathcal{I},\mathcal{O},\mathcal{B}$, relations
$R\subseteq\mathcal{I}\times\mathcal{O}$ and
$R_{1}\subseteq\mathcal{I}\times\mathcal{B}$. The goal is to find whether
there is a relation $R_{2}\subseteq\mathcal{B}\times\mathcal{O}$ such that
$(R_{1},R_{2})$ meet the TD/PD conditions.

The exact nature of the domains and relations varies as before according to
the problem setting (explicit, etc.). As we see, such a hint as a partial
solution relaxes the computational difficulty of TDP/PDP, shown in previous
sections, considerably. To that end, we show the following maximum property
that is relevant for all TDP/PDP settings. Given a TDP/PDP instance with a
hint $R_{1}$, define the relation
$R^{\prime}_{2}\subseteq(\mathcal{B}\times\mathcal{O})$ to be
$R^{\prime}_{2}=\\{(b,o)\mid\forall i\in\mathcal{I}((i,b)\in
R_{1}\rightarrow(i,o)\in R)\\}$. Note that $Dom(R^{\prime}_{2})$ can strictly
contain $Img(R_{1})$.

######  Lemma 14.

Every solution for TDP/PDP with a hint $R_{1}$ is contained in
$R^{\prime}_{2}$ and if there exists such a solution then $R^{\prime}_{2}$ is
a solution as well.

######  Proof 6.1.

We prove for TDP, we skip the proof for PDP that is almost identical. Let
$R_{2}$ be a solution to TDP with a hint $R_{1}$. We first see that
$R_{2}\subseteq R^{\prime}_{2}$. Let $(b,o)\in R_{2}$. Suppose there exists
$i$ such that $(i,b)\in R_{1}$ and $(i,o)\not\in R$. Then we have that
$R_{1}\circ R_{2}\not\subseteq R$ which means that $R_{2}$ is not a solution,
a contradiction. Therefore we have that for all $i$, if $(i,b)\in R_{1}$ then
$(i,o)\in R$, hence $(b,o)\in R^{\prime}_{2}$. To see that $R^{\prime}_{2}$ is
a solution, first see that since $R_{2}$ is a solution contained in
$R^{\prime}_{2}$ then $Dom(R_{1}\circ R^{\prime}_{2})=Dom(R)$ and
$Img(R_{1})\subseteq Dom(R^{\prime}_{2})$. Let $(i,o)\in R_{1}\circ
R^{\prime}_{2}$. Then there is a $b$ such that $(i,b)\in R_{1}$ and $(b,o)\in
R^{\prime}_{2}$, which means that by the definition of $R^{\prime}_{2}$ and
since $(i,b)\in R_{1}$, it must be that $(i,o)\in R$. Finally, assume that
$(i,o)\in R$. Then there is $b$ such that $(i,b)\in R_{1}$, and $(b,o)\in
R^{\prime\prime}_{2}$ for some solution $R^{\prime\prime}_{2}$ contained in
$R^{\prime}_{2}$. Therefore $(b,o)\in R^{\prime}_{2}$ so $(i,o)\in R_{1}\circ
R^{\prime}_{2}$.

From Lemma 14 we get a simple method to solve TDP/PDP with a hint $R_{1}$ for
the explicit settings as follows: Construct $R^{\prime}_{2}$ and check that
$(R_{1},R^{\prime}_{2})$ meet the TD/PD conditions. If $R^{\prime}_{2}$ meets
these conditions then $(R_{1},R^{\prime}_{2})$ is a solution for TD/PD.
Otherwise, there is no solution with $R_{1}$ as a hint. From this observation
we get:

######  Theorem 15.

TDP/PDP with a hint $R_{1}$ for explicit relations are in PTIME.

The definition of $R^{\prime}_{2}$ can also solve the symbolic setting with a
hint. Thus the following result allows the use of QBF solvers for finding a
solution for $R_{1}$.

######  Theorem 16.

TDP/PDP with a hint $C_{R_{1}}$ for symbolic relations are in $\Pi^{P}_{3}$.

######  Proof 6.2.

For the symbolic setting, when $R$ and $R_{1}$ are given as circuits $C_{R}$
and $C_{R_{1}}$, resp., we can use the definitions of $C_{R^{\prime}_{2}}$ to
verify the TD/PD conditions: for $TDP$ verify the following formulas (1)
$\forall\vec{b},\vec{i}\exists\vec{o}(C_{R_{1}}(\vec{i},\vec{b})\rightarrow
C_{R^{\prime}_{2}}(\vec{b},\vec{o}))$, and (2)
$\forall\vec{i},\vec{o}(\exists\vec{b}(C_{R_{1}}(\vec{i},\vec{b})\wedge
C_{R^{\prime}_{2}}(\vec{b},\vec{o})))\leftrightarrow C_{R}(\vec{i},\vec{o})$.
For PDP in addition to Formula (1) we also need to verify
(3) $\forall\vec{i}(\exists\vec{b},\vec{o}(C_{R_{1}}(\vec{i},\vec{b})\wedge
C_{R^{\prime}_{2}}(\vec{b},\vec{o})))\leftrightarrow\exists\vec{o}^{\prime}C_{R}(\vec{i},\vec{o}^{\prime})$
, and (4)
$\forall\vec{i},\vec{o}(\exists\vec{b}(C_{R_{1}}(\vec{i},\vec{b})\wedge
C_{R^{\prime}_{2}}(\vec{b},\vec{o}))\rightarrow C_{R}(\vec{i},\vec{o}))$. In
all these, $C_{R^{\prime}_{2}}$ need not be constructed but can be described
by the formula $(\forall\vec{i})(C_{R_{1}}(\vec{i},\vec{b})\rightarrow
C_{R}(\vec{i},\vec{o}))$.111 By performing quantifier elimination on this
formula, $C_{R^{\prime}_{2}}$ can be constructed explicitly, in time that may
be exponential. c.f., [16]..

For the automatic relation setting we have the following result for TDP/PDP
with a hint $R_{1}$, where we assume that $R_{1}$ is given as a DFA.

######  Theorem 17.

TDP/PDP with a hint $\mathcal{A}_{R_{1}}$ for automatic relations are in
EXPSPACE.

######  Proof 6.3.

We start by recalling some basic automata constructions. Let $A,B,C$ be
(possibly infinite) domains. If $\mathcal{A}$ is an automaton that describes a
relation $R\subseteq A\times B$ (in a the sense of Section 5.3) then an NFA
$Img(\mathcal{A})$ that describes $Img(R)$ is obtained by discarding the
$B$-alphabet labels from $\mathcal{A}$. Similarly an NFA $Dom(\mathcal{A})$
that describes $Dom(R)$ is obtained by discarding the $A$-alphabet labels from
$\mathcal{A}$. From automaton $\mathcal{A}_{1}$ that describes a relation
$R_{1}\subseteq A\times B$, and an automaton $\mathcal{A}_{2}$ that describes
a relation $R_{2}\subseteq B\times C$, we obtain an automaton denoted by
$\mathcal{A}_{1}\circ\mathcal{A}_{2}$ that describes $R_{1}\circ R_{2}$ by
taking the product automaton of $A_{1}$ and $A_{2}$, eliminate the labels
$(a,b,b^{\prime},c)$ in which $b\not=b^{\prime}$, then discarding the
$B$-alphabet labels from the remaining labels. Finally, to check if a DFA
$\mathcal{A}$ is contained in a DFA $\mathcal{A}^{\prime}$ we check for
emptiness the automaton $\mathcal{A}\cap\neg\mathcal{A}^{\prime}$.

Now for the proof, assume that
$\mathcal{A}_{R}=(\Sigma_{\mathcal{I}}\times\Sigma_{\mathcal{O}},Q,q^{0},\delta,F)$
is a DFA that describes $R$ and
$\mathcal{A}_{R_{1}}=(\Sigma_{\mathcal{I}}\times\Sigma_{\mathcal{B}},Q_{1},q^{0}_{1},\delta_{1},F_{1})$
is a DFA hint. We show how to construct a DFA
$\mathcal{A}_{2}=(\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}},Q_{2},q^{0}_{2},\delta_{2},F_{2})$
that describes the maximum relation $R^{\prime}_{2}$. We define
$\mathcal{A}^{\prime}=(\Sigma_{\mathcal{I}}\times\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{I}}\times\Sigma_{\mathcal{O}},Q_{1}\times
Q,(q_{1}^{0},q^{0}),\delta_{1}\times\delta,F^{\prime})$ as the product
automaton of $\mathcal{A}_{R_{1}}$ and $\mathcal{A}_{R}$. We re-define the
accepting states $F^{\prime}=F\times F_{1}$ by setting
$F^{\prime}=\\{(q,q^{\prime})\mid q\in F_{1}\rightarrow q^{\prime}\in F\\}$.
For the transition function, we first discard from $\mathcal{A}^{\prime}$ all
the $(i,b,i^{\prime},o)$ edges in which $(i\not=i^{\prime})$. Next we delete
the alphabets $\Sigma_{\mathcal{I}}\times\Sigma_{\mathcal{I}}$ from all the
labels in $\mathcal{A}^{\prime}$. This results in a non-deterministic
automaton, that we determinize (with possibly an exponential blow-up) in the
standard way through the subset construction, with the one exception that we
set every super-state (in the subset construction) to be accepting if and only
if all of its elements are accepting states. This results in a DFA
$\mathcal{A}_{2}$ over $\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}}$ that
describes the maximum relation $R^{\prime}_{2}$.

Note that the construction of $\mathcal{A}_{2}$ can take exponential time (in
the size of $\mathcal{A}_{R_{1}}$ and $\mathcal{A}_{R}$ because of the
determinization process.

$\mathcal{A}_{2}$ describes the maximum relation $R^{\prime}_{2}$.

######  Proof 6.4.

Let $(\vec{b},\vec{o})\in L(\mathcal{A}_{2})$. Then for every
$\vec{i}\in\Sigma_{\mathcal{I}}$ such that $(\vec{i},\vec{b})$ is in
$L(\mathcal{A}_{R_{1}})$ we see that $(\vec{i},\vec{o})$ is in
$L(\mathcal{A}_{R})$, which means $(\vec{b},\vec{o})\in R^{\prime}_{2}$.
Suppose otherwise, then we have that $(\vec{i},\vec{b})$ reaches an accepting
state in $\mathcal{A}_{R_{1}}$ and a non-accepting state in $\mathcal{A}_{R}$.
Therefore by our construction the word
$(\vec{i},\vec{b},\vec{i^{\prime}},\vec{o})$ is not accepting in
$\mathcal{A}^{\prime}$ before removing the $\Sigma_{\mathcal{I}}$ letters,
therefore $(\vec{b},\vec{o})$ is not in $\mathcal{A}^{\prime}$, a
contradiction. Next, assume $(\vec{b},\vec{o})\in R^{\prime}_{2}$. Then for
every $\vec{i}$ such that $(\vec{i},\vec{b})\in R_{1}$, we have that
$(\vec{i},\vec{o})\in R$. So if $(\vec{i},\vec{b})\in L(\mathcal{A}_{R_{1}})$
then $(\vec{i},\vec{o})\in L(\mathcal{A}_{R})$. Therefore for every
$\vec{i}\in\Sigma^{*}_{\mathcal{I}}$, we have that
$(\vec{i},\vec{b},\vec{i},\vec{o})$ is accepting in the construction process
of $\mathcal{A}_{2}$ before removing the $\Sigma_{\mathcal{I}}$ letters and
determinizing. So $(\vec{b},\vec{o})\in L(\mathcal{A}_{2})$.

Finally we need to check that $(\mathcal{A}_{R_{1}},\mathcal{A}_{2})$ meet the
TD/PD conditions. We do this step by step: For TDP we need to check:

  1. (1)

$L(Img(\mathcal{A}_{R_{1}}))\subseteq L(Dom(\mathcal{A}_{2}))$ which means
that $Img(\mathcal{A}_{R_{1}})\cap\neg Dom(\mathcal{A}_{2})=\emptyset$. Note
that both $Img(\mathcal{A}_{R_{1}})$ and $Dom(\mathcal{A}_{2})$ are non-
deterministic, but while checking the condition does not require
determinization of $Img(\mathcal{A}_{R_{1}})$, to construct $\neg
Dom(\mathcal{A}_{2})$ we need to determinize $Dom(\mathcal{A}_{2})$ with an
extra exponential time, in the size of $\mathcal{A}_{2}$. We can however avoid
direct construction by constructing the automata “on-the-fly” one state at a
time. This leads to an overall construction in EXPSPACE.

  2. (2)

$L(\mathcal{A}_{R_{1}}\circ\mathcal{A}_{2})=L(\mathcal{A})$. Here we need to
check that
$(\mathcal{A}_{R_{1}}\circ\mathcal{A}_{2})\cap\neg\mathcal{A}=\emptyset$,
which can be done in polynomial time since $\mathcal{A}$ is deterministic; and
that $\neg(\mathcal{A}_{R_{1}}\circ\mathcal{A}_{2})\cap\mathcal{A}=\emptyset$
that as before, requires determinization of
$\mathcal{A}_{R_{1}}\circ\mathcal{A}_{2}$, which already has exponential size,
all in all a double exponential blow up. Again a indirect construction can be
done as before in EXPSPACE.

For PDP check that:

  1. (1)

$L(Dom(\mathcal{A}_{R_{1}}))\subseteq L(Img(\mathcal{A}_{2}))$ which as before
can be done in EXPSPACE.

  2. (2)

$L(Dom(\mathcal{A}_{R_{1}}\circ\mathcal{A}_{2}))=L(Dom(\mathcal{A}))$ which
can also take exponential time, since as before checking $\neg
Dom(\mathcal{A}_{R_{1}}\circ\mathcal{A}_{2})\cap Dom(\mathcal{A})=\emptyset$
requires determinization of $\mathcal{A}_{R_{1}}\circ\mathcal{A}_{2}$ which is
already in exponential size. As before, this can be done in EXPSPACE.

  3. (3)

$L(\mathcal{A}_{R_{1}}\circ\mathcal{A}_{2})\subseteq L(\mathcal{A})$ which can
be done in polynomial time. Since
$(\mathcal{A}_{R_{1}}\circ\mathcal{A}_{2})\cap\neg\mathcal{A}=\emptyset$ since
$\mathcal{A}$ is deterministic.

Along the lines of the proof of Theorem 17, we can say the following on unary
intermediate alphabet.

######  Theorem 18.

TDP/PDP for automatic relations with a unary intermediate alphabet is in
PTIME.

######  Proof 6.5.

For a unary intermediate alphabet $\Sigma_{\mathcal{B}}=\\{b\\}$, every word
of length $n$ in $Dom(R)$ and in $Img(R)$ must be paired with the word
$b^{n}$. Therefore if $(\vec{i},\vec{o})\in L(\mathcal{A}_{R})$ for every
$\vec{i}\in L(Dom(\mathcal{A}_{R}))$ and $\vec{o}\in L(Img(\mathcal{A}_{R}))$
then there is a TDP (and therefore PDP) solution constructed as follows:
construct $\mathcal{A}_{R_{1}}$ from $\mathcal{A}_{R}$ by simply replacing
every $\Sigma_{\mathcal{O}}$ letter with the letter $b$ of
$\Sigma_{\mathcal{B}}$, and similarly construct $\mathcal{A}_{R_{2}}$ from
$\mathcal{A}_{R}$ by simply replacing every $\Sigma_{\mathcal{I}}$ letter with
the letter $b$ of $\Sigma_{\mathcal{B}}$. On the other hand if assume that
there exists $\vec{i}\in L(Dom(\mathcal{A}_{R}))$ and $\vec{o}\in
L(Img(\mathcal{A}_{R}))$ (suppose of size $n$) for which
$(\vec{i},\vec{o})\not\in L(\mathcal{A}_{R})$. Then we have that no solution
exists since then it means that
$(\vec{i^{\prime}},\vec{o}),(\vec{i},\vec{o^{\prime}})\in
L(\mathcal{A}_{R})\in L(\mathcal{A}_{R})$ for some $\vec{i^{\prime}},\vec{o}$,
but that means that $(\vec{i},b^{n})$, $(b^{n},\vec{o})$ must be accepting in
any solution for $R_{1},R_{2}$ respectively, then $(\vec{i},\vec{o})$ must be
in $L(\mathcal{A}_{R})$.

Therefore the approach that we take, is to construct an NFA that is non-empty
if and only if there indeed exists $\vec{i}\in L(Dom(\mathcal{A}_{R}))$ and
$\vec{o}\in L(Img(\mathcal{A}_{R}))$ for which $(\vec{i},\vec{o})\not\in
L(\mathcal{A}_{R})$, which means if and only if there is no TDP (or PDP)
solution. For that, we construct an NFA $\mathcal{A}$ that is the product of
$Dom(\mathcal{A}_{R})$, $Img(\mathcal{A}_{R})$ and $\mathcal{A}_{R}$. We then
first delete every label $(i,o,i^{\prime},o^{\prime})$ for which
$i\not=i^{\prime}$ or $o\not=o^{\prime}$. Then we set the accepting states of
$\mathcal{A}$ such that every state $(q,q^{\prime},q^{\prime\prime})$ is
accepting if and only if $q$ is an accepting state of $Dom(\mathcal{A}_{R})$,
$q^{\prime}$ is an accepting state of $Img(\mathcal{A}_{R})$, and
$q^{\prime\prime}$ is a non accepting state of $\mathcal{A}_{R}$.

To see that $\mathcal{A}$ is empty if and only if there is a TDP (or PDP)
solution, assume first that $\mathcal{A}$ is non-empty. Therefore there is an
accepting word $(\vec{i},\vec{o})$ which means that $\vec{i}\in
L(Dom(\mathcal{A}_{R}))$ and $\vec{o}\in L(Img(\mathcal{A}_{R}))$ but
$(\vec{i},\vec{o})\not\in L(\mathcal{A}_{R})$, therefore no TDP (or PDP)
solution exists. On the other hand if $\mathcal{A}$ is empty then it means
that for every $(\vec{i},\vec{o})$ for which $\vec{i}\in
L(Dom(\mathcal{A}_{R}))$ and $\vec{o}\in L(Img(\mathcal{A}_{R}))$, we have
that $(\vec{i},\vec{o})\in L(\mathcal{A}_{R})$ as well. Thus there is a TDP
solution.

Finally note that the construction of $\mathcal{A}$ is polynomial since no
determinization is required. Thus since checking emptiness for NFA can also be
done in polynomial time, we have that the problem is in PTIME.

Finally, for Strategic PDP in the automatic setting, we assume that the hint
is given in the form of a transducer.

######  Theorem 19.

Strategic PDP with a hint $T_{1}$ is in EXPTIME.

######  Proof 6.6.

For Strategic PDP with a hint $T_{1}$ as a transducer we simplify the
construction of Section 5.4. There we constructed $A_{2}$ by taking simulating
$A^{n}_{R}$ on $\tau_{2}$, and then checked non-emptiness for $A_{2}$ and
obtained a witness transducer $T_{2}$. Then we plugged $T_{2}$ into
$A^{n}_{R}$ and solved for $T_{1}$. Here we do not need to solve for $T_{1}$,
because it is given as a hint. In addition, also recall that $A^{n}_{R}$
guesses mappings
$\eta:\Sigma_{\mathcal{I}}\rightarrow\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}}$.
By taking the product of $A^{n}_{R}$ with $T_{1}$ we can ensure that these
guesses are consistent with $T_{1}$.

Formally, let
$T_{1}=(\Sigma_{\mathcal{I}},\Sigma_{\mathcal{B}},P,p_{0},\gamma)$, where $P$
is a finite state set, $p_{0}\in P$ is the initial state, and
$\gamma:P\times\Sigma_{I}\rightarrow P\times\Sigma_{\mathcal{B}}$ is the
transition function that yields, for a state $p\in P$ and input letter
$i\in\Sigma_{\mathcal{I}}$, a pair $\gamma(p,i)$ of a successor state and an
output letter.

Now we modify the construction of $\mathcal{A}_{2}$ from Section 5.4 and
define
$\mathcal{A}^{\prime}_{2}=(\Sigma_{\mathcal{B}},\Sigma_{\mathcal{O}},Q^{\prime\prime},(q_{0},p_{0}),\delta^{\prime}_{2},\alpha^{\prime}_{2})$,
where $Q^{\prime\prime}=\\{q_{0}\\}\cup(Q\times\Sigma_{\mathcal{O}})$,
$\alpha^{\prime}_{2}=Q^{\prime\prime}$, and the transition function is defined
as follows:

  * •

$\delta^{2}(q_{0},p_{0})=\
\bigvee_{\eta:\Sigma_{\mathcal{I}}\rightarrow\Sigma_{\mathcal{O}},}\bigwedge_{b\in\Sigma_{\mathcal{B}}}\bigwedge_{i\in\Sigma_{\mathcal{I}}~{}\mbox{and}~{}b=\gamma(p_{0},i)_{2}}\langle
b,(\delta(q_{0},(i,\eta(i))),\gamma(p_{0},i)_{1},\eta(i))\rangle$

  * •

$\delta^{2}((q,p,o^{\prime}),o)=\bigvee_{\eta:\Sigma_{\mathcal{I}}\rightarrow\Sigma_{\mathcal{O}}}\bigwedge_{b\in\Sigma_{\mathcal{B}}}\bigwedge_{i\in\Sigma_{\mathcal{I}}~{}\mbox{and}~{}b=\gamma(p,i)_{2}}\langle
b,(\delta(q,(i,\eta(i))),\gamma(p,i)_{1},\eta(i))\rangle$ if $q\in F$ and
$o=o^{\prime}$,

  * •

$\delta^{2}((q,p.o^{\prime}),o)=false$ if $q\not\in F$ or
$o^{\prime}\not=o^{\prime}$.

Now we continue as in 5.4; we check nonemptiness of $A^{\prime}_{2}$, and if
$\mathcal{A}^{\prime}_{2}$ is nonempty, we get a transducer $T_{2}$ that
defines a strategy from $\Sigma_{\mathcal{B}}^{+}$ to $\Sigma_{\mathcal{O}}$.
The complexity is exponential in the size of $\mathcal{A}_{R}$.

Finally, we consider the case of strategic PDP with hint $T_{2}$.

######  Theorem 20.

Strategic PDP with a hint $T_{2}$ is in PTIME.

######  Proof 6.7.

For Strategic PDP with a hint $T_{2}$ as a transducer we again simplify the
construction of Section 5.4. Now there is no need to construct the automaton
$\mathcal{A}_{2}$. Instead, we are given a a finite-state transducer $T_{2}$,
and we incorporate it in the construct of $A^{t}_{R}$.

Formally, let
$T_{2}=(\Sigma_{\mathcal{B}},\Sigma_{\mathcal{O}},P,p_{0},\gamma)$, where $P$
is a finite state set, $p_{0}\in P$ is the initial state, and
$\gamma:P\times\Sigma_{B}arr\rightarrow P\times\Sigma_{\mathcal{O}}$ is the
transition function that yields, for a state $p\in P$ and input letter
$i\in\Sigma_{\mathcal{B}}$, a pair $\gamma(p,i)$ of a successor state and an
output letter.

We now plug in $T_{2}$ into the automaton $A^{t}_{R}$. Formally,
${\mathcal{A}^{\prime}}_{R}^{t}=(\Sigma_{\mathcal{I}},\Sigma_{\mathcal{B}}\,Q^{\prime\prime},(q_{0},p+0),\delta^{t},\alpha)$
is a $\Sigma_{\mathcal{B}}$-labeled $\Sigma_{\mathcal{I}}$-tree deterministic
automaton, with $Q^{\prime}=\\{(q_{0},p_{0})\\}\cup(\Sigma_{\mathcal{I}}\times
Q\times Q)$, and $\alpha=Q^{\prime\prime}$ as the acceptance condition.

For the transition function, we have as follows:

  * •

$\delta^{t}(q_{0})=\bigwedge_{i\in\Sigma_{\mathcal{I}}}\langle
i,(i,q_{0},p_{0})\rangle$

  * •

$\delta^{t}((i,q,p),(b))=\bigwedge_{i^{\prime}\in\Sigma_{\mathcal{I}}}\langle
i^{\prime},(i^{\prime},\delta(q,(i,o),p^{\prime}))\rangle$, where
$o=\gamma(p,b)_{1}$ and $p^{\prime}=\gamma(p,b)_{2}$, for $q\not=q_{0}$ and
$q\in F$.

  * •

$\delta^{t}((i,q,p),(b))=false$, for $q\not=q_{0}$ and $q\not\in F$.

Note that ${\mathcal{A}^{\prime}}_{R}^{t}$ is of size that is polynomial in
$\mathcal{A}_{R}$ and $T_{2}$. Since non emptiness of deterministic tree
automata can be checked in polynomial time [19], the claim follows.

###  6.2. TDP/PDP with hint $R_{2}$

We now discuss the case for TDP/PDP when $R_{2}$ is given as a hint. The
definition, given below, is similar to that of $R_{1}$ being a hint.

TDP/PDP problem with a hint $R_{2}$ we are given input, output and
intermediate domain $\mathcal{I},\mathcal{O},\mathcal{B}$, relations
$R\subseteq\mathcal{I}\times\mathcal{O}$ and
$R_{2}\subseteq\mathcal{B}\times\mathcal{O}$. The goal is to find whether
there is a relation $R_{1}\subseteq\mathcal{I}\times\mathcal{B}$ such that
$(R_{1},R_{2})$ meet the TD/PD conditions.

As before, we define the maximum relation $R^{\prime}_{1}$ to be
$R^{\prime}_{1}=\\{(i,b)\mid(\exists o(b,o)\in R_{2})\wedge(\forall o((b,o)\in
R_{2}\rightarrow(i,o)\in R))\\}$. By an almost identical argument to that of
Lemma 14 we get the following.

######  Lemma 21.

Every solution for TDP/PDP with a hint $R_{2}$ is contained in
$R^{\prime}_{1}$ and if there exists such a solution then $R^{\prime}_{1}$ is
a solution as well.

For the explicit setting, construction again is easy. Therefore we have:

######  Theorem 22.

TDP/PDP with a hint $R_{2}$ for explicit relations is in PTIME.

And we also have

######  Theorem 23.

TDP/PDP with a hint $C_{R_{2}}$ for symbolic relations is in $\Pi^{P}_{3}$.

######  Proof 6.8.

The arguments for the proof are almost identical to those of Theorem 16, with
the one change that this time we are given $C_{R_{2}}$ and we need to verify
for TDP the formulas (1)
$\forall\vec{b},\vec{i}\exists\vec{o}(C_{R^{\prime}_{1}}(\vec{i},\vec{b})\rightarrow
C_{R_{2}}(\vec{b},\vec{o}))$ and (2)
$\forall\vec{i},\vec{o}\exists\vec{b}((C_{R^{\prime}_{1}}(\vec{i},\vec{b})\wedge
C_{R_{2}}(\vec{b},\vec{o}))\leftrightarrow C_{R}(\vec{i},\vec{o}))$. For PDP
in addition to Formula (1) we also need to verify (3)
$\forall\vec{i}(\exists\vec{b},\vec{o}(C_{R^{\prime}_{1}}(\vec{i},\vec{b})\wedge
C_{R_{2}}(\vec{b},\vec{o})))\leftrightarrow\exists\vec{o}^{\prime}C_{R}(\vec{i},\vec{o}^{\prime})$,
and (4)
$\forall\vec{i},\vec{o}(\exists\vec{b}(C_{R^{\prime}_{1}}(\vec{i},\vec{b})\wedge
C_{R_{2}}(\vec{b},\vec{o}))\rightarrow C_{R}(\vec{i},\vec{o}))$. In all these
$C_{R^{\prime}_{1}}\equiv(\exists\vec{o}C_{R_{2}}(\vec{b},\vec{o})\wedge\forall\vec{o}C_{R_{2}}(\vec{b},\vec{o})\rightarrow
C_{R}(\vec{i},\vec{o}))$.

Next, we can get a similar result to Theorem 17 for TDP/PDP for automatic
relations with a hint $R_{2}$, but we need to be more careful since $R_{1}$
imposes an extra condition of $Img(R_{1})\subseteq Dom(R_{2})$ that is needed
to be considered.

######  Theorem 24.

TDP/PDP for automatic relations with a hint $\mathcal{A}_{R_{2}}$ is in
EXPSPACE.

######  Proof 6.9.

Assume that
$\mathcal{A}=(\Sigma_{\mathcal{I}}\times\Sigma_{\mathcal{O}},Q,q^{0},\delta,F)$
is a DFA for $R$, and that
$\mathcal{A}_{R_{2}}=(\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}},Q_{2},q^{0}_{2},\delta_{2},F_{2})$
is a DFA for $R_{2}$ given as a hint. We show how to construct an automaton
$\mathcal{A}_{1}=(\Sigma_{\mathcal{I}}\times\Sigma_{\mathcal{B}},Q_{1},q^{0}_{1},\delta_{1},F_{1})$,
such that $L(\mathcal{A}_{1})=L(R^{\prime}_{1})$ where $R^{\prime}_{1}$ is the
maximum relation from Lemma 21.

We first construct an automaton that satisfies the second condition from the
definition of $R^{\prime}_{1}$, i.e. for every
$\vec{o}\in\Sigma_{\mathcal{O}}^{*}$, if $(\vec{b},\vec{o})\in R_{2}$ then
$(\vec{i},\vec{o})\in R$. Similar to the proof of Theorem 17, we define
$\mathcal{A}^{\prime}=(\Sigma_{\mathcal{I}}\times\Sigma_{\mathcal{O}}\times\Sigma_{\mathcal{B}}\times\Sigma_{\mathcal{O}},Q\times
Q_{2},(q^{0},q^{0}_{2}),\delta\times\delta_{2},F^{\prime})$ to be the product
automaton of $\mathcal{A}$ and $\mathcal{A}_{R_{2}}$. We redefine the
accepting states to be $F^{\prime}=\\{(q,q^{\prime})\mid q^{\prime}\in
F_{2}\rightarrow q\in F\\}$. To redefine the transition function, we first
discard from $\mathcal{A}^{\prime}$ all the edges $(i,o^{\prime},b,o)$ edges
in which $(o\not=o^{\prime})$. Next we delete the alphabets
$\Sigma_{\mathcal{O}}\times\Sigma_{\mathcal{O}}$ from all the labels in
$\mathcal{A}^{\prime}$. This results in a non-deterministic automaton, that we
determinize in the usual way through the subset construction, with the one
exception that we set every super-state (in the subset construction) to be
accepting if and only if all of its’ elements are accepting states. This
results in an automaton $\mathcal{A}^{\prime}_{1}$ over
$\Sigma_{\mathcal{I}}\times\Sigma_{\mathcal{B}}$.

Next, we have to take care of the required condition that if
$(\vec{i},\vec{b})$ is an accepting word in $\mathcal{A}^{\prime}_{1}$ then
$\vec{b}\in Dom(R_{2})$. For that we first construct
$\mathcal{A}^{\prime}_{2}=Dom(\mathcal{A}_{R_{2}})$ and determinize for an
exponential blowup. Then, we define $\mathcal{A}_{1}$ by taking the product
automaton of the DFAs $\mathcal{A}^{\prime}_{1}$ and
$\mathcal{A}^{\prime}_{2}$, and discarding all edges labeled
$(i,b,b^{\prime})$ in which $b\not=b^{\prime}$. Thus the overall construction
has an expontential blowup.

$\mathcal{A}_{1}$ defines the maximum relation $R^{\prime}_{1}$.

######  Proof 6.10.

Let $(\vec{i},\vec{b})$ be an accepting word in $\mathcal{A}_{1}$. Then
$(\vec{i},\vec{b},\vec{b})$ is an accepting word in
$\mathcal{A}^{\prime}_{1}\times\mathcal{A}^{\prime}_{2}$. Specifically
$\vec{b}$ is an accepting word in $\mathcal{A}^{\prime}_{2}$, therefore there
is a word $\vec{o}\in\Sigma_{\mathcal{O}}$ such that $(\vec{b},\vec{o})$ is
accepting in $\mathcal{A}_{R_{2}}$ so $\vec{b}\in Dom(R_{2})$. In addition
since $(\vec{i},\vec{b})$ is an accepting word in $\mathcal{A}^{\prime}_{1}$
then for every $\vec{o}\in\Sigma_{\mathcal{O}}$ such that $(\vec{b},\vec{o})$
is in $L(\mathcal{A}_{R_{2}})$ we have that $(\vec{i},\vec{o})$ is in
$L(\mathcal{A})$. Otherwise we have that $(\vec{b},\vec{o})$ reaches an
accepting state in $\mathcal{A}_{R_{2}}$, and a non-accepting state in
$\mathcal{A}$. Therefore by our construction the word
$(\vec{i},\vec{o},\vec{b},\vec{o})$ is not accepting in $\mathcal{A}^{\prime}$
before removing the $\Sigma_{\mathcal{O}}$ letters, therefore
$(\vec{i},\vec{b})$ is not in $\mathcal{A}^{\prime}$, a contradiction.

For the other side, assume $(\vec{i},\vec{b})\in R^{\prime}_{1}$. Then
$\vec{b}\in Dom(R_{2})$, therefore $\vec{b}\in L(\mathcal{A}^{\prime}_{2})$.
In addition, for every $\vec{o}$ such that $(\vec{b},\vec{o})\in R_{2}$, we
have that $(\vec{i},\vec{o})\in R$. So if $(\vec{b},\vec{o})\in
L(\mathcal{A}_{R_{2}})$ then $(\vec{i},\vec{o})\in L(\mathcal{A})$. Therefore
for every $\vec{o}\in\Sigma_{\mathcal{O}}$, we have
$(\vec{i},\vec{o},\vec{b},\vec{o})$ is accepting in the construction process
of $\mathcal{A}^{\prime}$ before removing the $\Sigma_{\mathcal{O}}$ letters
and determinizing. This means that $(\vec{i},\vec{b})\in
L(\mathcal{A}^{\prime})$. Therefore all in all we have that
$(\vec{i},\vec{b})$ is accepting in $\mathcal{A}^{\prime}_{1}$ and $\vec{b}$
is accepting in $\mathcal{A}^{\prime}_{2}$, thus $(\vec{i},\vec{b})$ is
accepting in $\mathcal{A}_{1}$ as required.

All is left is to we verify that $(\mathcal{A}_{1},\mathcal{A}_{R_{2}})$ meet
the condition for TDP/PDP, which done in the same way as in the proof of
Theorem 17. Again, the verification requires constructing the complement
$\mathcal{A}_{1}\circ\mathcal{A}_{R_{2}}$ which requires exponential time as
well as the complement of $Dom(\mathcal{A}_{1})$. Since these constructions
for verification purposes can also be done “on-the-fly” we conclude that the
over all complexity of proving the theorem is in EXPSPACE.

Finally for strategic PDP with a hint $T_{2}$ note that when $T_{2}$ is given
as a hint we do not need to construct $\mathcal{A}_{2}$, but simply construct
$\mathcal{A}_{1}$ from ${\mathcal{A}^{\prime}}_{R}^{t},T_{2}$ in the exact
construction as above. Then we check for emptiness. As before, if
$\mathcal{A}_{1}$ is empty then $T_{2}$ is not a good witness. Otherwise, we
get a transducer $T_{1}$ such that $(T_{1},T_{2})$ meet the Strategic PD
conditions. Note that this construction yields $T_{1}$ in polynomial time
therefore we overall have the following.

######  Theorem 25.

Strategic PDP with a hint $T_{2}$ is in PTIME.

###  6.3. Back to the undecidability conjecture

In Section 5.3.1 we conjectured that TDP/PDP for automatic relations is
undecidable. In this section we showed however that TDP/PDP are decidable for
automatic relations when given a hint. Can we leverage this idea towards
solving the problem of undecidability in full? That is, can we search for,
say, an automaton for $R_{1}$ that together with the maximal $R_{2}$
constructed, forms a solution for TDP/PDP?

It is tempting to try to use an automata-theoretic approach similar to the
strategic PDP (see Section 5.4) in which we consider representing
$R_{1}\subseteq(\Sigma_{\mathcal{I}}\times\Sigma_{\mathcal{B}})^{*}$ as a
labeled tree
$\tau_{1}:(\Sigma_{\mathcal{I}}\times\Sigma_{\mathcal{B}})^{*}\mapsto\\{0,1\\}$.
Then we can try to define a tree automaton $\mathcal{A}_{1}$ that accepts a
tree $\tau_{1}$ iff it is a correct hint for the total or partial
decomposition of an input/output relation
$R\subseteq(\Sigma_{\mathcal{I}}\times\Sigma_{\mathcal{B}})^{*}$. The
difficulty is that such an automaton has to check two properties of
$\tau_{1}$: (1) The domain of $R_{1}$ has to be equal to the domain of $R$.
This is essentially a requirement on the projection of $\tau_{1}$ on
$\Sigma_{\mathcal{I}}$. (2) The composition of $R_{1}$ with the maximal
$R_{2}$ is contained in or equal to $R$. This is essentially a requirement on
the projection of $\tau_{1}$ on $\Sigma_{\mathcal{B}}$. Known automata-
theoretic techniques exist for dealing with projection of trees, see for
example [27]. We currently, however, have no known technique to deal with two
orthogonal projections, as we have here.

Of course, this argument only shows that a particular technique to attack the
problem is unlikely to be successful. Therefore to further justify the
conjecture, we note that the dual-projection problem is reminiscent to the
problem of distributed temporal synthesis, which was shown to be undecidable
[40] (though there is no obvious formal connection between the decomposition
problem and the distributed-synthesis problem). There we are representing an
overall system strategy as a tree where tree labels correspond to actions of
system components and tree edges correspond to environment actions. When
different system components are expected to act independently, without
knowledge of actions by other components, the overall systems strategies has
to be decomposed into separate strategies as projections of the system
strategies.

##  7\. Discussion

We studied here a formal model of sequential decomposition, a fundamental
concept in computational thinking. We showed that while decomposition is
viewed as an approach to tame design complexity, complexity is not so easily
tamed and decomposition can be quite difficult when viewed as a computational
problem. Human intuition, used to offer hints to the decomposition algorithm,
is therefore necessary to tame the complexity of the decomposition problem.
The complexity of TDP/PDP in the automatic-relation setting, conjectured to be
undecidable, is still open. It is related to other decision problems for
automatic relations, cf. [30], and is a subject of future work.

The decomposition problems studied in this paper are specific to relational
decomposition, which arguably are enough to encode many types of
decomposition, for example a type of decomposition cover where the subproblems
overlap, or where the subproblems are required to satisfy certain properties
that would greatly reduce the search space. In that sense, as a further step
towards exploring other types of decomposition, another line of future work is
to explore the orthogonal problem of _parallel_ decomposition, in which a task
is decomposed into two tasks executed in parallel. This subject has been
studied in [1], but the specification of the system there is given by the
conjunction of its components’ specifications, while we study specifications
in terms of overall system input/output relations.

Finally a more practical approach to sequential decomposition can be found in
synthesis for symbolic settings. Indeed we showed in Section 5.2 that symbolic
TDP/PDP is NEXPTIME-complete, but this stands only when the size of the
intermediate domain $\mathcal{B}$ is given. For the synthesis approach we
relax this requirement so we get to choose $\mathcal{B}$. On one hand the
problem of solving TDP/PDP becomes uninteresting. On the other, however, The
challenge is to find a TDP/PDP solution $(R_{1},R_{2})$ that allows good
synthesis for a given relation $R$ in the sense that the composition of a
separate synthesis to $R_{2}$ and $R_{2}$ can be a synthesis solution to $R$.
A recent work inspired by this approach can be found in [9].

## References

  * [1] M. Abadi and L. Lamport.  Decomposing specifications of concurrent systems.  In Proc. IFIP Working Conference on Programming Concepts, Methods and Calculi, pages 327–340, 1994.
  * [2] S. Akshay, T. Antonopoulos, J. Ouaknine, and J. Worrell.  Reachability problems for Markov chains.  Inf. Process. Lett., 115(2):155–158, 2015.
  * [3] N. Amálio and C. Glodt.  A tool for visual and formal modelling of software designs.  Sci. Comput. Program., 98:52–79, 2015.
  * [4] J. L. Balcázar, A. Lozano, and J. Torán.  The complexity of algorithmic problems on succinct instances.  In Computer Science, pages 351–377. Springer, 1992.
  * [5] A. Basu, S. Bensalem, M. Bozga, J. Combaz, M. Jaber, T. Nguyen, and J. Sifakis.  Rigorous component-based system design using the BIP framework.  IEEE Software, 28(3):41–48, 2011.
  * [6] A. Benveniste, B. Caillaud, A. Ferrari, L. Mangeruca, R. Passerone, and C. Sofronis.  Multiple viewpoint contract-based specification and design.  In Proc. 6th International Symposium in Formal Methods for Components and Objects FMCO, pages 200–225, 2007.
  * [7] S. Bliudze, J. Sifakis, M. Bozga, and M. Jaber.  Architecture internalisation in BIP.  In Proc. 17th International Symposium on Component-Based Software Engineering, pages 169–178, 2014.
  * [8] A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili.  Regular model checking.  In Int’l Conf. on Computer-Aided Verification, pages 403–418. Springer, 2000.
  * [9] Supratik Chakraborty, Dror Fried, Lucas M. Tabajara, and Moshe Y. Vardi.  Functional synthesis via input-output separation.  In 2018 Formal Methods in Computer Aided Design, FMCAD 2018.
  * [10] C. Cheng, S. Bensalem, Y. Chen, R. Yan, B. Jobstmann, H. Ruess, C. Buckl, and A. Knoll.  Algorithms for synthesizing priorities in component-based systems.  In Proc. 9th International Symposium in Automated Technology for Verification and Analysis ATVA, pages 150–167, 2011.
  * [11] B. Das, P. Scharpfenecker, and J. Torán.  CNF and DNF succinct graph encodings.  Information and Computation, 2016.
  * [12] L. de Alfaro and T. A. Henzinger.  Interface theories for component-based sesign.  In Proc. First International Workshop on Embedded Software EMSOFT, pages 148–165, 2001.
  * [13] U. Fahrenberg and A. Legay.  General quantitative specification theories with modal transition systems.  Acta Inf., 51(5):261–295, 2014.
  * [14] J. Feigenbaum, S. Kannan, M. Y. Vardi, and M. Viswanathan.  The complexity of problems on graphs represented as obdds.  Chicago J. Theor. Comput. Sci., 1999, 1999.
  * [15] L. Fix, N. Francez, and O. Grumberg.  Program composition and modular verification.  In Proc. 18th Int. Colloq. on Automata, Languages, and Programming, pages 93–114, 1991.
  * [16] D. Fried, L.M. Tabajara, and M.Y. Vardi.  BDD-based Boolean functional synthesis.  In Proc. 28th Int’l Conf. on Computer Aided Verification, pages 402–421, 2016.
  * [17] H. Galperin and A. Wigderson.  Succinct representations of graphs.  Information and Control, 56(3):183–198, 1983.
  * [18] M. R. Garey and D. S. Johnson.  Computers and intractability: A guide to the theory of NP-Completeness.  W. H. Freeman, 1979.
  * [19] E. Grädel, W. Thomas, and T. Wilke.  Automata, Logics, and Infinite Games: A Guide to Current Research.  Lecture Notes in Computer Science 2500. Springer, 2002.
  * [20] C. A. R. Hoare.  An axiomatic basis for computer programming.  Commun. ACM, 12(10):576–580, 1969.
  * [21] J. E. Hopcroft, R. Motwani, and J. D. Ullman.  Introduction to automata theory, languages, and computation - international edition (2. ed).  Addison-Wesley, 2003.
  * [22] O. James.  Contentment in graph theory: covering graphs with cliques.  In Indagationes Mathematicae (Proceedings), volume 80, pages 406–424. Elsevier, 1977.
  * [23] D.S. Johnson.  The NP-completeness column: An ongoing guide.  Journal of algorithms, 8(2):285–303, 1987.
  * [24] R. M. Karp.  Reducibility among combinatorial problems.  In Proc. of a symposium on the Complexity of Computer Computations, pages 85–103, 1972.
  * [25] B. Khoussainov and A. Nerode.  Automatic presentations of structures.  In Proc. Workshop on Logic and computational complexity, LNCS 960, pages 367–392. Springer, 1995.
  * [26] D. Kozen.  Automata and computability.  Undergraduate texts in computer science. Springer, 1997.
  * [27] O. Kupferman and M.Y. Vardi.  Synthesis with incomplete informatio.  Advances in Temporal Logic, 16:109–127, 2000.
  * [28] O. Kupferman and M.Y. Vardi.  Synthesizing distributed systems.  In Proc. 16th IEEE Symp. on Logic in Computer Science, pages 389–398, 2001.
  * [29] E. Kushilevitz and N. Nisan.  Communication complexity.  Cambridge University Press, 1997.
  * [30] D. Kuske and M. Lohrey.  Some natural decision problems in automatic graphs.  J. of Symbolic Logic, pages 678–710, 2010.
  * [31] K. G. Larsen and L. Xinxin.  Equation solving using modal transition systems.  In Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS, pages 108–117, 1990.
  * [32] K. Guldstrand Larsen.  Modal specifications.  In Proc. Automatic Verification Methods for Finite State Systems, International Workshop, pages 232–246, 1989.
  * [33] Y. Lustig and M.Y. Vardi.  Synthesis from component libraries.  Software Tools for Technology Transfe, 15(5-6):603–618, 2013.
  * [34] N. Lynch and M. R. Tuttle.  An introduction to Input/Output automata.  CWI-quarterly, 2(3), 1989.
  * [35] J. Ouaknine and J. Worrell.  On the Positivity problem for simple linear recurrence sequences.  In Proc. ICALP, volume 8573 of LNCS. Springer, 2014.
  * [36] J. Ouaknine and J. Worrell.  On linear recurrence sequences and loop termination.  SIGLOG News, 2(2):4–13, 2015.
  * [37] C. H. Papadimitriou and M. Yannakakis.  A note on succinct representations of graphs.  Information and Control, 71(3):181–185, 1986.
  * [38] D.L. Parnas.  On the criteria to be used in decomposing systems into modules.  Commun. of the ACM, 15(12):1053–1058, 1972.
  * [39] A. Pnueli.  The temporal logic of programs.  In Proc. 18th Annual Symposium on Foundations of Computer Science, pages 46–57, 1977.
  * [40] A. Pnueli and R. Rosner.  Distributed reactive systems are hard to synthesize.  In Proc. 31st Annual Symposium on Foundations of Computer Science, pages 746–757, 1990.
  * [41] K. Rath, V. Choppella, and S.D. Johnson.  Decomposition of sequential behavior using interface specification and complementation.  VLSI Design, 3(3-4):347–358, 1995.
  * [42] S. Rubin.  Automatic structures.  PhD thesis, University of Auckland, New Zealand, 2004.
  * [43] Carsten Schürmann and Jatin Shah.  Representing reductions of np-complete problems in logical frameworks: a case study.  In Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003.
  * [44] M. Soittola.  On D0L synthesis problem.  In Automata, Languages, Development. North-Holland, 1976.
  * [45] H. Veith.  Languages represented by boolean formulas.  Inf. Process. Lett., 63(5):251–256, 1997.
  * [46] J. M. Wing.  Computational thinking.  Commun. ACM, 49(3):33–35, 2006.
  * [47] J. M. Wing.  Computational thinking.  In Proc. IEEE Symposium on Visual Languages and Human-Centric Computing, page 3, 2011.

##  Appendix A The reduction flow in Symbolic relations

For the article to be self contained, we describe the problems and the chain
of reductions that appear in the proof of Theorem 5. Each problem is followed
by it’s index number in [18]. The reduction are all from [24], apart from the
last one which is from [22] and its location is stated in details below.

##### The list of problems:

  * •

SAT (LO1): The language of all satisfiable CNF Boolean formulas with $U$
variables and $C$ clauses.

  * •

3SAT (LO2): The language of all satisfiable CNF Boolean formulas with $U$
variables and $C$ clauses where each clause $C$ contains $3$ literals.

  * •

KCOLORABILITY (GT4): The language of all graphs $G=(V,E)$ with $k>0$ for which
there exists a coloring function $f:V\leftarrow\\{1,\ldots,k\\}$ such that
$f(u)\not=f(v)$ for every edge $(u,v)\in E$.

  * •

PARTITIONCLIQUES (GT15): The language of all graphs $G=(V,E)$ with $k\leq|V|$
for which there exists a partition of $V$ into $V_{1},\ldots,V_{k}$ disjoint
sets such that for every $1\leq i\leq k$, the graph induced by $V_{i}$ is a
clique.

  * •

CCBS (GT18): (Covering by Complete Bipartite Subgraphs): The language of all
bipartite graphs $G=(V,E)$ with a positive integer $K\leq|E|$ for which there
are $k\leq K$ subsets $V_{1},\ldots,V_{k}$ of $V$ such that for every $1\leq
i\leq k$, the graph induced by $V_{i}$ is a complete bipratite subgraph of $G$
and such that for every edge $(u,v)\in E$, there is some $V_{i}$ such that
$(u,v)$ is contained in $V_{i}$.

  * •

CLIQUE (GT19): The language of all graphs $G=(V,E)$ with $k\leq|V|$ for which
there is a subset $V^{\prime}\subseteq V$ of size $k$ or more such that every
two vertices in $V$ are joint by an edge in $E$.

  * •

VC (GT1): The language of all graphs $G=(V,E)$ with $k\leq|V|$ for which there
is a subset $V^{\prime}\subseteq V$ of size $k$ or less such that for every
edge $(u,v)\in E$ either $u\in V$ or $v\in V$.

  * •

SC (SP5): The language of all $(S,C,K)$ where $C$ is a collection of all
subsets of a finite set $S$ and $K\leq|C|$ such that $C$ contains a cover of
$S$ of size $K$, i.e. there is a subset $C^{\prime}\subseteq C$ of size $K$ or
less such that every member in $S$ belongs to at least one member in
$C^{\prime}$.

##### The reductions:

  * •

$SAT\leq_{m}^{P}3SAT$: Every clause $(\ell_{1},\ldots,\ell_{j})$ in $C$ where
the $\ell_{i}$’s are literal, is converted to a set of clauses
$(\ell_{1}\vee\ell_{2}\vee a_{1})\wedge(\neg a_{1}\vee\ell_{2}\vee
a_{2})\wedge\ldots(\neg a_{k-3}\vee\ell_{k-1}\vee\ell_{k})$.

  * •

$3SAT\leq_{m}^{p}Kcolorability$: Let $F$ be a $3SAT$ formula with variables
$u_{1},\cdots u_{n}$ and clauses $C_{1},\cdots C_{r}$. Set $k=n+1$. Then
$G-(V,E)$ is as follows.
$V=\\{v_{1},\cdots,v_{n},v^{\prime}_{1},\cdots,v^{\prime}_{n},x_{1},\cdots
x_{n},c_{1},\cdots c_{r}\\}$. To construct $E$ set $(v_{i},v^{\prime}_{i})$
for every $i$, $(x_{i},x_{j})$,$(v_{i},x_{j})$ and $(v^{\prime}_{i},x_{j})$
for every $i\not=j$, and finally add $(v_{j},c_{i})$ if $u_{j}$ does not
appear in $C_{i}$ and add $(v^{\prime}_{j},c_{i})$ if $\neg u_{j}$ does not
appear in $C_{i}$. This reduction appeared in [43] as well.

  * •

$Kcolorability\leq_{m}^{p}PartitionCLIQUE$: Set $G^{\prime}$ to be the
complement of $G$. Then $(G,k)\in Kcolorability$ iff $(G^{\prime},k)\in
PartitionClique$.

  * •

$PartitionCLIQUE\leq_{m}^{p}CCBS$: Given a graph $G=(V,E)$ with
$v_{1},\cdots,v_{n}$ vertices and a non negative integer $k\leq n$, construct
a bipartite graph $G^{\prime}=(U,E^{\prime})$ in which $U=u_{1},\cdots
u_{n},w_{1},\cdots w_{n}$ are vertices, and in addition for every $i\not=j$
add vertices $u_{ij},w_{ij}$. Construct $E^{\prime}$ by setting edges
$(u_{i},w_{i})$ for every $i$, and for every $i\not=j$,
$(u_{i},w_{j}),(u_{ij},w_{ij}),(u_{ij},w_{j}),(w_{ij},u_{i})$. Then $(G,k)\in
PartitionClique$ if and only if $(G^{\prime},\ell)\in CCBS$ where
$\ell=k+|E|-|V|$. The reduction is shown in [22] as a proof of Theorem $8.1$
where $PartitionClique$ is described there as Problem $P_{0}$ and CCBS is
described as Problem $P_{2}$.

  * •

$SAT\leq_{m}^{p}CLIQUE$: Given a CNF formula $F$ with $C1,\cdots C_{p}$
clauses, we construct a graph $G=(V,E)$ where $V=\\{<\ell,i>\mid\ell\text{ is
a literal and occurs in }C_{i}$, and $E=\\{(<\ell,i>,<m,j>\mid i\neq
j\wedge\ell\neq\neg m\\}$. Then $F\in SAT$. if and only if $(G,p)\in CLIQUE$.

  * •

$Clique\leq_{m}^{P}VC$: Given a graph $G=(V,E)$ and a positive integer
$k\leq|V|$ we denote $G^{\prime}$ to be the complement of $G$ and
$k^{\prime}=|V|-k$. Then $(G^{\prime},k^{\prime})\in VC$ iff $(G,k)\in
Clique$.

  * •

$VC\leq_{m}^{P}SC$: Given a graph $G=(V,E)$ and a positive integer $k\leq|V|$,
let $C$ be the collection of all sets of edges $S_{i}$ incident on vertex $i$
for every $i\in V$. Then $(E,C,k)\in SC$ iff $(G,k)\in VC$.

##  Appendix B Supplementary definitions for Strategic PDP

Since the proof of Theorem 13 lies heavily on definitions and terminology from
[28], for containment of the paper we cite the definitions and theorems from
[28] that are of importance for the proof.

Given a finite set $\Upsilon$, a $\Upsilon$-tree is a set
$T\subseteq\Upsilon^{*}$ such that if $x\circ v\in T$ where $x\in\Upsilon^{*}$
and $v\in\Upsilon$ then also $x\in T$. When $\Upsilon$ is clear from the
context, we call $T$ a tree. When $T=\Upsilon^{*}$ we say that $T$ is full.
The elements of $T$ are called nodes, and the empty word $\epsilon$ is the
root of $T$. For every $x\in T$, the nodes $x\circ v\in T$ where
$v\in\Upsilon$ are the children of $x$. Each node $x$ of $T$ has a direction,
$dir(x)$ in $\Upsilon$. The direction of $\epsilon$ is $v^{0}$, for some
designated $v^{0}\in\Upsilon$, called the root direction. The direction of a
node $x\circ v$ is $v$.

Given two finite sets $\Upsilon$ and $\Sigma$, a $\Sigma$-labeled
$\Upsilon$-tree is a pair $(T,V)$ where $T$ is a $\Upsilon$-Tree and
$V:T\rightarrow\Sigma$ maps each node of $T$ to a letter in $\Sigma$. When
$\Upsilon$ and $\Sigma$ are not important or clear from the context, we call
$(T,V)$ a labeled tree.

For a $\Sigma$-labeled $\Upsilon$-tree $(\Upsilon^{*},V)$, we define the x-ray
of $(\Upsilon^{*},V)$, denoted $xray((\Upsilon^{*},V))$ as the
$(\Sigma\times\Upsilon)$-labeled $\Upsilon$-tree $(\Upsilon^{*},V^{\prime})$
in which each node is labeled by both its direction and its labeling in
$(\Upsilon^{*},V)$. Thus, for every $x\in\Upsilon^{*}$, we have
$V^{\prime}(x)=(dir(x),V(x))$.

An (alternating) tree-automaton that runs over full $\Sigma$-labeled
$\Upsilon$-tree is a tuple
$\mathcal{A}=(\Upsilon,\Sigma,Q,q_{0},\delta,\alpha)$, where $\Sigma,\Upsilon$
are finite alphabets, $Q$ is a finite set of states, $q_{0}$ is an initial
state, $\alpha\subseteq Q^{\omega}$ is an acceptance condition, and
$\delta:Q\times\Sigma\to B^{+}(\Upsilon\times Q)$ is the transition function,
where $B^{+}(\Upsilon\times Q)$ is the set of positive Boolean formulas over
$\Upsilon\times Q$. A special case, in which case the automaton is
_deterministic_ , is when the automaton sends at most one successor state in
each tree direction. Formally, this means that when considering a Boolean
transition condition $\delta(q,a)$, for $q\in Q$ and $a\in\Sigma$, in
disjunctive normal form, there is no disjunct (which is a conjunction) that
contains two distinct atoms $(q_{1},b)$ and $(q_{2},b)$ associated with the
same direction $b\in\Upsilon$.

A run of an alternating automaton $A$ on an input $\Sigma$-labeled
$\Upsilon$-tree $(\Upsilon^{*},V)$ is a tree $(T_{r},r)$ in which the nodes
are labeled by elements of $(\Upsilon^{*}\times Q)$. Each node of $T_{r}$
corresponds to a node of $\Upsilon^{*}$. A node in $T_{r}$, labeled $(x,q)$,
describes a copy of the automaton that reads the node $x$ of $T$ and visits
the state $q$. The label of the node and its children have to satisfy the
transition function. Each infinite path $\rho$ in $(T_{r},r)$ is labeled by a
word $r(\rho)$ in $Q^{\omega}$. Let $inf(\rho)$ denote the set of states in
$Q$ that appear in $r(\rho)$ infinitely often. A run $(T_{r},r)$ is accepting
iff all its infinite paths satisfy the acceptance condition. In Rabin
alternating automata, $\alpha\subseteq 2^{Q}\times 2^{Q}$, and an infinite
path $\rho$ satisfies an acceptance condition
$\alpha=\\{(G_{1},B_{1}),\cdots(G_{k},B_{k})\\}$ iff there exists $1\leq i\leq
k$ for which $inf(\rho)\cap G_{i}\not=\emptyset$ and $inf(\rho)\cap
B_{i}=\emptyset$. The number of pairs in $\alpha$ is called the index of
$\alpha$. An automaton accepts a tree if there is an accepting run on it. In
_Büchi_ automata, $\alpha\subseteq Q$, and an infinite path $\rho$ satisfies
an acceptance condition if $inf(\rho)\cap F\not=\emptyset$. The language of
the automaton $A$ is denoted $L(A)$. The automaton $A$ is said to be non-empty
if $L(A)\not=\emptyset$. The size of an alternating automaton is the length of
its description, which is typically dominated by the description of the
transition function.

We now bring Theorem $4.2$ from [28] as follows.
Theorem 4.2 from [28]: Given an alternating tree automaton $A$ over
$(\Upsilon\times\Sigma)$-labeled $\Upsilon$-trees, we can construct an
alternating tree automaton $A^{\prime}$ over $\Sigma$-labeled $\Upsilon$-trees
such that $A^{\prime}$ accepts a labeled tree $(\Upsilon^{*},V)$ iff $A$
accepts $xray((\Upsilon^{*},V))$ and the automata $A^{\prime}$ and $A$ have
the same size and index. We call $A^{\prime}$ the cover of $A$ and is denoted
by $cover(A)$.