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

18.4.1.1 Observations

All the computations above involve only those types that are in the “normal”
flow for finite automata (in terms of computing the transition relations). These
computations have been implemented efficiently in a special version of BALM. The
final accepting set

C

is derived as a side computation as discussed above. In the
special case when the fixed part is given as a logic network, the computations

of the transition structures can be done using the partitioned method discussed in
Chap. 7.
Thus, in this section, nothing special has been done that is associated with
computing with Buchi automata, except for the side computations of determining
the acceptance states. Even the determinization st ep when deciding which of the
subset states are to be put in the Buchi final set,

F

C

, is a typical operation in which
each subset state is classified as soon as it is generated. The only difference in the
transition structures for the Buchi case will come when the interpretation of

C

,i.e.

C

what it means for to be the accepting set, is used to construct FSM solutions. This

is discu ss ed in the next section, where special non-regular methods are formulated
to trim

P C

. Thus, all the
efficient implementations done in BALM for computing with finite automata can be
used.
Another observation is that for specifications, which are co-looping automata,
it is kn own that the pseudo-determinization step in this section is exact, i.e., P D
P # . u ; v / . This follows from the fact that looping automata can be determinized by the
subset construction [80]. Hence for this case, we obtain the most general solution
automaton.

to obtain FSM solutions to meet the co-Buchi condition

18.4.2 Applying the co-B uchi Conditions to Obtain Particular

FSM Solutions

To obtain particular FSM implementations for the unknown component, we first
need to determinize the most general solution, and then to eliminate all loops that
contain a non-accepting state. Moreover, input-progressiveness must be enforced.
To eliminate all such loops, we will generate all sub-graphs, of the state transition
graph of the solution

just found, such that any loop that contains a non-stable state
will be eliminated, leaving only acyclic paths from the initial state to

X

C

.Themost
difficult part is to do this while maintaining input-progressiveness of the solutions. 6
We emphasize that, in general, some solutions will be lost, since only sub-graphs are

6 Algorithms for finding minimum feedback-arc sets in directed graphs exist [33], but do not deal
with input-progressiveness.