Hardware Reference
In-Depth Information
we trim. Note that what is left is either empty or has one or more accepting loops.
This is so because it has a finite number of states and it is input-progressive (there
is always a next state). We obtain the final FSM by just selecting one that steers to
one of the accepting loops.
For B uchi conditions we cannot insist that the largest solution is prefix-closed
even though we want to finally get an FSM from it. To get an FSM solution for
Buchi conditions, we have to give up initially on the largest solution automaton
to be prefix-closed and just get the largest solution. Afterwards, to find an FSM
solution is a different problem that in general we did not address in this chapter
except for the co-Buchi case where we can use some special properties.
Discuss how to find an FSM solution when synthesizing for Buchi properties.
Search WWH ::
Custom Search