Hardware Reference
In-Depth Information
3. Produc
tO
mega(
P
D
F S
); (Compute the product
P
of the two Buchi automata
).
4. Hide variables in
F
and
S
P
invisible to
X
,i.e.hide
i
and
o
.
5. Pseudo-determinizeOmega(
P
); (determinize the Buchi automaton
P
).
6. ComplementOmega(
P
); (dualize the acceptance conditions to produce a co-
Buchi automaton).
7. Restrict to FSM solutions; (final processing to produce FSM sub-solutions).
The first six steps compute a general automaton solution while the last step
constrains it to only FSM solutions. The general flow has been modified to avoid
complementing (possibly non-deterministic) Buchi automata (
), as discussed
below.
4
The term “Omega” has been added to emphasize these modifications.
P
18.4.1
Computing a General Automaton Solution
We summarize the modifications of the first six steps and argue that they can be
done in the same way as for regular finite-word automata, but with only slight
modifications to keep track of the Buchi type acceptance conditions. All transition
relations of intervening automata computed will be the same as for the unmodified
case, and thus can be done by the methods discussed in Chap. 7. The co-Buchi/Buchi
acceptance conditions are simply inferred by analyzing the computations leading up
to Step 7, which then applies the acceptance condition to extract a set of particular
FSM solutions.
1.
Complementing the Specification
S
.
S
is a deterministic co-Buchi automaton
with final states
, and therefore can be complemen
te
d into a Buchi automaton
by simply inverting its
a
cceptance condition. Thus
,
A
S
is a deterministic Buchi
automaton and a run of
infinitely often.
We will handle Buchi in a similar way except this first step will compute the
complement of
S
is accepted if it intersects
A
Q
S
n
A
as another (ND) Buchi [81].
2.
Completing the Fixed Part
S
is an FSM, but it can interpreted also as a special
Buchi automaton; its accepting set of states is the set
F
.
F
,
as an automaton, is incomplete, it can be completed by adding a single new state,
n
F
, which is the only non-accepting state (it is added as a state with no-exit
and a universal self-loop - a “don't care” state). For convenience, the completed
automaton is also denoted by
B
of all its states. Since
F
F
.
3.
Creating the Product
are Buchi automata. The product
of two Buchi automata is conventionally done by introducing a binary flag as
a third entry in the product state. The flag toggles whenever an accepting state
of one of the automaton arguments, indicated by the flag, is just visited. This is
P
D
F
S
.
F
and
S
4
The
general
procedure
would
have
combined
Steps
5
and
6
into
a
single
step,
“complementOmega(
P
)”.
Search WWH ::
Custom Search