Specifying Various Time Models with Temporal Propositional Variables in Duration Calculus - Formal Methods and Hybrid Real-Time Systems - page 173

A relatively complete proof system for Duration Calculus with no operator ∗
and 0 has been given in [2], and the complete proof system for Duration Calculus
with Iteration on the abstract time domain is given in [6].

3 Specifying Substructure of Time with Temporal

Propositional Letters

In this section we consider how Duration Calculus can specify some classes of
time models with temporal propositional letters. We show that different classes
of Duration Calculus time models can be expressed by sub-languages of Dura-
tion Calculus. Hence, there is no need to have different definitions of Duration
Calculus for different classes of time models. Using the original DC with the
sub-language of DC for a class of models as the assumption we can reason about
the validity in the model class.

3.1 Discrete Duration Calculus Models

Discrete models of Duration Calculus use the set of natural numbers N ,which

+ , for time (we assume that 0

is a subset of ). We can embed the dis-

crete time models into continuous time models by considering a state variable
in discrete DC models as a state in continuous models that can change its value
only at the integer points. For that purpose, we introduce several fresh tempo-
ral propositional letters and state variables with specific meaning. Let int be a
temporal propositional letter with the meaning that int is interpreted as 1 for
an interval if and only if the interval is from an integer to an integer, i.e. for
any interpretation

R ∈ N

.Let C be a state variable that
changes its value at each natural number which represents a tick of the real-time
clock, i.e. C I ( t )=1iff

I , int I ([ a, b ]) = 1 iff a, b ∈ N

is odd. The axioms to characterise the properties of
the temporal propositional letter int can be given as follows. First, the integer
intervals have integral endpoints, and remain integer intervals when extended
by 1 time unit:

t

=0) ( int =1) ∗ ) int ⇒ (( int ∧ ∧ ∧

=1) ∗ ( int (( int ∧ ∧ = 0)) (1)

int ( =1) ⇒ int

(2)

Second, int = 1 should be a unique partition of the greatest integral subin-

terval of any interval with length 2 or more, i.e.

∧

< 1 (( int =1) ∗ ∧ ≥ 2 ⇒ ∧ (3)

( true ( int =1) =1) ∗ ) ¬ ∧ ¬ ( int ∧ ∧

=1) ∗ ( int =1) true )) ¬ ( ¬ ( int ∧ ∧

< 1

Similarly to Lemma 3.2 in [4] we can show that the axiom 3 is equivalent to the
fact that any interval [ b, e ] that have the length 2 or longer has the unique set