Hardware Reference
In-Depth Information
Eventually, we eliminate a node in the loop whose incoming edge on the loop is
non-essential. Thus this loop could have been broken by simply eliminating that
non-essential edge initially.
18.4.4
Complementing B uchi Automata
After the construction of the product of two Buchi automata and the hiding of some
variables (
P # . u ; v / is obtained. The last step to find
the most general automaton solution would be to complement this. Although there
has been much progress in complementing ND Buchi automata (see [42] for a good
review and the most recent construction), a tight lower bound on the number of states
in this is
i
and
o
)anNDBuchi automaton
2 O.nlog n/ where
n
is the number of states in the original Buchi automaton.
.1:06n/ n (see again [42]). A subset construction cannot be used
for determinizing co-Buchi (Buchi) automata. However, for co-looping (looping)
automata, it can be used. A subset construction is upper bounded by
An upper bound is
2 n in the number
of states. Thus the procedure in this section is much less expensive in complexity.
In addition, experience with the subset construction on a number of practical
problems, shows that its behavior is surprisingly well-behaved, in some cases even
resulting in a reduced number of states. However, the price paid is that only a subset
of the most general solution is obtained (unless of course the original specification
is co-looping).
18.4.5
Solving for B uchi Specifications
Buchi specifications provide an effective way for specifying liveness properties,
e.g., always eventually something good happens. The overall flow for using Buchi
specifications might seem to be similar to that already discussed for co-Buchi
specifications, just by interchanging the words “Buchi” and “co-Buchi”. However,
in synthesizing for co-Buchi, we had to determinize a Buchi product (Step 5) and
thus for synthesizing for Buchi, we would have to determinize a co-Buchi product.
However, the subset construction for co-Buchi produces a smaller language and so
the procedure is not sound (since its complement produces a larger language).
If the specification is a looping automaton, then the basic procedure is correct.
However this restriction to safety properties is not satisfactory, since the reason for
considering Buchi was its ability to express liveness.
For a general deterministic Buchi specification,
, a sound approach would be
to compute its complement using the procedure in [80]. This produces a Buchi
complement, so the product and the rest of the operations are now the same as
they would be if we had started out with a co-Buchi specification. In addition to this
complementation procedure being linear, by adding to the description of the fixed
part
S
F
, often the specification
S
can be a simple monitor and described with only a
Search WWH ::




Custom Search