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

logics that provide a very high level of abstraction from operational detail, like
e.g. the monadic second order logic of temporal distance [46] or the Duration
Calculus [49].
Unfortunately, in the realm of dense metric time, logics featuring rich metric-
time vocabulary and full negation tend to become undecidable (e.g., above two
are), which has direct impact on the feasibility of sound and complete auto-
matic synthesis procedures. However, the argument which makes decidability a
necessary condition for feasibility of synthesis (to be reviewed in Sect. 3.4) relies
on an essentially unconstrained environment dynamics. We argue that through
exploitation of general constraints on environment dynamics, synthesis methods
can be exposed even for some undecidable metric real-time logics, and exemplify
this on synthesis procedures for timed controllers from dense-time Duration Cal-
culus in Sect. 3.5.

3.1 Duration Calculus
Duration Calculus (abbreviated DC in the remainder) is a real-time logic that
is specially tailored towards reasoning about durational constraints on time-
dependent Boolean-valued states. The syntax of the subsets of DC formulae
that we will study is
hformulai ::= hatomicformij:hformulaij
( hformulai^hformulai ) j ( hformulai ; hformulai )
k :: 2 IN
h statei ::= hvariableij:hstateij ( hstatei^hstatei )
hvariablei :: 2 Varname
Concerning the available atomic formulae, we distinguish two dierent subsets of
DC. In the rst subset, often called the

fdPe;` = kg fragment, atomic formulae

take the form

hatomicformi ::= dhstateie j ` = k;

f R P while in the so-called fragment,

hatomicformi

= kg

::= hstatei = k:

Duration Calculus is interpreted over trajectories

de =

tr 2 Traj f tr : Time ! Varname ! IB j Time = R ; tr nitely variable g

0

that provide a nitely variable, time-dependent, Boolean-valued valuation of
variables. Finite variability | sometimes also called non-Zenoness | means
that only nitely many state changes may occur within any nite time interval.
The denition of satisfaction of a formula by a trajectory tr , denoted tr j = is

given in Table 2. The set of models of , i.e. trajectories satisfying , is denoted

M [[ ]] .

As usual, we say that is valid i M [[ ]] = Traj . According to [48], validity

is undecidable for the fragment fdPe;` = kg . Consequently, the same applies for

f R P can be encoded as R :P ( R true =0)and

the fragment = kg ,as dPe =0 ^:

as R true = ` = k k ,resp.