More in detail, in our technique we have two
phases, which we describe in the following.
3.1 Optimal Raw Controller
Synthesis Phase
In the first phase, an explicit model checking algo-
rithm is used, which performs a Depth First (DF) visit
of all the reachable states of S, starting from s
0
. As
usual, a hash table HT is used in order to store al-
ready visited states. Moreover, the stack holds, to-
gether with states, also the next action to be explored.
However, the DF visit is enriched in order to gen-
erate the controller C. To this aim, HT also stores, for
each visited state, a flag toGoal, initially set to 0.
When a goal state g is reached, then the states in the
current path from s
0
to g (that is to say, the states cur-
rently on the stack) will have this flag set to 1, as soon
as the visit backtracks to them. This is to signify that
such states indeed reach a goal, and may be put in C –
together with the action taken and the number of steps
they need to reach the goal itself. In this way, when a
state s with the toGoal flag set to 1 is reached, then
we can analogously set the toGoal flag on all the
states currently on the stack, and put them on C.
However, this scheme may fail in the following
case. Suppose that a cycle s
1
r
1
. . . r
h
s
2
t
1
. . . t
k
s
1
is
found, were s
1
and s
2
are on the stack. When analyz-
ing t
k
, the toGoal flag of s
1
is not set to 1, since we
have not backtracked from s
2
yet. However, the visit
is truncated, since s
1
is already visited, thus t
k
will
not be inserted in C (unless it was already present, or
it reaches a goal through another path which does not
intersect the stack).
To avoid this, a predecessor table PT is maintained
for each state which is visited again while it is on the
stack. We have that PT stores all the paths leading
from a state on the stack and another state previously
on the stack. Thus, in the situation described above,
the path r
1
. . . r
h
s
2
t
1
. . . t
k
is added to the predeces-
sor table of s
1
. Thus, when the DF visit of s
1
is fin-
ished, all the states in its predecessor table are added
on C by using a backward visit, provided that s
1
in-
deed reaches a goal.
Finally, in order to preserve optimality, each inser-
tion on C is effectively performed only if the number
of steps to be inserted is less than the already stored
one.
3.2 Controller Strengthening Phase
The second phase of our approach performs a
strengthening of the controller C generated by the first
phase. In fact, C only contains an optimal plan that
can be used to drive S from s
0
to the goal. That is,
C does not take into account any state outside the op-
timal plan. The final controller should be aware of
a larger set of states: indeed, the dynamics of S can
be very complex, and a particular setting of the con-
trol variables may not always drive S to the expected
state. That is, all the state variables usually have a
specific tolerance, and the reactions to controls are
subject to these tolerances. For this reason, we refer
to the controller C output by the first phase as a raw
controller.
Therefore, to ensure the robustness of the con-
troller, in the second strengthening phase we explore a
larger number of states obtained by randomly perturb-
ing the raw controller states. That is, for each state s
in the raw controller table C, we apply a set of small
random changes, bounded by the state variables toler-
ances, and obtain a new state s
′
. Then, from each new
state s
′
, we start a breadth first visit of the state space
of S stopping as soon as we reach a state s
′′
that is
already in C. The path from s
′
to s
′′
is stored in C and
the process is restarted.
After some iterations of this process, we have that
C is now able to drive S from any reasonable system
state to the nearest state of the optimal controller and,
from there, reach a goal. That is, C is now our final
optimal controller.
4 THE CONTROLLER
GENERATION PROCESS
The CGMurϕ tool is an extended version of the
CMurϕ (Cached Murphi Web Page, 2006; Della
Penna et al., 2004) model checker. It is based on an
explicit enumeration of the state space, originally de-
veloped to verify protocol-like systems. We choose
CMurϕ as a base to develop our controller generator
since it already implements the most common state
space compression techniques, such as bit compres-
sion (Murphi Web Page, 2004) and hash compaction
(Stern and Dill, 1998; Stern and Dill, 1995), use-
ful to decrease the memory requirements of the con-
troller generation process when dealing with large-
dimensional control systems. In particular, when bit
compression is enabled, CMurϕ saves memory by
using every bit of the state descriptor, the memory
structure maintaining the state variables, instead of
aligning the state variables on byte boundaries (this
saves on average 300% of memory). When using hash
compaction, compressed values, also called state sig-
natures, are used to remember visited states instead
of full state descriptors. The compression ratio can
be set to obtain an arbitrary state site (CMurϕ default
is 40 bits), but is lossy, so there is a certain probabil-
ity that some states will have the same signature after
compression.
ICINCO 2006 - INTELLIGENT CONTROL SYSTEMS AND OPTIMIZATION
28