Sequential Synthesis with Co-Büchi Specifications

Computations are developed for the synthesis of a finite state machine (FSM) embedded in a known FSM such that their combined behavior satisfies a co-Büchi specification (the solution must finally enter an acceptable set of states and stay there forever). The procedures for this are shown to be very similar to those used for regular (non-omega) automata, except for a final step in which a set of FSM solutions is represented as a SAT instance of which each satisfying assignment corresponds to an FSM solution. The computations have been implemented and we discuss some results.