# THE CHURCH SYNTHESIS PROBLEM OVER CONTINUOUS TIME

Alexander Rabinovich  Tel-Aviv University<EMAIL_ADDRESS>Daniel
Fattal  Tel-Aviv University<EMAIL_ADDRESS>
###### Abstract

Church’s Problem asks for the construction of a procedure which, given a
logical specification $\varphi(I,O)$ between input $\omega$-strings $I$ and
output $\omega$-strings $O$, determines whether there exists an operator $F$
that implements the specification in the sense that $\varphi(I,F(I))$ holds
for all inputs $I$. Büchi and Landweber provided a procedure to solve Church’s
problem for MSO specifications and operators computable by finite-state
automata. We investigate a generalization of the Church synthesis problem to
the continuous time of the non-negative reals. We show that in the continuous
time there are phenomena which are very different from the canonical discrete
time domain of the natural numbers.

##  1 Introduction

###  1.1 Church Synthesis Problem

Let Spec be a specification language and Pr be an implementation language. The
following problem is known as the Synthesis problem.

Synthesis problem
Input: A specification $S(I,O)\in Spec$. Question: Is there a program $P\in
Pr$ which implements it, i.e., $\forall I.\ S(I,P(I))$?

We first discuss the classical Church synthesis problem over discrete time
$\omega=(\mathbb{N},<)$, and then explain its generalization to continuous
time.

_The specification language_ for the Church Synthesis problem is the Monadic
Second-Order Logic of Order ($\mathit{MSO[<]}$). The monadic second-order
logic is the extension of the first-order logic by monadic predicates and
quantifications over them. We use lower case letters $x,y,z,\dots$ to denote
first-order variables and upper case letters $X,Y,Z,\dots$ to denote second-
order variables; The atomic formulas of $\mathit{MSO[<]}$ are $x<y$ and
$X(y)$. The formulas are constructed from the atomic formulas by boolean
connectives and the first-order and the second-order quantifiers. A formula
$\varphi(x_{0},\dots,x_{k-1},X_{0},\dots,X_{l-1})$ is a formula with free
variables among $x_{0},\dots,x_{k-1},X_{0},\dots,X_{l-1}$.

In an $\mathit{MSO[<]}$ formula $\varphi(X,Y)$, free variables $X$ and $Y$
range over monadic predicates over $\mathbb{N}$. Since each such monadic
predicate can be identified with its characteristic $\omega$-string, $\varphi$
defines a binary relation on $\omega$-strings. A function $F$ from
$\omega$-strings to $\omega$-strings is definable by $\varphi(X,Y)$ iff
$\forall X\forall Y(Y=F(X)\leftrightarrow\varphi(X,Y))$.

_Implementation:_ Functions from $\omega$-strings to $\omega$-strings. Such
functions are called operators. A machine that computes an operator at every
moment $t\in\mathbb{N}$ reads an input symbol $X(t)\in\\{0,1\\}$, updates its
internal state, and produces an output symbol $Y(t)\in\\{0,1\\}$. Hence, the
output $Y(t)$ produced at $t$ depends only on inputs symbols
$X(0),X(1),\dots,X(t)$. Such operators are called causal operators
(C-operators); if the output $Y(t)$ produced at $t$ depends only on inputs
symbols $X(0),\dots,X(t-1)$, the corresponding operator is called a strongly
causal (SC-operator).

Another property of interest is that the machine computing $F$ is finite-
state. In the light of Büchi’s proof [Bu62] of the expressive equivalence of
$\mathit{MSO[<]}$ and finite automata, $F$ is finite-state if and only if it
is $\mathit{MSO[<]}$-definable.

The following problem is known as the Church Synthesis problem over the
discrete time of naturals $\omega:=(\mathbb{N},<)$.

Church Synthesis problem
Input: an $\mathit{MSO[<]}$ formula $\Psi(X,Y)$. Question: Is there a
C-operator $F$ such that $\forall X\Psi(X,F(X))$ holds over
$\omega:=(\mathbb{N},<)$?

Büchi and Landweber [BL69] proved that the Church synthesis problem is
computable. Their main theorem can be stated as:

######  Theorem 1.

Let $\Psi(X,Y)$ be an $\mathit{MSO[<]}$ formula.

  1. 1.

Determinacy: exactly one of the following holds for $\Psi$:

    1. (a)

There is a C-operator $F$ such that $\omega\models\forall X.\ \Psi(X,F(X))$.

    2. (b)

There is a SC-operator $G$ such that $\omega\models\forall Y.\
\neg\Psi(G(Y),Y)$.

  2. 2.

Decidability: it is decidable whether 1 (a) or 1 (b) holds.

  3. 3.

Definability:

    1. (a)

If 1 (a) holds, then there is an $\mathit{MSO[<]}$ formula $U$ that defines a
C-operator which implements $\Psi$.

    2. (b)

Similarly for 1 (b).

  4. 4.

Computability: There is an algorithm such that for each $\mathit{MSO[<]}$
formula $\Psi(X,Y)$:

    1. (a)

If 1 (a) holds, constructs an $\mathit{MSO[<]}$ formula $\varphi(X,Y)$ that
defines $F$.

    2. (b)

Similarly for 1 (b).

Recall that a formula $U(X,Y)$ defines an operator $F$ if $\forall X\forall
Y(Y=F(X)\leftrightarrow U(X,Y))$. In the above theorem we use “C-operator
definable by an $\mathit{MSO[<]}$ formula” instead of an equivalent “operator
computable by a finite state transducer (automaton).” This will allow us to
lift this theorem to continuous time where finite state transducers were not
defined.

The proof of Theorem 1 is based on the fundamental connections between Logic,
Games and Automata.

Classical Automata theory results show an equivalence between three
fundamental formalisms: logical nets, automata and $\mathit{MSO[<]}$ logic.
Trakhtenbrot [Tra95] suggested a program to extend the classical results from
discrete time to other time domains.

In this work we investigate the Church synthesis problem over continuous time.

$\mathit{MSO[<]}$ has a natural interpretation over the non-negative reals
$(\mathcal{R}^{\geq 0},<)$.

Shelah [She75] proved that $\mathit{MSO[<]}$ is undecidable over the reals if
we allow quantification over arbitrary predicates. In Computer Science,
however, it is natural to restrict predicates to finitely variable (non-Zeno)
predicates,

A signal is a function $f$ from $\mathcal{R}^{\geq 0}$ into a finite set
$\Sigma$ such that $f$ satisfies the finite variability (non-Zeno) property:
there exists an unbounded increasing sequence $\tau_{0}=0<\tau_{1}<\cdots$
such that $f$ is constant on every open interval $(\tau_{i},\tau_{i+1})$. In
other words, $f$ is finitely variable if it has finitely many discontinuities
in any bounded sub-interval of $\mathcal{R}^{\geq 0}$.

We denote the structure for $\mathit{MSO[<]}$ over $(\mathcal{R}^{\geq 0},<)$
with the finite variability predicates as the interpretation for the monadic
variables, by $\mathit{FVsig}$; $\mathit{MSO[<]}$ over $\mathit{FVsig}$ is
decidable. The $C$-operators and $SC$-operators from signals to signals are
defined naturally: $F$ is a $C$ (respectively, SC) operator if the output
$F(X)$ at $t\in\mathcal{R}^{\geq 0}$ depends only on $X$ in the interval
$[0,t]$ (respectively, $[0,t)$). We investigate the following synthesis
problem:

Church Synthesis problem for continuous time
Input: an $\mathit{MSO[<]}$ formula $\Psi(X,Y)$. Question: Is there a
C-operator $F$ such that $\forall X.\ \Psi(X,F(X))$ holds in $\mathit{FVsig}$?

###  1.2 Results

It turns out that the discrete case and the case for continuous time are very
different. Here are our main results.

######  Theorem 2 (Indeterminacy).

The synthesis problem for continuous time is indeterminate.
There exists an $\mathit{MSO[<]}$ formula $\Psi(X,Y)$ such that

  1. 1.

There is no C-operator $F$ such that $\mathit{FVsig}\models\forall X.\
\Psi(X,F(X))$.

  2. 2.

There is no SC-operator $G$ such that $\mathit{FVsig}\models\forall Y.\
\neg\Psi(G(Y),Y)$.

######  Theorem 3 (Dichotomy Fails).

There exists an $\mathit{MSO[<]}$ formula $\Psi(X,Y)$ such that both

  1. 1.

There is a C-operator $F$ such that $\mathit{FVsig}\models\forall X.\
\Psi(X,F(X))$.

  2. 2.

There is a SC-operator $G$ such that $\mathit{FVsig}\models\forall Y.\
\neg\Psi(G(Y),Y)$.

######  Theorem 4 (Undefinability).

There exists $\Psi(X,Y)$ such that

  1. 1.

There is no $\mathit{MSO[<]}$-definable C-operator $F$ such that
$\mathit{FVsig}\models\forall X.\ \Psi(X,F(X))$.

  2. 2.

There is a C-operator $F$ such that $\mathit{FVsig}\models\forall X.\
\Psi(X,F(X))$.

Theorem 4 leads us to two natural questions: (1) Is it decidable whether a
formula is implementable by an $\mathit{MSO[<]}$-definable C-operator, and if
so, is a formula defining an implementation computable? (2) Is it decidable
whether a formula is implementable by some C-operator?
The following theorems answer these questions:

######  Theorem 5 (Computability of Definable Synthesis).

Given an $\mathit{MSO[<]}$ formula $\Psi(X,Y)$, it is decidable whether there
exists an $\mathit{MSO[<]}$-definable C-operator $F$ such that
$\mathit{FVsig}\models\forall X.\ \Psi(X,F(X))$ and if so, there is an
algorithm that constructs an $\mathit{MSO[<]}$ formula that defines $F$.

######  Theorem 6 (Decidability of Synthesis).

Given an $\mathit{MSO[<]}$ formula $\Psi(X,Y)$, it is decidable whether there
exists a C-operator $F$ such that $\mathit{FVsig}\models\forall X.\
\Psi(X,F(X))$.

The proofs of Theorems 2-5 are not difficult. The last theorem is our main
result.

###  1.3 Related Works

As far as we know the Church synthesis problem over continuous time was
considered only in [JORW11]. This paper considered only the _right continuous_
signals. A signal $f$ is right continuous if there is an unbounded increasing
sequence $\tau_{0}=0<\tau_{1}<\cdots$ such that $f$ is constant on every
interval $[\tau_{i},\tau_{i+1})$. Note that there is no non-constant SC-
operator from the right continuous signals to the right continuous signals.
Computability of Definable Synthesis (like Theorem 5) was proved there. In
[JORW11] we also considered $\mathit{MSO[<,+1]}$ \- the extension of
$\mathit{MSO[<]}$ by a metrical plus one function. This is a very strong logic
and it is undecidable over the reals; yet, it is decidable over any bounded
subinterval $[0,n]$ of the reals for every $n\in\mathbb{N}$. We proved
Computability of Definable Synthesis for $\mathit{MSO[<,+1]}$ for every
bounded interval.

Timed automata [AD94] are popular models of real-time systems. Timed automata
accept timed sequences - $\omega$-sequences annotated with real numbers. These
timed sequences are different from signals. Two-player games on timed automata
have been considered (see e.g., [CHP11, FLTM02]). These games are concurrent
games. Both players suggest a move simultaneously. Due to concurrency, timed
automata games are indeterminate. Patricia Bouyer writes that there is a
“prolific literature on timed games.” Unfortunately, “one paper = one
definition of timed games” which are parameterized by: “symmetrical games or
not, take care of Zeno (and Zeno-like) behaviours or not, turn-based games or
not, etc.”

We were unable to deduce our results from the results about timed automata
games.

###  1.4 Structure of the Paper

The paper is organized as follows. Section 2 preliminaries. Section 3 proves
Theorems 2 \- 4. In Section 4 computability of definable synthesis problem is
proved. Decidability of the Church synthesis problem is proved in Sections
5-6. Section 5 provides a proof for the right continuous signals and contains
the main ideas. Section 6 extends the proof to FV-signals. This proof is
longer and more technical, but does not require new insights. Section 7
contains Conclusion. The appendix contains a proof of a lemma.

##  2 Preliminaries

###  2.1 Monadic Second-Order Logic of Order

####  2.1.1 Syntax

The language of Monadic Second-Order Logic of Order ($\mathit{MSO[<]}$) has
individual variables, monadic second-order variables, a binary predicate $<$ ,
the usual propositional connectives and first and second-order quantifiers
$\exists^{1}$ and $\exists^{2}$. We use $t,~{}v$ for individual variables and
$X,~{}Y$ for second-order variables. It will be clear from the context whether
a quantifier is the first or the second-order and we will drop the
superscript. We use standard abbreviations, in particular, “$\exists!$” means
“there is a unique.”

The atomic formulas of $\mathit{MSO[<]}$ are formulas of the form: $t<v$ and
$X(t)$. The formulas are constructed from atomic formulas by using logical
connectives and first and second-order quantifiers.

We write $\psi(X,Y,t,v)$ to indicate that the free variables of a formula
$\psi$ are among $X,~{}Y,~{}t,~{}v$.

####  2.1.2 Semantics

A structure $K=\langle A,B<_{K}\rangle$ for $\mathit{MSO[<]}$ consists of a
set $A$ partially ordered by $<_{k}$ and a set $B$ of monadic functions from
$A$ into $\\{0,1\\}$. The letters $\tau,t,s,x,y$ will range over the elements
of $A$ and capital bold letter X,Y,Z,… will range over the elements of $B$. We
will not distinguish between a subset of $A$ and its characteristic function.
The satisfiability relation
$K,\tau_{1},\dots\tau_{m},\textbf{X}_{1}\dots\textbf{X}_{n}\models\psi(t_{1},\dots
t_{m},~{}X_{1},\dots X_{n})$ is defined in a standard way. We sometimes use
$K\models\psi(\tau_{1},\dots\tau_{m},~{}\textbf{X}_{1}\dots\textbf{X}_{n})$
for
$K,\tau_{1},\dots\tau_{m},\textbf{X}_{1}\dots\textbf{X}_{n}\models\psi(t_{1},\dots
t_{m},~{}X_{1},\dots X_{n})$.

We will be interested in the following structures:

  1. 1.

The structure $\omega=\langle\mathbb{N},2^{\mathbb{N}},<_{\mathbb{N}}\rangle$
where $2^{\mathbb{N}}$ is the set of all monadic functions from $\mathbb{N}$
into $\\{0,1\\}$.

  2. 2.

The signal structure $\mathit{FVsig}$ is defined as
$\mathit{FVsig}=\langle\mathcal{R}^{\geq 0},SIG,<_{R}\rangle$, where $SIG$ is
the set of finitely variable signals.

  3. 3.

A signal is right continuous if there there exists an unbounded increasing
sequence $\tau_{0}=0<\tau_{1}<\cdots$ such that $f$ is constant on every half-
open interval $[\tau_{i},\tau_{i+1})$. The right continuous signal structure
$Rsig$ is defined as $Rsig=\langle\mathcal{R}^{\geq 0},RSIG,<_{R}\rangle$
where $RSIG$ is the set of right continuous signals.

Terminology: For a FV variability (or RC) signal $f$ we say that $f$ is
_constant_ or _continuous_ at $t$ if there are $t_{1}<t<t_{2}$ such that $f$
is constant in the interval $[t_{1},t_{2}]$. If $f$ is not constant at $t$ we
say that it _jumps_ at $t$ or it is _discontinuous_ at $t$. In particular,
every signal jumps at $t=0$.

###  2.2 Coding

Let $\Delta$ be a finite set. We can code a function from a set $D$ to
$\Delta$ by a tuple of unary predicates on $D$. This type of coding is
standard, and we shall use explicit variables which range over such mappings
and expressions of the form “$F(u)=d$” (for $d\in\Delta$) in MSO-formulas,
rather than their codings.

Formally, for each finite set $\Delta$ we have second-order variables
$X_{1}^{\Delta},X_{2}^{\Delta},\dots$ which range over the functions from $D$
to $\Delta$, and atomic formulas $X_{i}^{\Delta}(u)=d$ for $d\in\Delta$ and a
first-order variable $u$ [TB73]. Often, the type of the second-order variables
will be clear from the context (or unimportant) and we drop the superscript
$\Delta$.

###  2.3 Definability

Let $\phi(X)$ be an $\mathit{MSO[<]}$ formula. We say that a language (set of
predicates) $L$ is definable by $\phi(X)$ in a structure $K$ if $L$ is the set
of monadic predicates which satisfies $\phi(X)$ in $K$.

Example (Interpretations of Formulas).

  1. 1.

Formula $\forall t_{1}\forall t_{2}.~{}t_{1}<t_{2}\wedge(\neg\exists
t_{3}.~{}t_{1}<t_{3}<t_{2})\to(X(t_{1})\leftrightarrow\neg X(t_{2}))$ defines
the $\omega$-language $\\{(01)^{\omega},~{}(10)^{\omega}\\}$ in the structure
$\omega$ and it defines the set of all signals in the signal structures, since
every set $X\subseteq\mathbb{R}^{\geq 0}$ satisfies this formula.

  2. 2.

Formula $\exists Y.~{}\exists t^{\prime}.Y(t^{\prime})\wedge(\forall
t.~{}X(t)\to Y(t))\wedge(\forall t_{1}\forall t_{2}.t_{1}<t_{2}\wedge
Y(t_{1})\wedge Y(t_{2})\to\exists t_{3}.t_{1}<t_{3}<t_{2}\wedge\neg Y(t_{3}))$
defines in the structure $\omega$ is the set of strings in which between any
two occurrences of 1 there is an occurrence of 0. In the signal structure, the
above formula defines the set of signals that receive value 1 only at isolated
points. The formula defines the empty language under the right continuous
signal interpretation.

In the above examples, all formulas have one free second-order variable and
they define languages over the alphabet $\\{0,1\\}$. A formula
$\psi(X_{1},\dots X_{n})$ with $n$ free second order variables defines a
language over the alphabet $\\{0,~{}1\\}^{n}$. We say that a $\omega$-language
is definable if it is definable by a monadic formula in the structure
$\omega$.

Let $\psi(X^{\Sigma_{in}},Y^{\Sigma_{out}})$ be an $\mathit{MSO[<]}$ formula.
We say that $\psi$ defines an operator $F$ if for all $X$ and $Y$: $\psi(X,Y)$
if and only if $Y=F(X)$.

[Speed independent signal language] Let $L$ be a signal language. $L$ is speed
independent if for each order preserving bijection $\rho:\mathcal{R}^{\geq
0}\to\mathcal{R}^{\geq 0}$:

$X\in L$ if and only if $\rho(X)\in L$.

It is clear:

######  Lemma 7.

The $\mathit{MSO[<]}$ definable languages are speed independent.

Moreover,

######  Lemma 8 (The output signal jumps only if input signal jumps).

if $F$ is an $\mathit{MSO[<]}$ definable operator and $F(\textbf{X})$ is
discontinuous at $t>0$, then X is discontinuous at $t$.

######  Proof 2.1.

Assume that $F$ is definable by $\psi(X,Y)$ and $\textbf{Y}=F(\textbf{X})$ is
discontinuous at $t>0$. If X is continuous at $t$, then there is an interval
$(a,b)$ such that $t$ is the only point of discontinuity of $(\textbf{X,Y})$
in $(a,b)$. Let $\rho:\mathcal{R}^{\geq 0}\to\mathcal{R}^{\geq 0}$ be an order
preserving bijection that is the identity map outside of $(a,b)$ and maps $t$
to $t^{\prime}\neq t$. Now $(\rho(\textbf{X}),\rho(\textbf{Y}))$ satisfies
$\psi$. Note that $\rho(\textbf{{X}})=\textbf{X}$. Hence, by the functionality
of $F$, $\rho(\textbf{Y})=\textbf{Y}$, and this is a contradiction, because
the only point of discontinuity of Y in $(a,b)$ is $t$, and the only point of
discontinuity of $\rho(\textbf{Y})$ in $(a,b)$ is $t^{\prime}\neq t$.

###  2.4 Parity Automata

A deterministic parity automaton is a tuple
$\mathcal{A}=(Q,\Sigma,\delta,q_{0},pr)$ that consists of the following
components:

  * •

$Q$ is a finite set. The elements of $Q$ are called the states of
$\mathcal{A}$.

  * •

$\Sigma$ is a finite set called the alphabet of $\mathcal{A}$.

  * •

$\delta~{}Q\times\Sigma\rightarrow Q$ is the transition function of
$\mathcal{A}$.

  * •

$q_{0}\in Q$ is the initial state.

  * •

$pr:~{}Q\rightarrow\mathbb{N}$ is the priority function.

An input for $\mathcal{A}$ is an $\omega$-sequence
$\alpha=\sigma_{0}\sigma_{1}\cdots$ over $\Sigma$. The run of $\mathcal{A}$
over $\alpha$ is an infinite sequence $\rho=(r_{0},r_{1},r_{2},\cdots$ of
states, defined as follows:

  * •

$r_{0}:=q_{0}$.

  * •

$r_{i+1}:=\delta(r_{i},\sigma_{i})$ for $i\geq 0$.

_Acceptance condition:_ Let $Inf(\rho)$ be the set of states that occur
infinitely often in $\rho$. $\mathcal{A}$ accepts exactly those runs $\rho$
for which $\min(pr(q)\mid q\in Inf(\rho))$ is even. An $\omega$-string
$\alpha$ is accepted if the run over $\alpha$ is accepted. An
$\omega$-language of $\mathcal{A}$ is the set of $\omega$-strings accepted by
$\mathcal{A}$.

The following fundamental result is due to Büchi:

######  Theorem 9.

An $\omega$-language is definable by an $\mathit{MSO[<]}$ formula if and only
if it is accepted by a deterministic parity automaton.

##  3 Proofs of Theorems 2 \- 4

###  3.1 Indeterminacy

See 2 To prove that the synthesis problem is indeterminate, for each
$x\in\mathcal{R}^{\geq 0}$ consider the following signal

$\delta_{x}(t):=\cases{1},&\text{if}t=x\\\ 0\text{else}$

Recall that a signal $X$ jumps at $t$ if it is not continuous at $t$. Let

$\Psi(X,Y):=\text{\exists t>0suchthatXisconstanton(0,t]andYjumpsatt}$

######  Proof 3.1 (Proof of Theorem 3).

  1. 1.

Assume that there exists a C-operator $F$ such that
$\mathit{FVsig}\models\forall X.\ \Psi(X,F(X))$.

Notice that for each $x>0$, since $\delta_{x}$ jumps at $x$ and constant on
$(0,x)$, we have the following equivalence

$\Psi(\delta_{x},F(\delta_{x}))\mbox{ iff }\text{\exists
t\in(0,x)suchthatF(\delta_{x})jumpsatt}$

Therefore, $\mathit{FVsig}\models\Psi(\delta_{1},F(\delta_{1}))$ implies that

$\textbf{(*)}\ \ \text{\exists t\in(0,1)suchthatF(\delta_{1})jumpsatt}$

By non-Zeno, there exists a minimal $t\in(0,1)$ that satisfies (*). Moreover,

    1. (a)

By causality, since $\delta_{1}=\delta_{t}$ on $[0,t)$ then
$F(\delta_{1})=F(\delta_{t})$ on $[0,t)$.

    2. (b)

By minimality, $F(\delta_{1})$ is constant on $(0,t)$. So by (a), both
$F(\delta_{1}),F(\delta_{t})$ are constant on $(0,t)$.

    3. (c)

By $\Psi(\delta_{t},F(\delta_{t}))$, $F(\delta_{t})$ jumps at some
$x\in(0,t)$. That is contradictory to (b).

  2. 2.

Assume that there exists a SC-operator $G$ such that
$\mathit{FVsig}\models\forall Y.\ \neg\Psi(G(Y),Y)$. By applying logical
equivalences we obtain:

$\neg\Psi(X,Y)\mbox{ iff }\forall
t>0.~{}\text{$X$jumpson$(0,t]${or}$Y$iscontinuousat$t$}$.

Therefore, for each $x\in\mathcal{R}^{\geq 0}$:
$\neg\Psi(G(\delta_{x}),\delta_{x})\mbox{ iff }\forall
t>0.~{}G(\delta_{x})\text{jumpson$(0,t]${or}$\delta_{x}$iscontinuousat$t$}$,
but since $\delta_{x}$ is not continuous at $x$, we obtain
$G(\delta_{1})\text{jumpson$(0,1]$}$.

Let $a$ be the first positive jump point of $G(\delta_{1})$. Since
$\delta_{1}=\delta_{a/2}$ on $[0,a/2)$ then by SC,
$G(\delta_{1})=G(\delta_{a/2})$ on $[0,a/2]$. Thus, $G(\delta_{a/2})$ is
constant on $(0,a/2]$ and $\delta_{a/2}$ jumps in $(0,a/2]$. We obtained a
contradiction to $\neg\Psi(G(\delta_{a/2}),\delta_{a/2})$.

###  3.2 Failure of dichotomy

See 3

For the proof of Theorem 3, consider the formula $\Psi$, the C-operator $F$
and the SC-operator $G$ given below

$\Psi(X,Y):=X=Y$ $F(X):=X$
$G(X)(t):=\cases{1}-a&\text{;ifXhasaconstantvalueaover(0,t)}\\\ 1\text{;else}$

It is clear that $F$ is a $C$-operator that implements $\Psi$. Below we prove
(2).

  1. [label=]

  2. 1.

$G$ is a strongly-causal operator: suppose $\textbf{X}_{1}=\textbf{X}_{2}$ on
$(0,t)$. It is either both $\textbf{X}_{1},\textbf{X}_{2}$ have a jump point
in $(0,t)$ or both are constant over $(0,t)$.
In the first case, by Non-Zeno, there exists $t_{0}\in(0,t)$ such that $t_{0}$
is the first jump point of both $\textbf{X}_{1},\textbf{X}_{2}$ in $(0,t)$.
Therefore, both $\textbf{X}_{1},\textbf{X}_{2}$ have a constant value $a$ over
$(0,t_{0})$. Thus, by definition

$\forall t\geq
0.~{}G(\textbf{X}_{1})(t)=G(\textbf{X}_{2})(t)=\cases{1}-a&t\in(0,t_{0})\\\
1else$

The proof for the second case is similar.

  3. 2.

$G$ implements $\neg\Psi$: for each signal Y there exists a non-empty interval
such that $\textbf{Y}\neq G(\textbf{Y})$ on it. Thus, $\textbf{Y}\neq
G(\textbf{Y})$.

###  3.3 Undefinability

See 4 Consider the formula $\Psi(X,Y):{=}\text{$Y$jumpsinside}(0,\infty)$.
It is implemented by $F(X)(t):=\cases{1},&\text{if}t=1\\\ 0,\text{else}$
When $X$ is constant on $[0,\infty)$, $Y$ should jump at $t>0$, where $X$ is
continuous. However, by Lemma 8, no $\mathit{MSO[<]}$-definable operator
implements $\Psi$. Hence, $\Psi$ is implemented by a C-operator, but it is not
implemented by a definable operator.

##  4 Computability of Definable Synthesis

In [JORW11] the computability of definable synthesis problem over the right
continuous signals was proved:

######  Theorem 10 (Computability of Definable Synthesis over the RC Signals).

Given an $\mathit{MSO[<]}$ formula $\Psi(X,Y)$, it is decidable whether there
exists an $\mathit{MSO[<]}$-definable C-operator $F$ such that
$RC\models\forall X.\ \Psi(X,F(X))$ and if so, there is an algorithm that
constructs an $\mathit{MSO[<]}$ formula that defines $F$.

In this section we extend this theorem to finite variability signals:

See 5 Our proof is a variation of the proof of Theorem 10.

In the next subsection we recall a relationship between finite variability
signals and $\omega$-strings. In subsection 4.2 we discuss definable
operators. Finally, in subsection 4.3 we present an algorithm for the
definable synthesis problem.

###  4.1 FV-signals and $\omega$-strings

We recall the relationship between finite variability signals and
$\omega$-strings.

Let $X$ be a finite variability signal over $\Sigma$ and let
$\widetilde{\tau}:=0=\tau_{0}<\tau_{1}<\cdots<\tau_{n}<\cdots$ be an
$\omega$-sequence of reals such that $X$ is constant on every interval
$(\tau_{i},\tau_{i+1})$ and $\lim\tau_{i}=\infty$. We say that such
$\widetilde{\tau}$ is a sample sequence for $X$. In other words, an unbounded
$\omega$-sequence is a sampling sequence for $X$ if it contains all the points
of discontinuity of $X$.

We define

  * •

$D(X,\widetilde{\tau})$ be an $\omega$-string
$(a_{0},b_{0})(a_{1},b_{1})\dots(a_{i},b_{i})\dots$ over $\Sigma\times\Sigma$
defined as $a_{i}:=X(\tau_{i})$ and $b_{i}$ is the value of $X$ in
$(\tau_{i},\tau_{i+1})$. We say that $D(X,\tau)$ represents $X$.

  * •

$D(X):=\\{D(X,\widetilde{\tau})\mid\widetilde{\tau}$ is a sample sequence for
$X\\}$.

  * •

For a signal language $L$ define $D(L):=\cup_{X\in L}D(X)$.

Observe that if an $\omega$-string $U$ represents a signal $X$ and $\rho$ is
an order preserving bijection over non-negative reals, then $U$ represents
$\rho(X)$.

  * •

For an $\omega$-string $U=(a_{0},b_{0})(a_{1},b_{1})\dots(a_{i},b_{i})\dots$
over $\Sigma\times\Sigma$ and an unbounded $\omega$-sequence
$\widetilde{\tau}:=0=\tau_{0}<\tau_{1}<\cdots<\tau_{n}<\cdots$ of reals define
a finite variability signal:

$FV(U,\widetilde{\tau})$ to be $a_{i}$ at $\tau_{i}$ and $b_{i}$ in the
interval $(\tau_{i},\tau_{i+1})$.

  * •

$FV(U):=\\{FV(U,\widetilde{\tau})\mid\widetilde{\tau}$ is an unbounded
$\omega$-sequence $\\}$.

  * •

For an $\omega$-language $L$ define: $FV(L):=\cup_{U\in L}FV(U)$.

The following theorem was proved in [Rab02]:

######  Theorem 11.

A finitely variable signal language $S$ is $\mathsf{MSO}$-definable if and
only if there is an $\mathsf{MSO}$-definable $\omega$-language $L$ such that
$S=FV(L)$. Moreover, (1) there is an algorithm that from an $\mathsf{MSO}$
formula $\varphi(X^{\Sigma})$ computes an $\mathsf{MSO}$-formula
$\varphi^{D}(X^{\Sigma\times\Sigma})$ such that if $S$ is a signal language
definable by $\varphi$ then $D(L)$ is definable by $\varphi^{D}$, and (2)
there is an algorithm that from an $\mathsf{MSO}$ formula
$\varphi(X^{\Sigma\times\Sigma})$ computes an $\mathsf{MSO}$-formula
$\varphi^{FV}(X^{\Sigma})$ such that if $L$ is an $\omega$-language definable
by $\varphi$ then $FV(L)$ is definable by $\varphi^{FV}$.

Note also that if $L$ is a definable signal language, then $L=FV(D(L))$.
However, for a definable $\omega$-language $L$, it might be the case that
$L\neq D(FV(L))$.

[Stuttering Equivalence] Two $\omega$-strings are stuttering equivalent if
there is a signal $X$ which is represented by both of them. Equivalently, the
sets of signals represented by these strings coincide. [Stuttering Free] An
$\omega$-string $U$ is stuttering free if there is a signal $X$ such that (1)
or (2) holds.

  1. 1.

$X$ has an infinitely many points of discontinuity and
$U=D(X,\widetilde{\tau})$ where $\widetilde{\tau}$ is a sample sequence that
contains exactly all points of discontinuity of $X$, or

  2. 2.

$X$ has $k$ points of discontinuity $0=\tau_{0}<\tau_{1}<\cdots<\tau_{k-1}$,
and $U=D(X,\widetilde{\tau})$, where
$\widetilde{\tau}:=0=\tau_{0}<\tau_{1}<\cdots<\tau_{k-1}<\tau_{k}<\cdots$,
where $\tau_{i}$ (for $i<k$) are the points of discontinuity of $X$, and
$\tau_{j}$ for $j\geq k$ are arbitrary.

######  Lemma 12.

  1. 1.

For every signal $X$, all strings in $D(X)$ are stuttering equivalent.

  2. 2.

Every $\omega$-string $V$ is stuttering equivalent to a unique stuttering free
string $U$.

Stuttering free $\omega$-strings can be characterized as follows.

######  Lemma 13.

An $\omega$-string $U$ over $\Sigma\times\Sigma$ is stuttering-free if it
satisfies the following condition: if $i$-th letter of $U$ is $(a,b)$ and
$i+1$-th letter is $(b,b)$, then for all $j>i$, $j$-th letter of $U$ is
$(b,b)$.

Hence,

######  Lemma 14 (Stuttering free strings are definable).

There is an $\mathit{MSO[<]}$ formula that defines the set of stuttering free
$\omega$-strings over $\Sigma\times\Sigma$.

###  4.2 Definable Operators

Let $\alpha(X^{\Sigma^{2}_{in}},Y^{\Sigma^{2}_{out}})$ be a formula. It
defines an $\omega$-language over $\Sigma^{2}_{in}\times\Sigma^{2}_{out}$. To
an $\omega$-string over $\Sigma^{2}_{in}\times\Sigma^{2}_{out}$ in a natural
way corresponds an $\omega$-string over $(\Sigma_{in}\times\Sigma_{out})^{2}$
and an $\omega$-string over $\Sigma_{in}\times\Sigma_{out}$. Hence, we can
consider $\alpha$ as defining an $\omega$-language over
$\Sigma_{in}\times\Sigma_{out}$. We say that $\alpha$ defines a C-operator
(respectively, SC-operator), if its language is the graph of this operator.

######  Lemma 15.

Let $\alpha(X^{\Sigma^{2}_{in}},Y^{\Sigma^{2}_{out}})$ be a formula such that

  1. 1.

If $(X^{\Sigma^{2}_{in}},Y^{\Sigma^{2}_{out}})$ satisfies $\alpha$, then
$X^{\Sigma^{2}_{in}}$ is stuttering free.

  2. 2.

For every stuttering free $X$ there is a unique $Y$ such that $(X,Y)$
satisfies $\alpha$.

Then, $\alpha^{FV}$ defines an operator on signals. Moreover, if in addition
$\alpha$ defines C-operator (respectively, SC-operator) on $\omega$-strings,
then $\alpha^{FV}$ defines C-operator (respectively, SC-operator) on FV-
signals.

######  Lemma 16.

If there is a definable C-operator that implements
$\Psi(X^{\Sigma_{in}},Y^{\Sigma_{out}})$ over FV-signals, then there is a
definable C-operator that implements $\Psi^{D}$ (over $\omega$).

######  Proof 4.1.

Assume $\alpha$ defines C-operator that implements
$\Psi(X^{\Sigma_{in}},Y^{\Sigma_{out}})$. We claim that $\alpha^{D}$ defines a
C-operator that implements $\Psi^{D}$ (over $\omega$). First,
$\alpha^{D}\rightarrow\psi^{D}$. Now, for every
$U\in(\Sigma^{2}_{in})^{\omega}$ there is a FV signal $X$ and
$\widetilde{\tau}$ such that $U=D(X,\widetilde{\tau})$. Let $Y$ be such that
$\alpha(X,Y)$ holds. Since $Y$ changes only when $X$ changes,
$\widetilde{\tau}$ is also a sample sequence for $Y$, Let
$V:=D(Y,\widetilde{\tau})$. It is clear that $\alpha^{D}(U,V)$. Therefore, for
every $U$ there is $V$ such that $\alpha^{D}(U,V)$. It remains to show that
such $V$ is unique. Indeed, if there are $V_{1}$ and $V_{2}$ such that both
$(U,V_{1})$ and $(U,V_{2})$ satisfy $\alpha^{D}$, then for arbitrary
$\widetilde{\tau}$, $FV((U,V_{1}),\widetilde{\tau})$ and
$FV((U,V_{2}),\widetilde{\tau})$ satisfy $\alpha$. However,
$FV(V_{1},\widetilde{\tau})\neq FV(V_{2},\widetilde{\tau})$ and both are
$\alpha$ related to $FV(U,\widetilde{\tau})$. This contradicts that $\alpha$
defines an operator on signals.

Causality and strong causality are immediate.

Recall that Lemma 8 states: if $F$ is a definable operator on finite
variability signals, then: $F(X)$ is not continuous at $t$ only if $X$ is not
continuous at $t$.

######  Lemma 17.

Let $\Psi(X^{\Sigma_{in}},Y^{\Sigma_{out}})$ be in $\mathit{MSO[<]}$ and let
$F$ be an $\mathit{MSO[<]}$ definable C-Operator (or SC-operator).
Denote $\Psi^{*}(X^{\Sigma_{in}},Y^{\Sigma_{out}}):=$

$\Psi\land\text{\forall t\in(0,\infty),if{X}iscontinuousatt,thensois{Y}}\land$
$\text{if{X}isleft-continuousatt,thensois{Y}.}$

Then

$\text{Fimplements\Psi\iff Fimplements\Psi^{*}.}$

###  4.3 Algorithm

Now, we are ready to present an algorithm that verifies whether there is a
definable C-operator that implements an $\mathit{MSO[<]}$ formula over FV-
signals, and if so it computes an $\mathit{MSO[<]}$ formula that defines such
an operator.

Algorithm Let $\Psi(X^{\Sigma_{in}},Y^{\Sigma_{out}})$ be an $\mathit{MSO[<]}$
formula and let $\Psi^{*}$ be defined as in Lemma 17. Use Büchi-Landweber
algorithm to decide whether there is a C-operator that implements
$(\Psi^{*})^{D}$ over $\omega$. If the answer is “NO,” then there is no
$\mathit{MSO[<]}$ definable C-operator that implements $\Psi$. If $\alpha$
defines a C-operator that implements $(\Psi^{*})^{D}$ over $\omega$, then let
$\alpha_{sf}:=\alpha(X^{\Sigma^{2}_{in}},Y^{\Sigma^{2}_{out}})\land\mbox{``$X$
is stuttering free'.'}$ Let $\beta:=(\alpha_{sf})^{FV}$. Then, $\beta$ defines
a C-operator that implements $\Psi$.

######  Proof 4.2 (Correctness of the algorithm.).

If the answer is “NO,” the correctness follows from Lemma 16 and Lemma 17.

If the algorithm returns $\beta$, the correctness follows from Lemma 15 and
Lemma 17.

The algorithm that decides whether there is a SC-definable operator on FV-
signals that implements $\Psi$ is almost the same: replace everywhere
“C-operator” by “SC-operator.”

##  5 Games and the Church Problem

Our aim is to show that the Church Synthesis problem is computable for FV
signals. Here, we provide a proof of decidability of Church’s synthesis
problem over right continuous signals. It contains all the main ideas but
slightly simpler than the proof for FV signals. In the next section we outline
its extension to FV signals.

We start with a reduction to a game. Let $\Psi(X,Y)$ be a formula. Consider
the following two-player game $\mathcal{G}_{\Psi}$. During the play
$\mathcal{I}~{}$constructs a (timed sequenced for) input signal $X$ and
$\mathcal{O}~{}$constructs an output $Y$.

Round 0. Set $t_{0}:=0$.

  1. 1.

$\mathcal{I}~{}$chooses a value $a_{0}\in\Sigma_{in}$ which holds at $t_{0}$
and for a while after $t_{0}$.

  2. 2.

$\mathcal{O}~{}$responses with a timed $\omega$-sequence (equivalently, with a
signal $Y_{0}$ on $[t_{0},\infty)$).

Now, $\mathcal{I}~{}$has two options:

A) $\mathcal{I}~{}$accepts. In this case, the play ends.
$\mathcal{I}~{}$constructed $X$ which has $a_{0}$ at all $t\geq 0$, and
$\mathcal{O}~{}$constructed $Y:=Y_{0}$ \- the signal chosen by $\mathcal{O}$.

B) $\mathcal{I}~{}$interrupts at some $t_{1}>t_{0}$ by choosing $a_{1}\neq
a_{0}$ which holds at $t_{1}$ and for a while after $t_{1}$. $X^{\prime}_{0}$
constructed by $\mathcal{I}~{}$is $a_{0}$ in $[t_{0},t_{1})$ and is $a_{1}$ at
$t_{1}$, $Y^{\prime}_{0}$ constructed by $\mathcal{O}~{}$is the restriction of
$Y_{0}$ on the interval $[t_{0},t_{1})$. Now, proceed to step 1 of round 1.

Round $i+1$.

  1. 1.

$\mathcal{O}~{}$chooses a timed $\omega$-sequence (equivalently, a signal)
$Y^{\prime}_{i+1}$ on $[t_{i+1},\infty)$.

  2. 2.

Now, $\mathcal{I}~{}$has two options.

A) $\mathcal{I}~{}$accepts. In this case, the play ends. The signal $X$
constructed by $\mathcal{I}~{}$coincides with $X^{\prime}_{i}$ on
$[0,t_{i+1})$ and equal to $a_{i+1}$ on $[t_{i+1},\infty)$. The signal $Y$
constructed by $\mathcal{O}~{}$coincides with $Y^{\prime}_{i}$ on
$[0,t_{i+1})$ and with $Y^{\prime}_{i+1}$ on $[t_{i+1},\infty)$.

B) $\mathcal{I}~{}$interrupts at some $t_{i+2}>t_{i+1}$ by choosing
$a_{i+2}\neq a_{i+1}$ for $X$ at $t_{i+2}$ and for a while after it. In this
case, $X^{\prime}_{i+1}$ is the signal that has value $a_{i+1}$ on
$[t_{i+1},t_{i+2})$ and extends the signal $X^{\prime}_{i}$ constructed in the
previous steps on $[0,t_{i+1})$, and $Y^{\prime}_{i+1}$ coincides with
$Y^{\prime}_{i}$ on $[0,t_{i+1})$ and coincides with $Y^{\prime}_{i+1}$ on
$[t_{i+1},t_{i+2})$. Start round $i+2$.

After $\omega$ rounds, if $\lim t_{i}=\infty$, we define $X$ (respectively,
$Y$) to be the signal that coincides with $X^{\prime}_{i}$ (respectively, with
$Y^{\prime}_{i})$ on $[t_{i},t_{i+1})$ for every $i$.

_Winning conditions._ $\mathcal{O}~{}$wins the play iff $\Psi(X,Y)$ holds or
$\mathcal{I}~{}$interrupts infinitely often and the duration of the play
$<\infty$, i.e., $\lim t_{n}<\infty$, where $t_{n}$ is the time of $n$-th
interruption.

Note that in this game, player $\mathcal{I}~{}$has much more power than
$\mathcal{O}$. $\mathcal{O}~{}$provides a signal till infinity and
$\mathcal{I}~{}$observes it and can interrupt it at any time moment she
chooses. Nevertheless, we have the following lemma.

######  Lemma 18 (Reduction to games).

$\mathcal{O}~{}$wins $\mathcal{G}_{\Psi}$ if and only if there is a C-operator
that implements $\Psi$.

Assume that $\Psi$ expresses that $Y$ has a discontinuity at some $t>0$ where
$X$ is continuous. Let us describe a winning strategy for $\mathcal{O}$. At
$i$-th move $\mathcal{O}~{}$chooses a signal which has value $X(t_{i})$ at
$[t_{i},t_{i}+\frac{1}{2^{i}})$ and $\neg X(t_{i})$ at $t\geq
t_{i}+\frac{1}{2^{i}}$. It is clear that this is a winning strategy for
$\mathcal{O}$. Indeed, in order to ensure that $\Psi$ fails, at the $i$-th
round, $\mathcal{I}~{}$should interrupt at $t_{i+1}$ before
$t_{i}+\frac{1}{2^{i}}$. Therefore, the duration of such a play $<\sum
2^{-i}=2<\infty$. Hence, $\mathcal{O}~{}$wins.

######  Proof 5.1 (Proof of Lemma 18).

$\Rightarrow$-direction. Let $\sigma$ be an $\mathcal{O}$’s winning strategy.
Consider the play where $\mathcal{I}~{}$ignores $\mathcal{O}$’s moves and
constructs an input signal $X$. Let $Y$ be the signal constructed by
$\mathcal{O}~{}$in this play, This defines a $C$-operator, and $\Psi(X,Y)$
holds.

$\Leftarrow$-direction. Assume that $F$ is a $C$-operator that implements
$\Psi$. Define a winning strategy for $\mathcal{O}~{}$in an obvious way.

Round 0. If $\mathcal{I}~{}$chooses $a_{0}$, then $\mathcal{O}~{}$replies by
$F(X_{0})$ the output produced to the input signal equal $a_{0}$ everywhere.
If $\mathcal{I}~{}$interrupts at $t_{1}>t_{0}$ and chooses $a_{1}\neq a_{0}$,
then $\mathcal{O}~{}$replies by $Y^{\prime}_{1}$, where $Y^{\prime}_{1}$ is
the restriction of $Y_{1}=F(X_{1})$ and $X_{1}$ is $a_{0}$ on $[0,t_{1})$ and
$a_{1}$ on $[t_{1},\infty)$.

Continue in a similar way for the other rounds. This strategy is winning for
$\mathcal{O}$.

###  5.1 An automaton Game

Let $\mathcal{A}$ be a deterministic parity automaton equivalent to
$\Psi^{D}$. We modify $\mathcal{G}_{\psi}$ game as follows. Player
$\mathcal{O}~{}$chooses signals (equivalently, timed sequences) over the set
$Q:=Q_{\mathcal{A}}$ of states of $\mathcal{A}$, instead of timed sequences
over $\Sigma_{out}$. Of course, the sequences should be consistent with the
behavior of $\mathcal{A}$. A play is winning for $\mathcal{O}~{}$if the
constructed $\omega$-sequence satisfies the acceptance conditions of
$\mathcal{A}$. Alternatively, we can pretend that $\mathcal{O}~{}$chooses a
timed sequence over $\Sigma_{out}$. However, we are interested in the
corresponding sequences over $Q$.

Here is a modified game $\mathcal{G}_{\mathcal{A}}$ on the automaton
$\mathcal{A}$ equivalent to $\Psi^{D}$.

$\mathcal{G}_{\mathcal{A}}$ Game Round 0 Replace in step 2
“$\mathcal{O}~{}$responses…” by “$\mathcal{O}~{}$responses with a timed
$\omega$-sequence $Y_{0}=(q_{1},\tau_{1}),\cdots(q_{k},\tau_{k})\cdots$ over
$Q$ such that $\tau_{1}>t_{0}$ and
$q_{i+1}=\delta_{\mathcal{A}}(q_{i},(a_{0},b_{i}))$ for some
$b_{i}\in\Sigma_{out}$ and all $i\geq 0$.” Round $i+1$ In Step 1, replace by
“$\mathcal{O}~{}$chooses a timed $\omega$-sequence over
$Y^{\prime}_{i+1}:=(q_{1},\tau_{1}),\cdots(q_{k},\tau_{k})\cdots$ over $Q$
such that $\tau_{1}>t_{i+1}$ and
$q_{k+1}=\delta_{\mathcal{A}}(q_{k},(a_{i+1},b_{k}))$ for some
$b_{k}\in\Sigma_{out}$ and all $k\geq 0$, where $q_{0}$ is the last state of
$Y^{\prime}_{i}$.” Winning Condition $\mathcal{O}~{}$wins if either the
sequence of states produced by $\mathcal{O}~{}$is accepted by $\mathcal{A}$,
or there were infinitely many moves, but $\lim t_{i}$ is finite.

The following is immediate.

######  Lemma 19 ($\mathcal{G}_{\psi}$ and $\mathcal{G}_{\mathcal{A}}$ are
equivalent).

$\mathcal{O}~{}$wins in $\mathcal{G}_{\Psi}$ if and only if
$\mathcal{O}~{}$wins in $\mathcal{G}_{\mathcal{A}}$.

Now, we are going to restrict $\mathcal{O}~{}$moves. The first restriction is
a time schedule. When $\mathcal{O}~{}$chooses a timed sequence (equivalently a
signal), we require that the distance between consecutive jumps in this signal
should be the same. We call such a signal _simple timed_. Another restriction
is on the sequence of values. We require that this sequence is ultimately
periodic.

In the next subsection we describe the ultimately periodic sequences that we
need.

###  5.2 Ultimately Periodic Sequences

[Ultimately periodic strings] An $\omega$-string $w$ is ultimately periodic if
$w=uv^{\omega}$ for some (finite) string $u$ and $v$; $v$ (respectively, $u$)
is the periodic (respectively, pre-periodic or lag) part of $w$; the length of
$v$ (respectively, of $u$) is period(respectively, lag) of $w$. We denote by
$u[n]$ the $n$-th letter of a string $u$ and by $u[k,m)$ the set of letters
$\\{u[i]\mid k\leq i<m)\\}$. [$\equiv_{state}$-equivalence on finite strings]
Let $\mathcal{A}$ be an automaton over a set $Q$ of states and let $u,v$ be
finite strings over $Q$. We say that $u$ is equivalent to $v$ (notation
$u\equiv_{state}v$) if and only if

  1. 1.

$u$ and $v$ have the same first state and the same last state.

  2. 2.

For every $m$ there is $n$ such that $u[m]=v[n]$ and the states that appear in
$u[0,m)$ are the same as the states that appear in $v[0,n)$.

  3. 3.

Symmetrically, for every $n$ there is $m$ such that $u[m]=v[n]$ and the states
that appear in $u[0,m)$ are the same as the states that appear in $v[0,n)$.

  4. 4.

$u$ is run of $\mathcal{A}$ if and only if $v$ is a run of $\mathcal{A}$.

To be formal we have to use notations $u\equiv_{state}^{\mathcal{A}}v$ to
emphasize that this equivalence relation is parameterized by $\mathcal{A}$.
However, $\mathcal{A}$ will be clear from the context or unimportant and we
will use $\equiv_{state}$ instead of $\equiv_{state}^{\mathcal{A}}$.

The next lemma summarizes properties of $\equiv_{state}$-equivalence:

######  Lemma 20 (Properties of $\equiv_{state}$).

For every $\mathcal{A}$:

  1. 1.

$\equiv_{state}$ has finitely many equivalence classes.

  2. 2.

$\equiv_{state}$ is a congruence with respect to concatenation, i.e., if
$u_{1}\equiv_{state}v_{1}$ and $u_{2}\equiv_{state}v_{2}$, then
$u_{1}u_{2}\equiv_{state}v_{1}v_{2}$.

  3. 3.

For every $\omega$-string $\pi$ there are $u_{0},\dots,u_{n}\dots$ such that
$\pi=u_{0}\cdots u_{n}\cdots$ and
$u_{i}\equiv_{state}u_{j}\equiv_{state}u_{i}u_{i+1}$ for all $i,j>0$ and
$u_{0}\equiv_{state}u_{0}u_{1}$.

######  Proof 5.2.

(1) and (2) are immediate. (3) will be proved in the Appendix.

[Equivalence on $\omega$-strings] Let $\mathcal{A}$ be an automaton over a set
$Q$ of states, and let $u,v$ be $\omega$-strings over $Q$. We say that $u$ is
equivalent to $v$ iff

  1. 1.

$Inf(u)=Inf(v)$, i.e., a state appears infinitely often in $u$ iff it appears
infinitely often in $v$.

  2. 2.

for every $m$ there is $n$ such that $u[m]=v[n]$ and the states that appear in
$u[0,m)$ are the same as the states that appear in $v[0,n)$,

  3. 3.

Symmetrically, for every $n$ there is $m$ such that $u[m]=v[n]$ and the states
that appear in $u[0,m)$ are the same as the states that appear in $v[0,n)$.

  4. 4.

$u$ is a run of $\mathcal{A}$ if and only if $v$ is a run of $\mathcal{A}$.

The next lemma is immediate. It deals with the concatenations of
$\omega$-sequences of finite strings.

######  Lemma 21.

if $u_{i}\equiv_{state}v_{i}$ for $i\in\omega$, then $u_{0}u_{1}\dots$ is
equivalent to $v_{0}v_{1}\dots$

From Lemma 21 and Lemma 20 we obtain:

######  Lemma 22.

For every automaton $\mathcal{A}$ over a set $Q$ of states there is a finite
set of ultimately periodic strings $UP(Q)$ such that for every $\omega$-run
$\pi$ of $\mathcal{A}$ there is $w=uv^{\omega}\in UP(Q)$ which is equivalent
to $\pi$ and $v\equiv_{state}vv$ and $u\equiv_{state}uv$.

######  Proof 5.3.

For each $\equiv_{state}$-equivalence class (over finite strings) chose a
representative $u$. Let $u_{1},\dots,u_{k}$ be the representatives. A
$\equiv_{state}$-equivalence class $C$ is idempotent if $uv\equiv_{state}u$
for every $u,v\in C$, equivalently $uu\equiv_{state}u$ for an element $u\in
C$. Define $UP(Q):=\\{u_{i}u_{j}^{\omega}\mid u_{i}$ and $u_{j}$ are
representatives, and $u_{j}$ is in an idempotent class and
$u_{i}u_{j}\equiv_{state}u_{i}\\}$. Lemma 20(3) implies that every
$\omega$-string is equivalent to a string in $UP(Q)$.

Let $d_{Q}:=\max\\{|u|\mid u$ is the representative of its
$\equiv_{state}$-equivalence class$\\}$. Then, $d_{Q}$ is an upper bound on
the length of periods $v$ and lags of $\omega$-strings in $UP(Q)$.

######  Lemma 23.

Assume $v\equiv_{state}vv$ and $u\equiv_{state}uv$ and
$w=uv^{\omega}=q_{1}q_{2}\cdots$. Let $n$ and $m$ be the lengths of $u$ and
$v$ respectively. Let $S_{u}$ be the set of states that appear in $u$. Then,
for every $l\geq m$, the set of states that appear in $q_{1}\cdots q_{l}$ is
$S_{u}$. Moreover, for every $l,l^{\prime}\geq m$ if $q_{l}=q_{l^{\prime}}$,
then $q_{1}\cdots q_{l}\equiv_{state}q_{1}\cdots q_{l^{\prime}}$.

###  5.3 Restrictions on strategies of $\mathcal{O}$

[Simple Strategies] A timed $\omega$-string $(a_{0},t_{0})(a_{1},t_{1})\cdots$
is simple timed if $t_{i}=\Delta\times i$ for some $\Delta>0$. An
$\mathcal{O}$’s strategy is _simple_ if it chooses only simple timed
$UP(Q)$-sequences, i.e., the sequences of the form
$(a_{1},0)(a_{1},\Delta)\cdots(a_{i},\Delta\times i)\cdots$, where
$a_{0}a_{1}\cdots\in UP(Q)$.

######  Lemma 24 (Reduction to simple strategies in
$\mathcal{G}_{\mathcal{A}}$).

$\mathcal{O}~{}$has a winning strategy if and only if it has a simple winning
strategy.

######  Proof 5.4.

Let $\sigma$ be a winning strategy for $\mathcal{O}~{}$in
$\mathcal{G}_{\mathcal{A}}$. We are going to construct a simple winning
strategy. First, for a timed $\omega$-sequence
$u:=(a_{0},0)(a_{1},t_{1})\cdots$ let $first(u):=t_{1}$ be its first positive
point and $untimed(u)$ be the corresponding untimed $\omega$-sequence
$a_{0}a_{1}\cdots$.

By $u^{s}$ we denote the simple timed sequence $v$ such that $untimed(u)$ is
equivalent to $untimed(v)\in UP(Q)$ and the scale of $v$ is
$t_{1}:=first(u)/d_{Q}$ where $d_{Q}\geq$ is the length of the lag of
$untimed(v)$.

We are going to show that a strategy $\tau$ which replaces $u$ moves of
$\mathcal{O}~{}$in $\sigma$ by the corresponding $u^{s}$ moves is winning.

Consider a play $\pi$ consistent with $\tau$. We construct a play
$\pi^{\sigma}$ consistent with $\sigma$ such that the states visited
infinitely often are the same and the duration of $\pi^{\sigma}$ $\geq$ the
duration of $\pi$. Hence, if $\pi^{\sigma}$ is winning, then $\pi$ is winning.

For every prefix $\pi_{n}$ of $\pi$ where $\mathcal{O}~{}$moves, we construct
the corresponding prefix $\pi^{\sigma}_{n}$ of $\pi^{\sigma}$ where
$\mathcal{O}~{}$moves and the following invariants hold:

I-last state

$\pi_{n}$ and $\pi^{\sigma}_{n}$ ends in the same states.

I-recurrent states

The infix between $\pi_{n-1}$ and $\pi_{n}$ has the same states as the infix
between $\pi^{\sigma}_{n-1}$ and $\pi^{\sigma}_{n}$. I.e., let $v_{n}$
(respectively, $v^{\sigma}_{n}$) be such that $\pi_{n}=\pi_{n-1}v_{n}$
(respectively, $\pi^{\sigma}_{n}=\pi^{\sigma}_{n-1}v^{\sigma}_{n}$); then a
state occurs in $v_{n}$ if and only if it occurs in $v^{\sigma}_{n}$.

I-duration

The duration of $\pi^{\sigma}_{n}$ $\geq$ the duration of $\pi_{n}$.

Assume that a prefix $\pi_{n}$ was constructed and the corresponding prefix is
$\pi^{\sigma}_{n}$ (they end in the same state). If $\sigma$ prescribes for
$\mathcal{O}~{}$to choose $u$, let $u^{s}$ be the corresponding choose for
$\tau$.

Now, if $\mathcal{I}~{}$accepts $u^{s}$, then we are done; both plays are
accepting or rejecting. If $\mathcal{I}~{}$interrupts at a state $q$, we
consider two cases.

A) $\mathcal{I}~{}$interrupted $u^{s}$ at time $t$ at a position inside a
period. Then, we can find $t^{\prime}>t$ such that $u$ is at the state $q$ at
$t^{\prime}$ and the corresponding prefixes are $\equiv_{state}$-equivalent.
In fact, by Lemma lem:later-choice, there are infinitely many such positions
in $u$. Now, we constructed $\pi^{\sigma}_{n+1}$ prefix with the duration $>$
than the duration of corresponding $\pi_{n+1}$ prefix.

B) $\mathcal{I}~{}$interrupts at time $t$ in a state $q_{1}$ at a position in
the prefix; hence, $t<t_{1}=first(u)$. We choose the corresponding
interruption point in $u$. It is at time $\geq t_{1}$. Hence, the invariants
are preserved.

It remains to show that $\pi$ is winning for $\mathcal{O}~{}$if $\pi^{\sigma}$
is winning for $\mathcal{O}$.

If the plays are finite, then $\pi$ is winning iff $\pi^{\sigma}$ is winning.

If the plays are infinite, then (1) by the recurrent state invariant the same
states appear infinitely often in $\pi$ and in $\pi^{\sigma}$, and (2) if
$\mathcal{I}~{}$causes that time converges in $\pi^{\sigma}$ to
$t^{\sigma}<\infty$, then in $\pi$ time converges to the value $\leq
t^{\sigma}<\infty$. Since $\mathcal{O}~{}$wins $\pi^{\sigma}$, we obtain that
$\mathcal{O}~{}$wins $\pi$.

Now, we will play explicitly on a finite arena. This game corresponds to
$\mathcal{G}_{\mathcal{A}}$-game when $\mathcal{O}~{}$is restricted to use
only simple strategies.

Let $\mathcal{A}:=(Q,\Sigma_{in},\Sigma_{out},\delta,col)$ be an automaton. We
construct the following arena:

Arena for simple strategies games States: $\\{q_{init}\\}\cup
Q\times\Sigma_{in}\cup Q\times\Sigma_{in}\times UP(Q)$, where
$Q_{\mathcal{I}}:=\\{q_{init}\\}\cup Q\times\Sigma_{in}\times UP(Q)$ is the
set of $\mathcal{I}~{}$nodes, and $Q_{\mathcal{O}}:=Q\times\Sigma_{in}$ is the
set of $\mathcal{O}~{}$nodes. The set $F$ of final nodes is $\\{(q,a,u)\mid$
the maximal priority that appears infinitely often in $u$ is even$\\}$. Edges:
1. $q_{init}$ to $(q_{init},a)$ for every $a\in\Sigma_{in}$. 2. $(q_{0},a)$ to
$(q_{0},a,u)$, where $u=(q_{1},q_{2},\dots)\in UP(Q)$ such that $\exists
b_{i}\in\Sigma_{out}.~{}q_{i+1}=\delta(q_{i},(a,b_{i}))$ for all $i$. 3. There
is an edge from $(q,a,u)$ to $(q^{\prime},b)$ for $u\in UP(Q)$, if $a\neq
b\in\Sigma_{in}$ and there is $n$ such that $u(n)=q^{\prime}$; this edge will
be labeled by $p$ \- the maximal priority among $u(1),\dots,u(n)$ and it will
be called small if $u(1),\dots,u(n)$ is in the lag part of $u$; otherwise, it
will be called big.

This arena is a finite graph. There might be parallel edges from $(q,a,u)$ to
$(q^{\prime},b)$ which will have labels $(p,big)$ or $(p,small)$ for a
priority $p$. If $k$ is the number of priorities, then from $(q,a,u)$ to
$(q^{\prime},b)$ for every $p\leq k$ there is at most one edge $(p,small)$;
and by Lemma 23, there is a unique $p^{\prime}$ such that there is an edge
$(p^{\prime},big)$ from $(q,a,u)$ to $(q^{\prime},b)$; moreover, this
$p^{\prime}$ is the maximal of the priorities assigned to the states of $u$.

Now, consider the following game.

Timed game $\mathcal{G}^{arena}_{\mathcal{A}}$ on our finite arena Initial
step. $\mathcal{I}~{}$chooses $a\in\Sigma_{in}$ and the play proceeds to
$(q_{0},a)$; $t_{0}$ is set to 0. From a state $(q,a)$ at $i$-th move at time
$t_{i}$ $\mathcal{O}~{}$chooses an edge to $(q,a,u)$ and a time scale
$\tau_{i}$. It defines a sequence $Y_{i}$ on $[t_{i},\infty)$ as
$Y(t_{i}+\tau_{i}\times n)=q$ if $q$ is the $n$-th state of $u$. From a state
$(q,a,u)$, at $i+1$-move Player $\mathcal{I}~{}$either (A) accepts and the
play ends. It is winning for $\mathcal{O}~{}$iff $(q,a,u)\in F$, or (B)
interrupts at $t_{i+1}>t_{i}$ by chosen $b\neq a$. Then, the play moves to
$(q_{n},b)$ by an edge with priority $p$ if
$t_{i}+\tau_{i}\times(n-1)<t_{i+1}\leq t_{i}+\tau_{i}\times n$ and $p$ is the
maximal of priorities among $q_{1},\cdots,q_{n}$. _Winning Condition._
$\mathcal{O}~{}$wins a play $\pi$ if either $\pi$ is finite and its last state
is in $F$ or $\pi$ is infinite and $\lim t_{i}$ is finite, or the maximal
priority that appears infinitely often is even.

Note that in the above game the arena is finite, yet each player has
uncountable many moves, when he/she chooses time. The following is immediate.

######  Lemma 25.

$\mathcal{O}~{}$wins $\mathcal{G}^{arena}_{\mathcal{A}}$ if and only if
$\mathcal{O}~{}$has a winning simple strategy for
$\mathcal{G}_{\mathcal{A}}$-game.

Next, we are going to restrict further the strategies of
$\mathcal{O}~{}$player in $\mathcal{G}^{arena}_{\mathcal{A}}$.

A strategy is called almost positional, if at every vertex it always chooses
the same untimed move (timed scales might be different).

######  Lemma 26 (Almost positional winning strategy in
$\mathcal{G}^{arena}_{\mathcal{A}}$).

$\mathcal{O}~{}$has a simple winning strategy iff $\mathcal{O}~{}$has an
almost positional simple winning strategy.

######  Proof 5.5.

First, note that $\mathcal{G}^{arena}_{\mathcal{A}}$ game is determinate,
i.e., one of the player has a winning strategy.

Let $\sigma$ be a simple strategy for $\mathcal{O}$. For every vertex $s$ of
$\mathcal{O}$, let $out^{\sigma}_{s}$ be the cardinality of the set of
possible (untimed) moves from $s$ which are consistent with $\sigma$. We
proceed by the induction on $\sum out^{\sigma}_{s}$.

Basis. $\sigma$ is winning and $out^{\sigma}_{s}=1$ for every $s$. Hence,
$\sigma$ is almost positional.

Inductive step. Assume $out^{\sigma}_{s}>1$. Let $u$ be a move from $s$
consistent with $\sigma$. We consider the arena $G_{u}$ where only $u$ moves
(with different scales) are available from $s$ and the game $G_{\neg u}$ where
$u$ moves are forbidden and only the other moves are consistent with $\sigma$
are allowed from $s$.

If $\mathcal{O}~{}$wins in $G_{u}$ or in $G_{\neg u}$ we are done by the
inductive hypothesis. Hence, $\mathcal{I}~{}$wins in these games by strategies
$\tau_{u}$ and $\tau_{\neg u}$. We are going to show that this leads to a
contradiction.

Let $\pi$ be a play (or a prefix of a play) in $G$ from $s$. Partition it into
a play in $G_{u}$ and a play in $G_{\neg u}$. A move $v$ is in $G_{u}$ iff the
last move from $s$ before $v$ is $u$.

Let $View_{u}(\pi)$ (respectively, $View_{\neg u}(\pi)$ be the subplay in
$G_{u}$ (respectively, in $G_{\neg u}$).

Consider a play $\pi$ such that in $View_{u}(\pi)$ (respectively, $View_{\neg
u}(\pi)$) player $\mathcal{I}~{}$plays according to $\tau_{u}$ (respectively,
$\tau_{\neg u}$). Since, these are winning strategies for $\mathcal{I}$, the
duration of this play is unbounded, and the parity is good for Player
$\mathcal{I}$. Hence, $\pi$ is winning for $\mathcal{I}~{}$\- contradiction.

Finally, we restrict/eliminate the time scale that Player
$\mathcal{O}~{}$chooses.

######  Lemma 27 ($2^{-i}$ scale).

$\mathcal{O}~{}$has an almost positional simple winning strategy if and only
if $\mathcal{O}~{}$has an almost positional simple winning strategy when
$i$-th time move has the scale $2^{-i}$.

######  Proof 5.6.

Let $\sigma$ be an almost positional simple winning strategy for
$\mathcal{O}~{}$and $\sigma^{exp}$ be the corresponding almost positional
simple winning strategy for $\mathcal{O}~{}$when $i$-th time move has the
scale $2^{-i}$.

Assume $\pi^{exp}$ is a play consistent with $\sigma^{exp}$ which is winning
for $\mathcal{I}~{}$. We are going to construct $\pi$ consistent with $\sigma$
which is winning for $\mathcal{I}~{}$\- contradiction.

We will keep the following invariant: After $i$-th move of $\mathcal{I}~{}$the
corresponding subplays are in the same state, pass through the same set of
states, and infinitely often the duration of the $\pi$ subplay $>$ the
duration of the $\pi^{exp}$ subplay.

Let $u^{exp}$ be a move of $\mathcal{O}$. Assume $\mathcal{I}~{}$interrupts it
at a state $q$ after $t$ units of time. If $q$ is inside the period, we can
find $q$ which is far enough in the $u$ move and interrupts at the same $q$
with the same past. If $q$ is inside the prefix lag, we pick up the
corresponding $q$ in the prefix of $u$.

It is clear that the first two invariants are preserved. If the duration of
$\pi^{exp}$ is infinite, then there are infinitely many interruptions inside
the periods of $\mathcal{O}~{}$moves. Hence, for each such interruption at
$n$-th move we can choose the corresponding interruption in $u$ that ensures
that the duration of $\pi_{n}$ $>$ than the duration of $\pi^{exp}_{n}$.
Therefore, the third property holds.

To sum up, we proved that if there is a play consistent with $\sigma^{exp}$
which is winning for $\mathcal{I}$, then there is a play consistent with
$\sigma$ which is winning for $\mathcal{I}~{}$\- contradiction to the
assumption that $\sigma$ is a winning strategy for $\mathcal{O}$.

###  5.4 Decidability

We proved that $\mathcal{O}~{}$has a winning strategy iff $\mathcal{O}~{}$has
an almost positional simple winning strategy where $i$-th time move has the
scale $2^{-i}$. There are finitely many such strategies. Hence, to decide
whether $\mathcal{O}~{}$has a winning strategy it is enough to check whether
such a strategy is winning for $\mathcal{O}$.

Let $\sigma$ be an almost positional winning strategy for $\mathcal{O}~{}$with
the times scale $2^{-i}$ on the $i$-th move. It chooses exactly one edge from
every vertex $(q,a)$. Consider the sub-graph $G_{\sigma}$ of our game arena
where from $(q,a)$ only the edge specified by $\sigma$ is chosen (all other
edges from $(q,a)$ are removed). This is an arena for one player
$\mathcal{I}$. Recall that the edges from the nodes of the form $(q,a,u)$ are
labeled. Let $u=q_{1}\cdots q_{n}\cdots$. The edge which corresponds to the
move when $\mathcal{I}~{}$interrupts at $q_{n}$ is labeled by the maximal of
priorities $p$ assigned to the states $q_{1},\cdots,q_{n}$; and it is small
(respectively, big) if $q_{1}\cdots q_{n}$ is inside lag (respectively, period
of $u$) will carry label $(p,big)$ or $(p,small)$ for $p\leq k$. Note big and
small are just names that indicate whether a label appears in the period part
or in the lag part, and they do not affect the order.

######  Lemma 28 (Deciding whether a strategy is winning).

Let $\sigma$ be an almost positional winning strategy for $\mathcal{O}~{}$with
the times scale $2^{-i}$ on the $i$-th move. Player $\mathcal{I}~{}$wins
against $\sigma$ if and only if in $G_{\sigma}$ either (A) there is a
reachable node $(q,a,u)\not\in F$ or (B) there is a reachable cycle $C$ with
at least one edge labeled by a big priority and the maximal priority in $C$ is
odd.

######  Proof 5.7.

It is clear that if (A) holds, then $\mathcal{I}~{}$wins against $\sigma$. She
only needs to reach such a node $(q,a,u)\not\in F$ and then stop playing. If
(B) holds, then $\mathcal{I}~{}$can reach such a cycle $C$ and then move along
its edges. Moreover, when she goes over an edge labeled by a big priority $p$,
she can choose a time $t$ which is at distance at least one from the time when
the corresponding edge to $(q,a,u)$ is taken (by Lemma 23, she can choose time
as big as she wishes). This will ensure that every round along $C$ takes at
least one time unit; therefore, $\lim t_{i}=\infty$. Since the maximal
priority on $C$ is odd, this play is winning for $\mathcal{I}$.

Now, we assume that $\mathcal{I}~{}$wins and show that (A) or (B) holds. If
(A) does not hold, then a winning play for $\mathcal{I}~{}$must be infinite.
We are going to find a cycle as described in (B). If only small priorities
appear infinitely often, then the duration of the play is finite and it cannot
be winning for $\mathcal{I}$. Indeed, assume that after $t_{j}$ only small
priorities appear in the play. Then, $t_{i+1}-t_{i}<m_{Q}\times 2^{-i}$ for
all $i\geq j$. Hence, $\lim t_{i}\leq t_{j}+2m_{Q}<\infty$ and
$\mathcal{I}~{}$loses.

Therefore, there is an edge $e_{b}$ with a big priority that appears
infinitely often. Let $p$ be the maximal priority that appears infinitely
often (it is odd). Then, some edge $e_{p}$ with $p$ appears infinitely often,
and there is a sub-play that starts and ends at $e_{p}$ and passes through
$e_{b}$. This sub-play is a cycle that passes through an edge with a big
priority and the maximal priority of its edges is $p$ and $p$ is odd.

There are only finitely many almost positional strategies for
$\mathcal{O}~{}$with the times scale $2^{-i}$ on the $i$-th move (in
$\mathcal{G}^{arena}_{\mathcal{A}}$), and it is decidable whether such a
strategy is winning, and $\mathcal{O}~{}$wins iff it has such a winning
strategy. Hence, we obtain:

######  Lemma 29.

It is decidable whether $\mathcal{O}~{}$has a wining strategy
$\mathcal{G}^{arena}_{\mathcal{A}}$.

Recall $\mathcal{O}~{}$has a winning strategy in
$\mathcal{G}^{arena}_{\mathcal{A}}$ iff $\mathcal{O}~{}$has a winning strategy
in $\mathcal{G}_{\mathcal{A}}$ iff $\mathcal{O}~{}$has a winning strategy in
$\mathcal{G}_{\Psi}$ iff there is a causal operator that implements $\Psi$.
Therefore, we obtain:

######  Theorem 30 (Decidability of Synthesis for RC Signals).

The Church synthesis problem over RC signals is decidable.

##  6 The Church Synthesis Problem over FV Signals is Decidable

In this section a proof of the decidability of Church’s synthesis problem over
FV signals is outlined. See 6 The proof is very similar to the proof of
Theorem 30, and does not require novel insights or techniques. Here, we
explain what are the differences. We start with a game.

Consider the following two-player game $\mathcal{G}_{\Psi}$. During the play
$\mathcal{I}~{}$constructs a (timed sequenced for) input signal $X$ and
$\mathcal{O}~{}$constructs an output $Y$.

Round 0. Set $t_{0}:=0$.

  1. 1.

$\mathcal{I}~{}$chooses a value $a_{0}\in\Sigma_{in}$ which holds at $t_{0}$.

  2. 2.

$\mathcal{O}~{}$responses with $b_{0}\in\Sigma_{out}$.

  3. 3.

$\mathcal{I}~{}$chooses $a^{d}_{0}\in\Sigma_{in}$ to hold for a while after
$t_{0}$ (here and below the superscript $d$ indicates that this input lasts
for a non-singular interval).

  4. 4.

$\mathcal{O}~{}$responses with a timed $\omega$-sequence (equivalently, with a
signal $Y_{0}$ on $(t_{0},\infty)$).

Now, $\mathcal{I}~{}$has two options:

A) $\mathcal{I}~{}$accepts. In this case, the play ends.
$\mathcal{I}~{}$constructed $X$ which is $a_{0}$ at $t_{0}=0$ and $a^{d}_{0}$
at all $t>0$, and $\mathcal{O}~{}$constructed $Y$ which is $b_{0}$ at $t_{0}$
and $Y_{0}$ \- the signal chosen by $\mathcal{O}~{}$in $(t_{0},\infty)$.

B) $\mathcal{I}~{}$interrupts at some $t_{1}>t_{0}$ by choosing left or right
discontinuity in the input.

Discontinuity from the left

$\mathcal{I}~{}$chooses $a_{1}\neq a^{d}_{0}$ and the game proceeds to step
(1) of round 1, or $\mathcal{I}~{}$sets $a_{1}=a^{d}_{0}$ and

Discontinuity from the right

$a^{d}_{1}\neq a^{d}_{0}$ and the game proceeds to step (3) of round 1.

Round $i+1$.

  1. 1.

$\mathcal{O}~{}$chooses $b_{i+1}\in\Sigma_{out}$ to hold at $t_{i+1}$.

  2. 2.

$\mathcal{I}~{}$chooses $a^{d}_{i+1}$ to hold for a while after $t_{i+1}$.

  3. 3.

$\mathcal{O}~{}$response with a timed $\omega$ sequence $Y^{\prime}_{i+1}$
(equivalently, with a signal on $(t_{i+1},\infty)$).

  4. 4.

Now, $\mathcal{I}~{}$has two options.

A) $\mathcal{I}~{}$accept. In this case the play ends. The signal $X$
constructed by $\mathcal{I}~{}$coincides with $X^{\prime}_{i}$ on
$[0,t_{i+1})$ and equal to $a_{i+1}$ at $t_{i+1}$ and equal to $a^{d}_{i+1}$
in $(t_{i+1},\infty)$. The signal $Y$ constructed by $\mathcal{O}~{}$coincides
with $Y^{\prime}_{i}$ on $[0,t_{i+1})$ equal to $b_{i+1}$ at $t_{i+1}$ and
coincides with $Y^{\prime}_{i+1}$ on $[t_{i+1},\infty)$.

B) $\mathcal{I}~{}$interrupt at some $t_{i+1}>t_{i}$ by choosing:

    1. (a)

$a_{i+1}\neq a^{d}_{i}$ in this case round $i+2$ starts (in this case $X$ is
left discontinuous at $t_{i+1}$) or by

    2. (b)

$a_{i+1}=a^{d}_{i}$ and $a^{d}_{i+1}\neq a^{d}_{i}$. In this case round $i+2$
starts at step (3) by a choice of $\mathcal{O}~{}$(in this case $X$ is right
discontinuous at $t_{i+1}$).

Let $X$ be the signal that corresponds to the timed sequence
$(a_{0},a^{d}_{0},0)(a_{1},a^{d}_{1},t_{1})\dots(a_{i},a^{d}_{i},t_{i})\dots$
constructed by $\mathcal{I}$, and let $Y$ be the signal constructed by
$\mathcal{O}$.

_Winning conditions._ $\mathcal{O}~{}$wins the play iff $\Psi(X,Y)$ holds or
$\mathcal{I}~{}$interrupts infinitely often and the duration of the play
$<\infty$, i.e., $\lim t_{n}<\infty$, where $t_{n}$ is the time of $n$-th
interruption.

Similarly, to Lemma 18, we have

######  Lemma 31 (Reduction to games).

$\mathcal{O}~{}$wins $\mathcal{G}_{\Psi}$ if and only if there is a C-operator
that implements $\Psi$.

Note that in this game $\mathcal{O}~{}$has two types of moves. In step (1) she
chooses a letter in $\Sigma_{out}$ and in Step (3) she chooses a
$\Sigma_{out}$-signal over open interval $(t,\infty)$. Similarly to the proof
of Theorem 30, we are going to restrict $\mathcal{O}~{}$moves in step (3). The
first restriction is a time schedule. When $\mathcal{O}~{}$chooses a timed
sequence (equivalently a signal), we require that the distance between
consecutive time points in this signal should be the same. We call such a
signal _simple timed_. Another restriction is on the sequence of values. We
require that this sequence is ultimately periodic. But first, we consider a
game over an automaton in which $\mathcal{O}~{}$chooses signals over states
instead of signals over $\Sigma_{out}$. She chooses the run which corresponds
to a choice of an input over $\Sigma_{out}$.

Consider the game $G_{\mathcal{A}}$ over a deterministic parity automaton
$\mathcal{A}:=(Q,\Sigma_{in}\times\Sigma_{out},\delta,q_{init},pr)$ equivalent
to $\Psi^{D}$. In this game $\mathcal{O}~{}$will choose signals over $Q$
instead of signals over $\Sigma_{out}$.

Game $G_{\mathcal{A}}$.

Round 0. Set $t_{0}:=0$.

  1. 1.

$\mathcal{I}~{}$chooses a value $a_{0}\in\Sigma_{in}$ which holds at $t_{0}$.

  2. 2.

$\mathcal{O}~{}$responds with $q_{0}:=\delta(q_{init},(a_{0},b_{0}))$ for some
$b_{0}\in\Sigma_{out}$.

  3. 3.

$\mathcal{I}~{}$chooses $a^{d}_{0}\in\Sigma_{in}$ to hold for a while after
$t_{0}$.

  4. 4.

$\mathcal{O}~{}$responses with a signal $Y_{0}$ on $(t_{0},\infty)$ over $Q$
such that $Y_{0}$ is a run of $\mathcal{A}$ (from $q_{0}$) when the signal
over $\Sigma_{in}$ is fixed to be $a^{d}_{0}$.

Now, $\mathcal{I}~{}$has two options.

A) $\mathcal{I}~{}$accepts. In this case, the play ends.
$\mathcal{I}~{}$constructed $X$ which is $a_{0}$ at $t_{0}=0$ and $a^{d}_{0}$
at all $t>0$, and $\mathcal{O}~{}$constructed $Y$ which is $q_{0}$ at $t_{0}$
and is $Y_{0}$ \- the signal chosen by $\mathcal{O}~{}$in $(t_{0},\infty)$.

B) $\mathcal{I}~{}$interrupts at some $t_{1}>t_{0}$ by choosing left or right
discontinuity in the input. Let set $q_{1}$ to be the left limit of $Y_{0}$ at
$t_{1}$.

Discontinuity from the left

$\mathcal{I}~{}$chooses $a_{1}\neq a^{d}_{0}$ and the game proceeds to step
(1) of round 1, or $\mathcal{I}~{}$sets $a_{1}=a^{d}_{0}$ and

Discontinuity from the right

$a^{d}_{1}\neq a^{d}_{0}$ and the game proceeds to step (3) of round 1.

Round $i+1$.

  1. 1.

$\mathcal{O}~{}$chooses $q_{i+1}=\delta(q_{i},(a_{i+1},b_{i+1}))$ for some
$b_{i+1}\in\Sigma_{out}$ to hold at $t_{i+1}$.

  2. 2.

$\mathcal{I}~{}$chooses $a^{d}_{i+1}$ to hold for a while after $t_{i+1}$.

  3. 3.

$\mathcal{O}~{}$responds with a signal $Y_{i+1}$ over $Q$ on
$(t_{i+1},\infty)$) which is a run of $\mathcal{A}$ from $q_{i}$ when the
signal over $\Sigma_{in}$ is fixed to be $a^{d}_{i+1}$.

  4. 4.

Now $\mathcal{I}~{}$has two options.

A) $\mathcal{I}~{}$accept. In this case the play ends. The signal $Y$
constructed by $\mathcal{O}~{}$coincides with $Y_{i}$ on $(t_{l},t_{l+1})$ is
equal to $q_{l+1}$ at $t_{l+1}$ (for $l\leq i$) and coincides with $Y_{i+1}$
on $(t_{i+1},\infty)$.

B) $\mathcal{I}~{}$interrupt at some $t_{i+2}>t_{i+1}$. Set $q_{i+2}$ to be
the left limit of $Y_{0}$ at $t_{i+1}$. $\mathcal{I}~{}$chooses

    1. (a)

$a_{i+2}\neq a^{d}_{i+1}$ in this case round $i+2$ starts (in this case $X$ is
left discontinuous at $t_{i+1}$) or by

    2. (b)

$a_{i+2}=a^{d}_{i+1}$ and $a^{d}_{i+2}\neq a^{d}_{i+1}$. In this case round
$i+2$ starts at step (3) by a choice of $\mathcal{O}~{}$(in this case $X$ is
right discontinuous at $t_{i+1}$).

_Winning conditions._ $\mathcal{O}~{}$wins if either the sequence of states
produced by $\mathcal{O}~{}$is accepted by $\mathcal{A}$, or there were
infinitely many moves, but $\lim t_{i}$ is finite.

######  Lemma 32 ($\mathcal{G}_{\psi}$ and $\mathcal{G}_{\mathcal{A}}$ are
equivalent).

$\mathcal{O}~{}$wins in $\mathcal{G}_{\Psi}$ if and only if
$\mathcal{O}~{}$wins in $\mathcal{G}_{\mathcal{A}}$.

Exactly like in Subsection 5.2 we define $\equiv_{state}$-equivalence over
finite strings and an equivalence over $\omega$-strings. We define a finite
set of ultimately periodic $\omega$-string $UP(Q)$ and say that a move
$(q_{0},t_{0})(q_{1}.t_{1})\dots(q_{i},t_{i})\dots$ is simple if
$q_{0}q_{1}\dots q_{i}\dots\in UP(Q)$ and $t_{i+1}=t_{i}+\Delta$ for some
$\Delta$. A strategy is simple if it uses only simple moves. We have

######  Lemma 33 (Reduction to simple strategies).

$\mathcal{O}~{}$has a winning strategy if and only if it has a simple winning
strategy.

Now, we will play explicitly on a finite (node) arena. This game corresponds
to the game when $\mathcal{O}~{}$is restricted to use only simple strategies.

Let $\mathcal{A}:=(Q,\Sigma_{in}\times\Sigma_{out},\delta,pr)$ be an
automaton. We construct the following arena:

Arena for simple strategies games States: $\\{q_{init}\\}\cup
Q\times\Sigma_{in}\cup Q\times\\{{\dagger}\\}\cup
Q\times\\{{\dagger}\\}\times\Sigma_{in}\cup Q\times\Sigma_{in}\times UP(Q)$,
where $Q_{\mathcal{I}}:=\\{q_{init}\\}\cup
Q\times\\{{\dagger}\\}\times\Sigma_{in}\cup Q\times\Sigma_{in}\times UP(Q)$ is
the set of $\mathcal{I}~{}$nodes, and the rest is the set of
$\mathcal{O}~{}$nodes. The set $F$ of final nodes is $\\{(q,{\dagger},u)\mid$
the maximal priority that appears infinitely often in $u$ is even$\\}$. Edges:
1. $q_{init}$ to $(q_{init},a)$ for every $a\in\Sigma_{in}$. 2. $(q,a)$ to
$(q^{\prime},{\dagger})$ if $q^{\prime}=\delta(q,(a,b))$ for some
$b\in\Sigma_{out}$. 3. $(q,{\dagger})$ to $(q,{\dagger},a)$ for every
$a\in\Sigma_{in}$ (here $\mathcal{I}~{}$chooses $a$ to hold for a while). 4.
$(q_{0},{\dagger},a)$ to $(q_{0},a,u)$, where $u=(q_{1},q_{2},\dots)\in UP(Q)$
such that $\exists b_{i}\in\Sigma_{out}.~{}q_{i+1}=\delta(q_{i},(a,b_{i}))$
for all $i$. 5. There is an edge from $(q,a,u)$ to $(q^{\prime},b)$ for $u\in
UP(Q)$, if $b\neq a$ and $q^{\prime}=u(n)$ for $n=2m+1$ (this corresponds to
discontinuity from the left). 6. There is an edge from $(q,a,u)$ to
$(q^{\prime}{\dagger},,b)$ for $u\in UP(Q)$, if $b\neq a$ and
$q^{\prime}=u(n)$ for $n=2m$ (this corresponds to discontinuity from the
right). In (5) and (6) the edge will be labeled by $p$ \- the maximal priority
among $u(1),\dots,u(n)$ and it will be called small if $u(1),\dots,u(n)$ is in
the lag part of $u$; otherwise, it will be called big.

Now, consider the following game.

Timed game $\mathcal{G}^{arena}_{\mathcal{A}}$ on our finite arena Initial
step. $\mathcal{I}~{}$chooses $a\in\Sigma_{in}$ and the play proceeds to
$(q_{init},a)$; $t_{0}$ is set to 0. When the play is at node $(q,a)$,
$\mathcal{O}~{}$chooses an edge to $(q^{\prime},{\dagger})$ and the play is
now at $(q^{\prime},{\dagger})$. From $(q,{\dagger})$, $\mathcal{I}~{}$can
move to $(q,{\dagger},a)$. From a state $(q,{\dagger},a)$,
$\mathcal{O}~{}$chooses an edge to $(q^{\prime},a,u)$ and a time scale
$\tau_{i}$. It defines a signal $Y_{i}$ on $(t_{i},\infty)$ as
$Y(t_{i}+\tau_{i}\times n)=u(2n)$ and $Y_{i}(t)=u(2n+1)$ if
$t\in(t_{i}+\tau_{i}\times n,t_{i}+\tau_{i}\times(n+1))$. From a state
$(q,a,u)$ at $i+1$-move Player $\mathcal{I}~{}$either (A) accepts and the play
ends. It is winning for $\mathcal{O}~{}$iff $(q,a,u)\in F$, or (B) interrupts
at $t_{i+1}>t_{i}$ by choosing $b\neq a$ and the left or the right
discontinuity at $t_{i}$. Let $q$ be the left limit of $Y_{i}$ at $t_{i+1}$.
If the left discontinuity is chosen, then the play moves to $(q,b)$. If the
right discontinuity is chosen, the play moves to $(q,{\dagger},b)$. _Winning
Condition._ $\mathcal{O}~{}$wins a play $\pi$ if either $\pi$ is finite and
its last state is in $F$ or $\pi$ is infinite and $\lim t_{i}$ is finite, or
the maximal priority that appears infinitely often at the edges or the nodes
of the play is even.

######  Lemma 34.

$\mathcal{O}~{}$wins $\mathcal{G}^{arena}_{\mathcal{A}}$ if and only if
$\mathcal{O}~{}$has a winning simple strategy for
$\mathcal{G}_{\mathcal{A}}$-game.

Next, like in the proof of Theorem 30, we are going to restrict further the
strategies of $\mathcal{O}~{}$in $\mathcal{G}^{arena}_{\mathcal{A}}$.

A strategy is called almost positional, if at every node it always chooses the
same untimed move (timed scales might be different).

######  Lemma 35 (Almost positional winning strategy in
$\mathcal{G}^{arena}_{\mathcal{A}}$).

$\mathcal{O}~{}$has a simple winning strategy if and only if
$\mathcal{O}~{}$has an almost positional simple winning strategy.

Finally, we restrict the time scale that Player $\mathcal{O}~{}$chooses. We
say that a strategy of $\mathcal{O}~{}$is well-scaled if the $i$-th time move
from a state of the form $(q,{\dagger},a)$ has the scale $2^{-i}$.

######  Lemma 36 ($2^{-i}$ scale).

$\mathcal{O}~{}$has an almost positional simple winning strategy if and only
if $\mathcal{O}~{}$has an well-scaled almost positional simple winning
strategy.

######  Lemma 37 (Deciding whether a well-scaled strategy is winning).

Let $\sigma$ be a well-scaled almost positional winning strategy for
$\mathcal{O}$. It is decidable whether $\sigma$ is winning.

Since there are only finitely many well-scaled almost positional winning
strategies, we obtain that

######  Lemma 38.

It is decidable whether $\mathcal{O}~{}$has a winning strategy in timed game
on $\mathcal{G}^{arena}_{\mathcal{A}}$.

Finally, Theorem 6 follows from Lemmas 31-34 and Lemma 38.

##  7 Conclusion

We investigate a generalization of the Church synthesis problem to the
continuous time of the non-negative reals. We show that in continuous time
there are phenomena which are very different from the canonical discrete time
domain of natural numbers. We proved the decidability the Church synthesis
problem when the specifications are given by $\mathit{MSO[<]}$ formulas.

One can consider a specification language stronger than $\mathit{MSO[<]}$. For
example, let ${\mathcal{M}}:=\langle\mathcal{R}^{\geq
0},SIG,<_{R},P_{1},\dots,P_{k}\rangle$ be an extension of $Sig$ structure by
unary predicates $P_{1},\dots,P_{k}$. If $MSO[<,P_{1},\dots,P_{k}]$ decidable,
then the Church synthesis problem for specifiactions given by
$MSO[<,P_{1},\dots,P_{k}]$ formulas is decidable.

The extension of $\mathit{MSO[<]}$ by $+1$ function is undecidable. Hence, the
the Church synthesis problem for $MSO[<,+1]$ is undeciable. There are
decidable fragments of $MSO[<,+1]$ which use metric constraints in a more
restricted form. The most widespread such decidable metric language is Metric
Interval Temporal Logic (MITL) [AFH96]. We do not know whether the Church
problem is decidable for MITL specifications.

The satisfiability problem for $\mathit{MSO[<]}$ is non-elementary. The
complexity of our algorithm for the Church synthesi problem is non-elementary.
There are two reasons for non-elementary complexity of our algorithm. The
first is that the translation form $\mathit{MSO[<]}$ to an equivalent parity
automaton is non-elementary. The second is that $\mathcal{O}~{}$chooses her
moves from $UP(Q)$ and the size of $UP(Q)$ is non-elementary (even in the size
of $Q$).

Fattal considered specifications (of signal languages) given by deterministic
parity automata [Fat23]. He reduced the Church problem to games in which
$\mathcal{O}~{}$chooses on her move only one letter from $\Sigma_{out}$ and
its duration. He provided an NP upper bound for the synthesis problem when the
specifications are provided by deterministic parity automata. For
specifications given by deterministic Büchi automata he provided a polynomial
algorithm. Unfortunately, even for specifications given by deterministic
automata of parity 3 we do not know whether there exists a polynomial
algorithm (in the discrete case for every fixed bound $p$ on the priorities of
a parity automaton, there s a polynomial algorithm).

##  Appendix A Proof of Lemma 20(3)

A coloring of $\omega$ is a function $f$ from the set of unordered pairs of
distinct elements of $\omega$ into a finite set $T$ of colors. For $x<y$, we
will write $f(x,y)$ instead of $f(\\{x,y\\})$. The coloring $f$ is additive if
$f(x,y)=f(x^{\prime},y^{\prime})$ and $f(y,z)=f(y^{\prime},z^{\prime})$ imply
that $f(x,z)=f(x^{\prime},z^{\prime})$. In this case a partial function $+$ is
defined on $T$ such that if $x<y<z$, then $f(x,y)+f(y,z)=f(x,z)$. A set $J$ is
$t$-homogeneous (for $f$ and the color $t$) if $f(x,y)=t$ for every $x<y\in
J$.

Ramsey’s theorem for additive coloring [She75] states:

######  Theorem 39.

If $f$ is an additive coloring of $\omega$, then there is $t\in T$ and an
infinite $t$-homogeneous subset $J$ of $\omega$. Moreover, there is $t_{0}\in
T$ such that $f(0,j)=t_{0}$ for every $j\in J$.

Now, we are ready to prove Lemma 20(3).

Let the set of colors be the set of $\equiv_{state}$-equivalence classes.
Given $\pi$. Define coloring $f$ as $f(i,j):=$ the equivalence class of the
substring of $\pi$ on the interval $[i,j)$. By Lemma 20(2), this is an
additive coloring. Let $J=\\{j_{0}<j_{1}<\cdots\\}$ be an infinite homogeneous
subset of color $v$ (such a set exists by Theorem 39).

Define $u_{0}$ to be the substring of $\pi$ over $[0,j_{0})$, and $u_{j}$ to
be the substring of $\pi$ over $[u_{j},u_{j+1})$ for $j>0$. Let $v_{0}$ be the
equivalence class of $u_{0}$.

By Theorem 39 we obtain $u_{i}$ and $u_{i}u_{i+1}$ and $u_{j}$ are all in the
$v$-equivalence class for all $i,j>0$, and $u_{0}\equiv_{state}u_{0}u_{1}$ are
both in $v_{0}$ equivalence class. Therefore,
$u_{i}\equiv_{state}u_{j}\equiv_{state}u_{i}u_{i+1}$ for all $i,j>0$ and
$u_{0}\equiv_{state}u_{0}u_{1}$. x

## Acknowledgement

Supported in part by Len Blavatnik and the Blavatnik Family foundation.

## References

  * [AD94] Rajeev Alur and David L. Dill.  A theory of timed automata.  Theoretical Computer Science, 126(2):183–235, 1994.
  * [AFH96] R. Alur, T. Feder, and T. A. Henzinger.  The benefits of relaxing punctuality.  J. ACM, 43(1):116-–146, 1996.
  * [BL69] J. Richard Buchi and Lawrence H. Landweber.  Solving sequential conditions by finite-state strategies.  Transactions of the American Mathematical Society, 138:295–311, 1969.
  * [Bu62] J. Richard Buchi.  On a decision method in restricted second order arithmetic. In E. Nagel, P. Suppes, and A. Tarski (Eds.), Logic, methodology and philosophy of science. Stanford: Stanford University Press, 1–11, 1962.
  * [CHP11] Krishnendu Chatterjee, Thomas Henzinger, and Vinayak Prabhu.  Timed parity games: Complexity and robustness.  Logical Methods in Computer Science, 7, 12 2011.
  * [FLTM02] M. Faella, S. La Torre, and A. Murano.  Dense real-time games.  In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pages 167–176, 2002.
  * [Fat23] Daniel Fattal.  Selection and uniformization over continuous time.  Master’s thesis, Tel-Aviv university, 1923.
  * [JORW11] Mark Jenkins, Joël Ouaknine, Alexander Rabinovich, and James Worrell.  The church synthesis problem with metric.  In Marc Bezem, editor, Computer Science Logic, 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011, September 12-15, 2011, Bergen, Norway, Proceedings, volume 12 of LIPIcs, pages 307–321. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011.
  * [Rab02] A. Rabinovich.  Finite variability interpretation of monadic logic of order.  Theoretic]al Computer Science, 275:111–125, 2002.
  * [She75] S. Shelah.  The monadic theory of order.  The Annals of Mathematics, 102(3):379–419, 1975.
  * [TB73] B. Trakhtenbrot and Y. M. Barzdin.  Finite automate: behaviour and synthesis.  1973\.
  * [Tra95] B. Trakhtenbrot.  Origins and metamorphoses of the trinity: logic, nets, automata.  In Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science, pages 506–507, 1995.