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$.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.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.
Generalized sequential machine synthesis subject to language equivalence/inclusion and reachability
cc.complexity theory;ds.algorithms;lo.logic;automata theory;sat