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

Finally, if timed transition tables are to be used as embedded controllers, we
must require that they be input open. Due to the clock-dependent behaviour, this
involves a slight extension to above notion of being input-open: a timed transition
table is input-open i from any state

under any possible clock valuation there

is a transition for each IB. A timed transition table with that property

is called timed controller (with input

i 2 I !

) in the remainder.
Based on the denition of trajectories of timed controllers, it is straightfor-
ward to dene when a timed controller satises a DC formula. The criterion is
trajectory inclusion.

I and outputs O

C

Denition 8 (Satisfaction). Let be a timed controller and aDuration

C C C M

Calculus formula. We say that satises i [[ ]] [[ ]] .

3.3 Control Problems and Controller Synthesis

Duration Calculus was designed for bridging the gap between requirements cap-
ture and controller implementation in an embedded-controller design activity.
Consequently, we are interested in the satisfaction problem between controllers
from the design space and control problems expressed in Duration Calculus.

Denition 9 (Control problem). A control problem is a pair ( Req ) ,where

Req is a formula of Duration Calculus specifying the admissible controller be-
haviours and

;I

I

Varname is a set of variable names specifying the inputs to
the controller, i.e. those variables that the controller cannot control and hence is
not allowed to constrain in their evolution over time. We say that a control prob-
lem ( Req

R

;I ) is a fdPe;` = kg control problem (or a f P = kg control problem)

f R P

i Req is a fdPe;` = kg formula (a = kg formula, resp.).

A controller C is said to solve the control problem ( Req ;I ) i C has inputs

I and satises Req.

Aiming at solutions to control problems we are interested in synthesis meth-
ods that derive controllers from control problems. Such a synthesis method can
be understood as a partial mapping synt from control problems to controllers.
Let synt be a (for the moment not necessarily eective) partial function from
the set of control problems to controllers. We will now dene when synt provides
a sound and complete synthesis method for control problems.

Denition 10 (Soundness and completeness of a synthesis procedure).
We say

1. that synt is sound i it maps control problems to solutions thereof, and
2. that synt is f R P

fdPe;` = kg -complete (or = kg -complete) i its domain

f R P

contains all fdPe;` = kg control problems ( = kg control problems,

resp.) that are solvable by timed controllers.

The interesting question is whether there is a sound and complete mechanic
synthesis method for timed controllers from DC-based control problems. Unfor-
tunately, the answer is negative, as is shown in the next section.