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

of time points b ≤ τ 0 <τ 1 < ... < τ m ≤ e such that I , [ τ i ,τ i +1 ] | = int ∧ =1,

τ 0 − b< 1and e − τ m < 1, and [ τ i ,τ i +1 ] are the only subintervals of [ b, e ]that

that satisfy ( int ∧ =1).

ID ID

specifies all the
properties of integer intervals except that their endpoints are integer.

Let denote the set of these three axioms 1, 2 and 3.

Proposition 1
1. Let

be an interpretation satisfying that int I ([ b, e ]) = true iff [ b, e ] is an
integer interval. Then

I

I , [ b, e ] |

= D for any integer interval [ b.e ] , and for any

formula D ∈ID.
2. Let I be an interpretation satisfying that I , [ b, e ] | = D for any interval [ b.e ] ,

and for any formula D .Then,int I ([0 , 0]) = true implies that for

int I ([ b, e ]) = true iff [ b, e ] is an integer interval.

∈ID

Proof. The item 1 is obvious, and we only give a proof of Item 2 here. Let us
consider an interval [0 ,n ]with n> 100. From the fact that I , [0 ,n ] | = D where

D is the formula 3, we have that there are points 0 ≤ τ 0 <τ 1 < ... < τ m ≤ e

such that I , [ τ i ,τ i + i ] | = int ∧ =1, τ 0 < 1and n − τ m < 1, and

( true ( int =1) =1) ∗ )

I , [ τ 0 ,τ m ] | =( ¬ ∧ ¬ ( int ∧ ∧

¬ ¬

( int

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

(

If τ 0 > 0, from the axiom 2, it follows that I , [0 ,k ] | = int for all k ∈ N and

k ≤ n and k<τ k <k + 1. Applying the axiom 1 for the interval [0 ,k ] implies

=1) ∗ that I , [ k, k +1] | = int ∧ =1.Consequently, I , [ m − 1 ,τ m ] | = ¬ ( int ∧

and I , [ m − 2 ,m 1 ] | =( int ∧ = 1). This is a contradiction to I , [ τ 0 ,τ m ] | =

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

Note that Item 2 of Proposition 1 can be generalised as

Let I be an interpretation satisfying that I , [ b, e ] | = D for any inter-

val [ b.e ], and for any formula D

+ , h< 1. Then,
int I ([ h, h ]) = true implies that for int I ([ b, e ]) = true iff [ b, e ]isofthe
form [ h + n, h + m ], m, n

∈ID .Let h ∈R

∈ N and n ≤ m .

So, is a set of formulas specifying the set of intervals of a discrete time

obtained by shifting

ID

by h time units ( h< 1).
The state variable C can also express if an interval is an integer interval.
Namely, we have

N

( C ∨¬ C ) ∧ =1 ⇒ int

int ∧ =1 ⇒ ( C ∨¬ C )

true int true

C ¬ C ⇒

true int true

¬ C C ⇒

=1) ( int ( int ∧ ∧ =1) ⇒

=1) ( (( C ∧ ¬ C ∧ =1)) ∨

=1) (

(( ¬ C ∧ C ∧ =1))

Let specifies all the properties of the

special clock state variable C . Any interval satisfying int

CC denote the set of these formulas. CC

∧ > 0 can be expressed