Latticed-LTL Synthesis in the Presence of Noisy Inputs
======================================================

In the classical synthesis problem, we are given a linear temporal
logic (LTL) formula $\psi$ over sets of input and output signals, and
we synthesize a finite-state transducer that realizes $\psi$: with
every sequence of input signals, the transducer associates a sequence
of output signals so that the generated computation satisfies
$\psi$. In recent years, researchers consider extensions of the
classical Boolean setting to a multi-valued one. We study a setting in
which the truth values of the input and output signals are taken from
a finite lattice, and the specification formalism is Latticed-LTL
(LLTL), where conjunctions and disjunctions correspond to the meet and
join operators of the lattice, respectively. The lattice setting
arises in practice, for example in specifications involving priorities
or in systems with inconsistent viewpoints.

We solve the LLTL synthesis problem, where the goal is to synthesize a
transducer that realizes $\psi$ in desired truth values.

For the classical synthesis problem, researchers have studied a
setting with incomplete information, where the truth values of some of
the input signals are hidden and the transducer should nevertheless
realize $\psi$. For the multi-valued setting, we introduce and study a
new type of incomplete information, where the truth values of some of
the input signals may be noisy, and the transducer should still
realize $\psi$ in a desired value. We study the problem of noisy LLTL
synthesis, as well as the theoretical aspects of the setting, like the
amount of noise a transducer may tolerate, or the effect of perturbing
input signals on the satisfaction value of a specification.