# Generalized sequential machine synthesis subject to language equivalence/inclusion and reachability

A generalized sequential machine (GSM) is a generalization of a Mealy machine where on each transition one input symbol is read and 0 or more output symbols are written. As in a Mealy machine, we assume that there are no final states, i.e. a GSM operates on infinite input/output words. A GSM has finitely many states.

Assume $A$ and $B$ are two single-valued GSMs and $C$ is a not necessarily single-valued GSM. Single-valued means that for each infinite input word there is at most one infinite output word (determinism is a sufficient but not necessary condition for single-valuedness). Suppose in addition that $A$ and $C$ are fully reachable, i.e. there is a path from the start state to every other state. In the following, two GSM synthesis problems are described. Let $T_X$ denote the set of states of GSM $X$.

1. Are there single-valued GSMs $X$ and $Y$ such that $X \circ A \equiv Y \circ B$ and in $X \circ A$ for every $t \in T_A$ there is a state $(\_, t) \in T_X \times T_A$ reachable from the start state, i.e. $A$ remains fully reachable in $X \circ A$? Note that $\circ$ denotes transducer composition.
2. Are there single-valued, finite state transducers $X$ and $Y$ such that $X \circ C \supseteq Y \circ B$ and in $X \circ C$ for every $t \in T_C$ there is a state $(\_, t) \in T_X \times T_C$ reachable from the start state, i.e. $C$ remains fully reachable in $X \circ C$?

Clearly, 1. is semi-decidable and 2. is undecidable if $C$ is non-deterministic (without restriction, i.e. infinitely-valued). However, is 1. decidable and if so what is the complexity? For it to be decidable it must be possible to bound the number of states of $X$ and $Y$. Moreover, is 2. decidable if $C$ is finitely-valued, i.e. there is a bounded number of infinite output words for each infinite input word? I'm particularly interested in symbolic methods, also references to practical bounded synthesis approaches. I appreciate any hints that relate this problem to a standard problem as well. Thanks for your input.

• idea, can this be simplified/converted to a problem where all the input/output alphabets are the same? – vzn Jan 2 '14 at 19:31
• @vzn: Good point. I don't see a problem when we assume that all $\Sigma_\_$ and $\Gamma_\_$ are equal. I just added the details to provide an intuition of $X$ and $Y$. Moreover, in 1. we can replace $B \circ C$ by some single-valued finite state transducer $D$. – Dave Lang Jan 2 '14 at 23:00
• re ref to infinite words, are these actually something like buchi transducers? – vzn Jan 3 '14 at 3:38
• @vzn: Thanks for your question. I extended my post. The transducer considered here has no final states. The automaton transduces (input, output) words $(u, v) \in (\Sigma^\star \cup \Sigma^\omega) \times (\Gamma^\star \cup \Gamma^\omega)$, i.e. both finite and infinite words (due to $\epsilon$ transitions). However, it's also fine to assume a generalized sequential machine without final states instead (must consume an input symbol on each transition). – Dave Lang Jan 3 '14 at 12:35
• An input/output word $(u, v)$ is transduced if there is a corresponding path in the transducer. There are no acceptance conditions as in Büchi or Muller automata. – Dave Lang Jan 3 '14 at 12:45