Hardware Reference
In-Depth Information
given game computed with that model is not empty, and yet there is no winning
strategy, i.e., one that brings the game to a state that achieves the goal.
Does the introduction of specifications expressed by co-Buchi automata address
adequately these issues? Argue it in the case of the Wolf-Goat-Cabbage game.
18.3.
Compare the models and solutions of the Wolf-Goat-Cabbage game as
described in Problem 17.2 as a regular game, and in Problem
18.2
as an
!
-regular
game.
Are the solutions different? If no, why not? If yes, what is the interpretation of
their differences with the respect to the acceptance conditions of the two models?
18.4. Aircraft Control
The problem is to keep an airplane within a specified range of altitudes above
ground, e.g., between 1 and 2 units of elevation above ground. The land elevation
varies and there is a random up or down air draft causing the aircrafts rate of climb
to alter.
Notice that in the case of airplane control, if we adopt the point-of-view of
Chap. 17 where we model the problem with FSMs and if we start on the ground,
one solution would be that the system does not progress at all from the initial state,
whereas we are looking for a control where we take off and finally keep within
the interval of allowed elevations forever. For this reason we need to model the
specification using co-Buchi conditions.
The fixed automaton,
, describes the dynamics of the flight in terms of the
planes position, elevation and rate of climb. It has 3 inputs, 1 for the random air
draft input and 2 for the auto-pilot control. The auto-pilot has two controls to adjust
the rate of climb, one can increase or decrease it by 1 or 2 units and the other is a
binary boost which doubles the effect of the first input. The airplane takes off at the
ground elevation, so it is not initially in the accepting set of states. The up or down
draft of air is limited to affect the rate of climb by at most one unit. For simplicity,
there are 16 ground positions with different elevations. The plane flies in a loop over
these positions. The fixed part,
F
, describes these dynamics. It has two inputs from
the controller,
i1
and
i2
, and one output,
out
.
The specification automaton has two states,
F
a
and
c
of which
a
is the initial state
and
is the only accepting state. Its input,
out
, comes from the fixed part and simply
indicates if the elevation is OK or not. There is a transition from
c
a
to
c
if
out = OK
and from
if
out = notOK
. This specification is clearly co-Buchi, but not
co-looping since it is possible to exit the accepting set of states. Model and solve
the aircraft control problem with the procedure described in this chapter.
c
to
a
18.5.
Model and solve the application of the Guideway scheduling synthesis
problem discussed in [119].
18.6.
In the co-Buchi case we find an automaton such that any cycle has all of its
states in the set of final states. The first thing we do is to find the largest prefix-closed
and input-progressive solution without enforcing the co-Buchi conditions. Then we
trim this solution using the co-Buchi conditions by eliminating loops that are not
contained in the final set. We keep the resulting automaton input-progressive while
Search WWH ::
Custom Search