Information Technology Reference
In-Depth Information
3.5
Constrained Environment Dynamics
In the remainder, we will investigate the synthesis problem under some reason-
able constraints on the possible input and output dynamics. Therefore, we say
that
Traj
I
Traj
is a
constraint on input behaviour
for the inputs
I
Varname
implies
tr
0
2
for any
tr
0
2
i
tr
Traj
that diers from
tr
only
on non-input variables (i.e., any
tr
0
that satises
tr
(
2
Traj
I
Traj
I
=
tr
0
(
t
)(
x
)
t
)(
x
)
) x 62 I
).
Similarly,
Traj
O
Traj
is a
constraint on output behaviour
i
tr
2
Traj
O
im-
plies
tr
0
2
for any
tr
0
2
Traj
O
Traj
that diers from
tr
only on non-output
variables.
Denition 13 (Satisfaction under behavioural constraints).
We say that
a
controller
C
satises
Req
under input constraint
Traj
I
and output constraint
Traj
O
is used in a context where
the environment guarantees the constraint on input behaviour then
i Traj
I
\C
[[
C
]]
M
[[
Req
]]
\
Traj
O
. I.e., if
C
C
guarantees
both Req and the constraint on output behaviour.
Now, it is straightforward to dene when a controller solves a control problem
under input and output constraints and when synthesis is sound and complete
with respect to given input and output behavioural constraints.
With this machinery, we are now prepared for investigating the synthesis
problem under behavioural constraints.
Bounded Variability of Input and Output Behaviour.
Considering the
fact that any physically realizable reactive system is subject to band-limitedness,
an easily justiable assumption on
realistic
device models is that state changes
can only come arbitrarily close in time if they originate from dierent subsystems.
As the number of subsystems in a given technical system is nite this implies
that the number of state changes observable at the controller's interface within
a time unit is bounded by a system-dependent natural number. An appropriate
behavioural model is that of
n
-bounded trajectories
, which are those trajectories
that exhibit at most
n
state changes over any unit-length interval of time, where
n 2
IN is a system-dependent parameter. The set of
n
-bounded trajectories is
denoted
Traj
n
. Given inputs
, we furthermore denote by
Traj
I;n
(
Traj
O;m
) the sets of trajectories which after projection to the inputs
I
and outputs
O
I
(outputs
O
-bounded, resp.).
Traj
I;n
and
Traj
O;m
represent constraints on input and output behaviour.
With respect to synthesis it is interesting to see that these easily justiable
constraints suce to facilitate synthesizing timed controllers from
, resp.) are
n
-bounded (
m
fdPe;`
=
kg
control problems:
Theorem 14.
There is an eective, sound, and
-complete synthe-
sis procedure for timed controllers when input dynamics is constrained to be
fdPe;`
=
kg
n
-
bounded and output dynamics is constrained to be
m
-bounded for given
n;m 2
IN
.
Proof.
Using standard techniques, an eective mapping of
formulae
that do contain
exactly one, outermost, negation
to timed automata that recog-
nize their counterexamples of
nite
variability can be dened. Using the timed
fdPe;`
=
kg
Search WWH ::
Custom Search