Compilation and Synthesis for Real-Time Embedded Controllers - Correct System Design: Recent Insights and Advances - page 266

3.4 Synthesis Under Unconstrained Environment Dynamics

We start with analyzing the synthesis problem with respect to unconstrained en-
vironment dynamics. I.e., inputs may change arbitrarily | but of course nitely
variable | over time. Then, a controller cannot contribute to requirements that
are in terms of inputs only:

Lemma 11. Let be a duration formula and let C be an arbitrary controller

with inputs I free ( ) . Then C satises i is valid.

Proof. It is obvious that validity of implies that C satises , as the trajectories

of are necessarily a subset of the universe Traj of trajectories. For the converse

implication observe that satisfaction of

C

by a trajectory tr does only depend on
the valuation that tr assigns to variables in free (

). Assume that is invalid and

has a trajectory tr 0 that coincides with tr on

let tr 6j = .As C has inputs I , C

all variables in I free ( ). As satisfaction of depends only on the valuation

of its free variables, tr 0 6j = follows. I.e., C does not satisfy . t

This lemma has direct consequences for the feasibility of automatic synthesis.

Theorem 12. Any synthesis procedure is necessarily unsound or fdPe;` = kg -

f R Pg

incomplete (and hence also -incomplete) or ineective. I.e., there is no

eective procedure that generates solutions for any solvable

fdPe;` kg

= control

problem.

Proof. Let synt be a sound and complete mapping from fdPe;` = kg control

problems to timed controllers. Let be a fdPe;` = kg formula.

;

According to Lemma 11, the control problem ( free ( )) has a solution i

; 2

is valid. As synt is sound and complete it follows that ( free ( )) dom ( synt )

i is valid. Thus, an eective mapping synt would provide a decision procedure

for formulae, in contrast to the undecidability result of [48]. This

implies that synt cannot be eective.

fdPe;` = kg

t

Thus, automatic synthesis of controllers is impossible even for the restricted class
of control problems, unless one is willing to sacrice completeness.

However, it is enlightening to observe that the reduction of the decision prob-
lem to the synthesis problem performed in above proof is based on the reduction
of the validity problem to a satisfaction problem in Lemma 11, which in turn
crucially relies on the unconstrained input dynamics of timed controllers. The
latter allows inputs to exhibit arbitrary nitely variable dynamics, which per-
mits above reductions. However, embedded real-time controllers are embedded
into an environment which may not be able to provide arbitrary nitely vari-
able stimuli. Hence, it is questionable whether the full range of nitely variable
trajectories should be regarded as crucial to the satisfaction problem between
controllers and control problems. In most (if not all) application domains, more
restrictive constraints on the temporal evolution of trajectories can be justied
from physical properties of the systems. Therefore, it makes sense to investigate
the synthesis problem for Duration Calculus under suitable restrictions of the
possible input and output behaviour.

fdPe;` = kg