Hardware Reference
In-Depth Information
to that described in Chap. 2 for regular (finite-word) automata. We use a subset
construction to obtain a deterministic Buchi over-approximation of an ND Buchi
automaton. Therefore, the final complementation, done by simply complementing
the acceptance conditions to obtain a co-Buchi automaton, yields a subset 2
of the
most general solution automaton.
Up to the last step, our solution flow does not involve using the co-Buchi
acceptance condition for constructing the transition relations on the automata
structures; it merely keeps track of the acceptance conditions of the final result and
uses this to trim the final transition structure. To do this, a SAT instance [37, 42, 92]
is formulated, each of whose solutions corresponds to a particular FSM solution.
The SAT instance contains clauses that ensure the input-progressiveness property
required for FSMs. Other clauses enforce the co-Buchi condition by requiring
the elimination of all simple cycles that contain a non-accepting state. The SAT
instance represents all FSM solutions that can be associated with sub-graphs of the
automaton solution; solutions with non-simple cycles are not represented, but we
argue that such solutions are impractical anyway. In addition, we only focus on sub-
graphs and do not consider the possibility of splitting states and then looking for
a sub-graph as is done in Chap. 2 to find the largest compositionally progressive
solution.
To simplify the SAT instance, a graph pre-processing step derives a partial order
based on input-progressiveness. In this, an edge is classified as essential if its
removal causes a state to become non-progressive. This concept is used to simplify
the graph (see Sect. 18.4.3 , which then is used to obtain a simpler SAT formulation.
The algorithm was implemented in a special version of BALM and we discuss some
results on a few simple examples. On larger problems, we found that the bottleneck
was the enumeration of all simple cycles required for the SAT instance. It remains a
challenge to make this more efficient in order to apply these ideas to larger problems.
This procedure provides a synthesis flow for co-Buchi specifications that follows
the flow for finite automata; hence it is simpler than for general
-automata and can
make use of recent efficient algorithms for regular automata as described in Chap. 2.
Only in a final step, which extracts an FSM implementation using a SAT formula-
tion, does the flow differ substantially from that for finite automata specifications.
It turns out that this same procedure can be used for Buchi specifications, except
that at the beginning we need to complement the Buchi specification
!
S
into a (ND)
Buchi automaton which can be done linearly by an algorithm in [81].
This chapter is structured with some preliminaries given in Sect. 18.2 ,andthe
problem statement presented in Sect. 18.3 . The proposed
-property synthesis tech-
niques are addressed in Sect. 18.4 , including the SAT formulation. In Sect. 18.4.4
we discuss the complexity of complementing non-deterministic Buchi automata in
!
2 An important subclass of co-B uchi automata is the one of “co-looping” automata. For this class
of specifications, our procedure is exact and thus obtains the most general solution automaton.
Search WWH ::




Custom Search