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

general with respect to the construction in this chapter; moreover, in Sect. 18.4.5
we mention a minor modification that can be used for synthesizing to Buchi
specifications. Sect. 18.5 concludes.

18.2 B uchi and co-B uchi Automata

An -automaton is a finite state automaton that accepts infinite strings [53, 122].

For the purposes of this chapter, we only need to discuss Buchi, co-Buchi, looping,
and co-looping automata.
Both Buchi and co-Buchi automata have a designated subset of states (called
the stable set or acceptance condition or final set), which define their acceptance
condition. In the Buchi case the meaning is that an accepting run should visit the
stable set infinitely often, while in the co-Buchi case an accepting run eventually
should enter the stable region and stay there forever. For an ND automaton with
acceptance condition Acc , an input sequence is accepted (is in the language of the
automaton) if there exists an accepting run under that input sequence.
A co-looping automaton is a co-Buchi automaton with the additional restriction
that the set of final states must be a sink, i.e. there is no edge from any final state
to a non-final state. A looping automaton is the dual of a co-looping automaton; its
non-final states are a sink. Thus an accepting run for a looping automaton is one that
always avoids a non-final state. Looping automata are useful for expressing safety
properties. Looping and co-looping automata have the property that they can be
determinized by the subset construction [80], which is simpler than for the general
case.
Thus, the difference between co-looping and co-Buchi is that the latter can
have a final set from which it is possible to exit. However, it seems possible that
in many cases with a general co-Buchi specification, the synthesis problem can
be divided into two phases, the problem of steering the state of the system into
a state of the final set (a co-looping problem), and the problem of keeping it
there (a looping problem). These might be solved separately. We will see that the
procedure described in this chapter, when used for finding the most general solution
with a co-looping specification, is exact, while for the general co-Buchi case, it is a
conservative approximation.

!

18.3 Problem Statement

The synthesis problems considered in this chapter have the topology shown in
Fig. 18.1 , 3 however, we investigate the situation where S is a co-Buchi automaton.

3 The particular topology of communication is not important. Our results can be adapted easily to
other topologies.