Extending BALM to Synchronous Equations Over co-B¨uchi Specifications - The Unknown Component Problem: Theory and Applications - page 276

Being a sub-graph of a general solution automaton with the required properties, it
is a solution of the synthesis problem. Hence, all its deterministic sub-machines are
solutions. In [138] it is proved that any solution of the above SAT instance is an
FSM solution of the

-language synthesis problem.
A SAT solver can be configured to enumerate all possible satisfying assignments.
Hence, the formulated SAT instance represents a set of FSM solutions. However,
all FSM solutions may not be represented, e.g., those where a non-simple loop is
traversed a finite number of times before it is exited. An associated FSM would
require enough extra states to count effectively the number of times it has gone
around a particular loop. In this sense, such solutions might not be of interest from
a practical point of view. On the other hand, it is possible that our SAT instance is
not satisfiable, but still there may exist an FSM solution. Possibly this gap might be
remedied by first duplicating one or more states and then formulating a new SAT
instance which is satisfiable. Finally, as noted previously, the subset determinization,
Step 5, may cause some FSM solutions to be lost.

!

18.4.3 Preprocessing to Simplify the SAT Instance

To reduce the size of the SAT inst an ce, a preprocessing step, which trims away
some of the states and transitions of

P

can be done. In some cases, after this step, it
is possible that no SAT solving would be needed.

18.4.3.1 Trimming the Acceptance Set

P C

. We create an acceptance automa-
ton as follows. A nomi nal initial state is created where its outgoing transitions are
all the transitions from

is a co-Buchi automaton with accepting set

C C

to , (the labels on these edges are irrelevant); the n all

C C C

states of the automaton have

been eliminated. This automaton is processed in the regular way, which trims away
some states and transitions in

are eliminated. Thus all transitions from to

C

,tomakeit u -progressive. If the result is empty, then
there can be no cycles ent ire ly contained in

C

and we stop.

P C

Otherwise, we modify by merging all remaining nodes of into a sink node

f , having a single outgoing edge being a universal self-loop. Incoming edges to f

C

are only those which lead to the remaining nodes of ; other edges are re mo ved. We

P

obtain a so-called path (co-looping) automaton X path , derived thus from ,which

has only one nominal stable state f with a universal self-loop.