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

fe w states. After this, the flow is the same as described for the co-Buchi case, sin ce
S is obtained as a Buchi automaton using the procedure of [80], and therefore P

will be a co-Buchi automaton.

18.5 Conclusions

In general, the computational flow to synthesize an FSM according to co-Buchi or
Buchi specifications method is sound but incomplete since we chose to complement
a deterministic over-approximation of a ND Buchi automaton in the inner loop,
instead of complementing the ND Buchi itself, which is a reduction of the most
general FSM, and so may exclude some solutions. The computational steps are the
same as those used in regular finite-word automata synthesis, except for the last step,
which derives a particular solution by formulating and solving a corresponding SAT
problem.
The case considered was for a deterministic specification. If it is non-
deterministic, it seems expeditious to complement it using the algorithms for
complementation mentioned in Sect. 18.4.4 . Although these are super-exponential
in complexity, the number of states in the specification usually can be kept small by
embedding the details of

. Synthesizing for Buchi specifications
is only a minor modification of the procedure presented, because most of the details
of

S in the fixed part F

small and easily complemented.
The above presented synthesis approach has interesting applications in the
controller synthesis area. Control strategies for some case studies (see the problems
at the end of the chapter) were synthesized with a specialized version of BALM for
Buchi/co-Buchi specifications.
The practicality of this approach rests on the ability to enumerate bad cycles. In
experiments we have seen that this is a bottleneck and more research needs to be
done to do this efficiently.

S can be embedded in F ,making S

Acknowledgments This chapter grew out of a research project report by Guo Qiang Gerald
Wang at UC Berkeley. Thanks to Orna Kupferman for extensive readings of a previous draft and
suggesting the application to looping automata, and to Moshe Vardi for very useful comments.

Problems

18.1. Wolf-Goat-Cabbage
Solve the Wolf-Goat-Cabbage problem by the steps of the procedure outlined in
this chapter. Notice that there are no inputs in this example. For an introduction

to the Wolf-Goat-Cabbage game, see Problem 17.2. Here we would like to find all

i