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

Time-Wise Discrete Input and Output Behaviour. In order to obtain
automatic synthesis procedures for f R P control problems, we may try to

reduce the model class that is regarded crucial to satisfaction still further. If the
devices to be designed are embedded into a synchronously clocked environment
it makes sense to consider trajectories that are changing state only at evenly
spaced time instants. This is captured by studying time-wise discrete trajectories ,
where a trajectory tr

= kg

2

Traj is called time-wise discrete i it has discontinuities
only in time instants which are multiples of the time unit. The set of time-wise
discrete trajectories is denoted DTraj . Accordingly, the input constraint that
restricts inputs to change only in time instants which are multiples of the time
unit is denoted DTraj I , while the corresponding behavioural output constraint
is denoted DTraj O .
The restriction to such time-wise discrete interface behaviour allows auto-
matic synthesis even for f R P

= kg control problems:

f R P

Theorem 15. There is an eective, sound, and = kg -complete (and thus

also -complete) synthesis procedure for timed controllers when input

and output behaviour is constrained to be time-wise discrete.

fdPe;` = kg

Proof. It is a tedious, yet mostly straightforward exercise to show that for any
formula f R P

-regular
language to real-time based on the convention that one letter per time unit is
traversed. A corresponding

of the = kg fragment, M [[ ]] \ DTraj is an unrolling of an !

-automaton Aut twd can be eectively constructed
(the construction is fully pursued in [14, chapter 6.3]).
Now, a similar construction as in the proof of the previous theorem can be
applied to Aut twd to obtain an appropriate game graph representing the be-
haviorally constrained synthesis problem. However, this time the game graph
obtained is

!

-regular as Aut twd

is an untimed nite automaton and the be-
havioural constraints can also be formalised with untimed automata using the
convention that one letter per time unit is traversed. This eectively reduces the
synthesis problem to strategy construction in

!

-regular games. As algorithms for
the latter are well-known (cf. e.g. [44]), this yields the desired synthesis method.
Details of the construction can be found in [13,14].

!

t

As, for example, the ProCoS gas-burner requirements specication [41] can
be expressed in the

f R P

subset of DC, this allows automatic synthesis of a
timed controller directly from the requirements specication of the gas-burner,
which is shown in the next section.

= kg

3.6 A Case Study: Synthesizing a Synchronous Controller for the

ProCoS Gas-Burner

The ProCoS gas-burner [41,42] is a simple model of a computer-controlled gas-
burner, depicted in Fig. 1. Its embedded controller has just three binary control
lines connected to the environment: hr signals heat requests from a thermostat,
fl signals whether the flame is burning, and gas controls the gas valve. The
gas valve is the only actuator in the system, and gas is expected to usually