Axioms for real-time logics.
This paper presents a complete axiomatization of two decidable propositional real-time linear temporal logics: Event Clock Logic (EventClockTL) and Metric Interval Temporal Logic with past (MetricIntervalTL). The completeness proof consists of an effective proof building procedure for EventClockTL. From this result we obtain a complete axiomatization of MetricIntervalTL by providing axioms translating formulae, the two logics being equally expressive. Our proof is structured to yield axiomatizations also for interesting fragments of these logics, such as the linear temporal logic of the real numbers (TLR).
Introduction
Many real-time systems are safety-critical, and therefore deserve to be specified
with mathematical precision. To this end, real-time linear temporal logics
[5] have been proposed and served as the basis of specification languages.
preliminary version of this paper appeared in the Proceedings of the Tenth
International Conference on Concurrency Theory (CONCUR), Lecture Notes in
Computer Science 1466, Springer-Verlag, 1998, pp. 219-236.
?? This work is supported in part by the ONR YIP award N00014-95-1-0520, the NSF
CAREER award CCR-9501708, the NSF grant CCR-9504469, the DARPA/NASA
grant NAG2-1214, the ARO MURI grant DAAH-04-96-1-0341, the Belgian National
Fund for Scientific Research (FNRS), the European Commission under WGs Aspire
and Fireworks, the Portuguese FCT under Praxis XXI, the Walloon region, and
Belgacom.
Preprint submitted to Elsevier Preprint 12 November 1999
They use real numbers for time, which has advantages for specification and
compositionality. Several syntaxes are possible to deal with real time: freeze
quantification [4,12], explicit clocks in a first-order temporal logic [11,21], integration
over intervals [10], and time-bounded operators [17]. We study logics
with time-bounded operators, because those logics are the only ones which
have, under certain restrictions, a decidable satisfiability problem [5].
The logic extends the operators of temporal logic to allow the
specification of time bounds on the scope of temporal operators. For example,
the that "every p event is followed
by some q event after exactly 1 time unit." It has been shown that the logic
undecidable and even not recursively axiomatizable [4]. One reason
for this undecidability result is the ability of to specify exact
distances between events; these exact distance properties are called punctuality
properties. The logic MetricIntervalTL is obtained from
removing the ability to specify punctuality properties: all bounds appearing
in temporal operators must be non-singular intervals. For example, the formula
which expresses that "every p event is followed by some q
event after at least 1 time unit and at most 2 time units," is a MetricIntervalTL
formula, because the interval [1; 2] is non-singular. The logic MetricIntervalTL
is decidable [3]. This decidability result allows program verification using automatic
techniques. However, when the specification is large or when it contains
first-order parts, a mixture of automatic and manual proof generation is more
suitable. Unfortunately, the current automatic reasoning techniques (based on
timed automata) do not provide explicit proofs. Secondly, an axiomatization
provides deep insights into a logic. Third, a complete axiomatization serves
as a yardstick for a definition of relative completeness for more expressive logics
(such as first-order extensions) that are not completely axiomatizable, in
the style of [16,20]. This is why the axiomatization of time-bounded operator
logics is cited as an important open question in [5,17].
We provide a complete axiom system for decidable real-time logics, and a
proof-building procedure. We build the axiom system by considering increasingly
complex logics: LTR [6], EventClockTL with past clocks only, Event-
with past and future clocks (also called
with past and future operators.
The method that we use to show the completeness of our axiomatization is
standard: we show that it is possible to construct a model for each consistent
formula. More specifically, our proof of completeness is an adaptation and
an extension of the proof of completeness of the axiomatization of
The handling of the real-time operators requires care and represents the core
technical contribution of this paper. Some previous works presented axioms
for real-time logics, but no true (versus relative) completeness result for dense
real-time. In [12], completeness results are given for real-time logics with explicit
clocks and time-bounded operators, but for time modeled by a discrete
time domain, the natural numbers. In [9,7], a completeness result is presented
for the qualitative (non real-time) part of the logics considered in this pa-
per. There, the time domain considered is dense but the hypothesis of finite
variability that we consider 1 is dropped and, as a consequence, different techniques
have to be applied. In [17], axioms for real-time logics are proposed.
These axioms are given for first-order extensions of our logics, but no relative
completeness results are studied (note that no completeness result can be
given for first-order temporal logics.) Finally, a relative completeness result
is given for the duration calculus in [10]. The completeness is relative to the
hypothesis that valid interval logic formulae are provable.
Models and logics for real-time
2.1 Models
As time domain T, we choose the nonnegative real numbers R
0g. This dense domain is natural and gives many advantages detailed
elsewhere: compositionality [6], full abstractness [6], stuttering independence
[1], easy refinement. These advantages, and the results of this paper, mainly
depend on density: they can easily be adapted for the rational numbers Q, the
real numbers R. To avoid Zeno's paradox, we add to our models the condition
of finite variability [6] (condition (3) below): only finitely many state changes
can occur in a finite amount of time.
An interval I ' T is a convex subset of time. Given t 2 T, we freely use
notations such as t + I for the interval ft 0 j 9t 00 2 I with t
the constraint "t ? t 0 for all t 0 2 I ", # I for the interval ft ? 0j9t g.
A bounded non-empty interval has an infimum (also called greatest lower
bound, or left endpoint, or begin) and a supremum (also called least upper
bound, or right endpoint, or end). Such an interval is thus usually written
as e.g. (l; r], where l is the left endpoint, the rounded parenthesis in "(l"
indicates that l is excluded from the interval, r is the right endpoint, and
the square parenthesis in "r]" indicates that r is included in the interval.
The interval is called left-open and right-closed. If we extend the notation, as
usual, by allowing r to be 1, then any interval can be written in this form.
Two intervals I and J are adjacent if the right endpoint of I, noted r(I), is
equal to the left endpoint of J , noted l(J ), and either I is right-open and J
is left-closed or I is right-closed and J is left-open. We say that a non-empty
1 In every finite interval of time, the interpretation of propositions can change only
finitely many times.
interval I is singular if r(I). In this case, we often use the
rather than [t; t]. Similarly, ! l abbreviates (0; l), etc. An interval sequence
is an infinite sequence of non-empty bounded intervals so
that (1) the first interval I 0 is left-closed with left endpoint 0, (2) for all i - 0,
the intervals I i and I i+1 are adjacent, and (3) for all t 2 T, there exists an
Consequently, an interval sequence partitions time so
that every bounded subset of T is covered by finitely many elements of the
partition. Let P be a set of propositional symbols. A state s ' P is a set of
propositions. A timed state sequence -s; -
I) is a pair that consists of an
infinite sequence - s of states and an interval sequence -
I. Intuitively, it states
the period I i during which the state was s i . Thus, a timed state sequence -
can be viewed as a function from T to 2 P , indicating for each time t 2 T a
state -
2.2 The Linear Temporal Logic of Real Numbers (LTR)
The formulae of LTR [6] are built from propositional symbols, boolean con-
nectives, the temporal "until" and "since" and are generated by the following
where p is a proposition.
The LTR formula OE holds at time t 2 T of the timed state sequence - , written
according to the following definition, where we
An LTR formula OE is satisfiable if there exists - and a time t such that (-; t)
OE, an LTR formula OE is valid if for every - and every time t we have (-; t)
This logic was shown to be expressively equivalent to the monadic first-order
logic of the order over the reals [15].
Our operators U; S are slightly non-classical, but more intuitive: they do not
require OE 2 to start in a left-closed interval.
On the other hand, each of them is slightly weaker than its classical variant,
but together they have the same expressive power, as we show by providing
mutual translations below in sections 2.2.1 and 2.4.1. It is thus a simple matter
of taste. We will note the classical until as -
U.
2.2.1 Abbreviations
In the sequel we use the following abbreviations:
defined below).
the "Until" reflexive for its first argument;
the "Until" reflexive for its two arguments;
meaning "just after in the future" or "for a short time in the
future". The dual of fl is noted K + in [9], and it means thus "arbitrarily
close in the future". We don't introduce it, since we will see that due to
finite variability, fl is his own dual.
meaning "eventually in the future";
meaning "always in the future";
ffl their reflexive counterparts: \Sigma
meaning "unless in the future";
ffl its reflexive counterparts: W
and the past counterpart of all those abbreviations:
the "Since" reflexive for its first argument;
the "Since" reflexive for its two arguments;
meaning "just before in the past" or "arbitrarily close in the
meaning "eventually in the past";
meaning "always in the past";
ffl their reflexive counterparts:
meaning "unless in the past";
ffl its reflexive counterparts: Z
2.3 Event-Clock Temporal Logic
The formulae of EventClockTL [22] are built from propositional symbols, boolean
connectives, the temporal "until" and "since" operators, and two real-time op-
erators: at any time t, the history operator / I OE asserts that OE was true last in
the interval t \Gamma I, and the prediction operator . I OE asserts that OE will be true
next in the interval t I. The formulae of EventClockTL are generated by the
following
I OE
where p is a proposition and I is an interval which can be empty, singular and
whose bounds are natural numbers (or infinite). The
holds at time t 2 T of the timed state sequence - , written (-; t) according
timevalue
of the
for
timed
trace
sequence
event tick reset event reset
event
reset
undefined small big blocked small small blocked small
tick
event
clock
Fig. 1. A History clock evolving over time
to the rules for LTR and the following additional clauses:
t
A . I OE formula can intuitively be seen as expressing a constraint on the value
of a clock that measures the distance from now to the next time where the
formula OE will be true. In the sequel, we use this analogy and call this clock a
prediction clock for OE. Similarly, a / I OE formula can be seen as a constraint on
the value of a clock that records the distance from now to the last time such
that the formula OE was true. We call such a clock a history clock for OE. For a
history (resp. prediction) clock about OE,
ffl the next / =1 OE (resp. previous . =1 OE) is called its tick;
ffl the point where OE held last (resp. will hold next) is called its event;
ffl the point (if any) at which OE will hold again (resp. held last) is called its
reset;
ffl if OE is true at time t and was true just before t (resp. and will still be true
just after t) then we say that the clock is blocked at time t;
ffl if OE was never true before t (resp. will never be true after t) then the clock
is undefined at time t.
The main part of our axiomatization consists in describing the behavior and
the relation of such clocks over time. For a more formal account on the relation
between EventClockTL formulae and clocks, we refer the interested reader
to [22]. We simply recall:
Theorem 1 [22] The satisfiability problem for EventClockTL is complete for
Pspace.
which is the best result that can be expected, since any temporal logic has
this complexity.
Example 1  (p ! . =5 p) asserts that after every p state, the first subsequent
p state is exactly 5 units later (so in between, p is false); the formula  (/ =5
asserts that whenever the last p state is exactly 5 units ago, then q is true
now (time-out).
2.4 Metric-Interval Temporal Logic
restricts the power of MetricTLin an apparently different way
from EventClockTL: here the real-time constraints are attached directly to
the until, but cannot be punctual. The formulae of MetricIntervalTL [3] are
built from propositional symbols, boolean connectives, and the time-bounded
"until" and "since" operators:
U I OE 2 j OE 1
S I OE 2
where p is a proposition and I is a nonsingular interval whose bounds are
natural numbers or infinite. The holds at time
of the timed state sequence - , written (-; t) according to the
following definition (the propositional and boolean clauses are as for LTR):
U I OE 2 iff 9t
Here, we have used the classical until to respect the original definition, but
this doesn't matter as explained in subsection 2.2.1.
Theorem 2 [3] The satisfiability problem for MetricIntervalTL is complete for
Expspace.
So although the logics are equally expressive, their translation must be difficult
enough to absorb the difference in complexity. Our translation, presented in
section 5, indeed gives an exponential blowup of formulae.
2.4.1 Abbreviations
In the sequel we use the following abbreviations:
U (0;1) OE 2 , the untimed "Until" of MetricIntervalTL.
UOE expresses that the next OE-interval is left-closed.
U I OE 2 .
U I OE, meaning "within I";
ffl   I OE j :\Sigma I :OE, meaning "always within I";
and the past counterpart of all those abbreviations. The fact that we use the
same notations as in the other logics is intentional and harmless, since the
definitions are semantically equivalent.
Furthermore, now that we have re-defined the basic operators of EventClockTL,
we also use its abbreviations.
asserts that every q state is preceded by a p state
of time difference at most 5, which is right-closed, and all intermediate states
are r states; the formula  (p ! \Sigma [5;6) p) asserts that every p state is followed
by a p state at a time difference of at least 5 and less than 6 time units. This
is weaker than the EventClockTL example, since p might also hold in between,
and of course because 5 units are not exactly required.
3 Axiomatization of EventClockTL
In section 4, we will present a proof-building procedure for EventClockTL. In
this section, we simply collect the axioms used in the procedure, and present
their intuitive meaning. Our logics are symmetric for past and future (a duality
that we call the "mirror principle"), except that time begins but does not
end: therefore the axioms will be only written for the future, but with the
understanding that their mirror images, obtained by replacing U by S, . by /,
etc. are also axioms. This does not mean that we have an axiomatization of the
future fragment of these logics: our axioms make past and future interact, and
our proof technique makes this interaction is unavoidable, mainly in axiom
(11).
3.1 Qualitative axioms (complete for LTR)
We use the rule of inference of replacement of equivalent formulae:
(1)
All propositional tautologies (2)
For the non-metric part, we use the following axioms and their mirror images:
They mainly make use of the fl operator, because as we shall see, it corresponds
to the transition relation of our structure. Axiom (3) is the usual
necessitation or modal generalization rule, expressed as an axiom. Similarly,
(4) is the usual weakening principle, expressed in a slightly non-classical form.
(5), (6) allow to distribute fl with boolean operators. Note that the validity
of (6) requires finite variability. (7), (8) describe how the U and S operators
are transmitted over interval boundaries. (9) gives local consistency conditions
over this transmission. (10) ensures eventuality when combined with (11). It
can also be seen as weakening the left side of the U to ?. The induction axiom
is essential to express finite variability: If a property is transmitted over
interval boundaries, then it will be true at any point; said otherwise, any point
is reached by crossing finitely many interval boundaries.
The axioms below express that time begins (12) but has no end (13):
We have written the other axioms so that they are independent of the begin
or end axioms, in order to deal easily with other time domains (see subsection
4.4). This is why some apparently spurious fl? occur above, e.g. in (11): they
are useful when the future is bounded.
Remark 3 Theorem 21 shows that the axioms above form a complete axiomatization
of the logic of the real numbers with finite variability, defined as LTR
in [6]. The system proposed in [6] is unfortunately unsound, redundant and
incomplete. Indeed, axiom F5 of [6] is unsound; axiom F7 can be deduced
from axiom F8; and the system cannot derive the induction axiom (11). To
see this last point, take the structure formed by R -0 followed by R, with finite
variability: it satisfies the system of [6] (corrected according to [7]) but not the
induction axiom. Thus this valid formula cannot be derived in their system.
3.2 Quantitative axioms
For the real-time part, we first describe the static behavior; intersection, union
of intervals can be translated into conjunction, disjunction due to the fact that
there is a single next event:
. I[J OE $ . I OE - . J OE (14)
. I"J OE $ . I OE - . J OE (15)
Since . is a strict future operator, the value 0 is never used:
If we do not constrain the time of next occurrence, we simply require a future
occurrence:
Finally the addition corresponds to nesting:
The next step of the proof is to describe how a single real-time . I OE evolves
over time, using fl and -. We use (20) to reduce left-open events to the easier
case of left-closed ones.
These axioms are complete for formulae where the only real-time operators
are prediction operators . I OE and they all track the same (qualitative) formula
OE. For a single history tracked formula, we use the mirror of the axioms plus
an axiom expressing that the future time is infinite, so that any bound will be
exceeded:
The description provided by these axioms are mostly expressed by the automaton
of figure 2, showing the possible evolution of history predicates.
This figure will receive a formal status in lemma 22. Most consequences of
OE
Fig. 2. The possible evolutions of a history clock
these axioms can simply be read from this automaton: For instance, /?1 OE !
(/ ?1 OE - :OE)U - fl /!1 OE is checked by looking at paths starting from /?1 OE.
As soon as several such formulae are present, we cannot just combine their
individual behavior, because the .; / have to evolve synchronously (with the
common implicit real time). We use a family of axioms (and their mirrors) to
express this common speed. They express the properties of order and addition,
but expressed with different clocks. Said otherwise, the ordering of the ticks
should correspond to the ordering of their events. We use U (or W) to express
the ordering: :pUq means that q will occur before (or at the same time as)
any p. E.g. in (26), the antecedent / =1 OE states that OE ticks now, thus after of
together with /. Then their events shall be in the same order: :OES/. Similarly,
(30) says that if last OE was less than 1 ago, and / was even closer, than last
was less than 1 ago as well.
(.
(.
3.3 Theorems
We will use in the proof some derived rules of LTR (and thus EventClockTL):
Lemma 4 The rules of modus ponens and modal generalization are derivable.
OE
Proof.
ffl the rule of modus ponens (32) is derived from replacement (1) as follows:
from OE we deduce propositionally OE $ ?; by (1) we replace OE by ? in
propositionally /.
ffl the rule of modal generalization (33) (also called necessitation) is derived
similarly from (1) and (3): From OE, we deduce :OE $ ?. Replacing in (3),
we obtain :(/U:OE). By taking / := ?, we get \LambdaOE.
We'll also need some theorems:
. I OE $ :\SigmaOE - . I OE (43)
. I OE
. I OE ! . J OE with (I ' J) (45)
Proof.
By (13), we can remove the condition fl? in the mirror of (6).
We use (5) and duality through (34).
Expanding the definition of -, we have to prove ?SOE ! ?S?. This
results from the mirror of (4) with OE := ?; / := ?; / 0 := OE.
From (36). So all - formulae are false at the beginning of time.
(38) By (8).
By (7).
(40) By (13), (10).
(41) Take (14) with I := ;; J := [0; 0]. By (16) we obtain
(42) We'll prove its mirror. By (14), / I / ! /? 0/. By (17), \Sigma/. By (10), fl/.
(43) By (15), (14), (17).
(44) By (15), (14), (17).
(45) By (15). (or by (14)).
By (4).
4 Completeness of the axiomatic system for EventClockTL
As usual, the soundness of the system of axioms can be proved by a simple
inductive reasoning on the structure of the axioms. We concentrate here on
the more difficult part: the completeness of the proposed axiomatic system. As
usual with temporal logic, we only have weak completeness: for every valid formula
of EventClockTL, there exists a finite formal derivation in our axiomatic
system for that formula. So if As often, it is more convenient to
prove the contrapositive: every consistent EventClockTL formula is satisfiable.
Due to the mirror principle, most explanations will be given for the future
only.
Our proof is divided in steps, that prove the completeness for increasing fragments
of EventClockTL.
(1) We first deal with the qualitative part, without real-time. This part of
the proof follows roughly the completeness proof of [19] for discrete-time
logic.
(a) We work with worlds that are built syntactically, by maximal consistent
sets of formulae.
(b) We identify the transition relation, and its syntactic counterpart: it
was the "next" operator for discrete-time logic [19], here it is the fl,
expressing the transition from a closed to an open interval, and -,
expressing the transition from an open to a closed interval.
(c) We impose axioms describing the possible transitions for each operator

(d) We give an induction principle (11) that extends the properties of
local transitions to global properties.
(2) For the real-time part:
(a) We give the statics of a clock;
(b) We describe the transitions of a clock;
(c) By further axioms, we force the clocks to evolve simultaneously. The
completeness of these axioms is proved by showing that only realistic
clock evolutions are allowed by the axioms.
4.1 Qualitative part
Let us assume that the formula ff is consistent and let us prove that it is
satisfiable. To simplify the presentation of the proof, we use the following
lemma:
Lemma 5 Every EventClockTL formula can be rewritten into an equivalent
formula of (using only the constant 1).
Proof. First by the use of the theorem . I OE . !I OE - . #I OE (44), every
formula . I OE with l(I) 6= 0 can be rewritten as a conjunction of formulae
with 0-bounded intervals. Using the axioms .-m+n OE $ .-m .-n OE (18) and
every interval can be decomposed into a nesting of
operators associated with intervals of length 1. \Xi
In the sequel, we assume that the formula ff for which we want to construct a
model is in EventClockTL 1 , as allowed by lemma 5.
We now define the set C(ff) of formulae associated with ff:
ffl Sub: the sub-formulae of ff.
ffl The formulae of Sub subject to a future real-time constraint:
Subg. We will say that a prediction clock is associated to these formulae.
ffl For these formulae, we will also track flOE when the next occurrence of OE is
left-open: this will simplify the notation. The information about OE will be
reconstructed by axiom (20). Rg.
ffl To select whether to track OE or flOE, we need the formulae giving the openness
of next interval:
ffl The formulae giving the current integer value of the clocks: I = f.!1 OE; . =1 OE;
Jg. Thanks to our initial transformation, we only have to
consider whether the integer value is below or above 1.
Among these, the "tick" formulae will be used in F to determine the fractional
parts of the clocks: Ig.
ffl We also define the mirror sets. For instance,
ffl The formulae giving the ordering of the fractional parts of the clocks, coded
by the ordering of the ticks:
g.
ffl The eventualities:
ffl The constant true ?, because -? will be used in lemma 14.
We close the union of all sets above under :; fl; - to obtain the closure of ff,
noted C(ff). This step preserves finiteness since we stop after adding just one of
each of these operators. Theorems (39), (38) show that further addition would
be semantically useless. For the past, we only have (6), (37). They also give
the same result, since we only have two possible cases: if -? is true, we can
move all negations outside and cancel them, except perhaps one. Otherwise,
we know that all -/ are false by (4). In each case, at most one - or fl and
one are needed. We use the notational convention to identify formulas with
their simplified form. For example, we write OE 2 C(ff) $ flOE 2 C(ff) to mean
is the simplification operator.
Note that although we are in the qualitative part, we need already include the
real-time formulae that will be used later. In this subsection they behave as
simple propositions.
A propositionally consistent structure
A set of formulae F ae C(ff) is complete w.r.t. C(ff) if for all formulae OE 2
C(ff), either OE 2 F or :OE 2 F ; it is propositionally consistent if (i) for all
We call such a set a propositional atom of C(ff).
We define our first structure, which is a finite graph,
the set of all propositional atoms of C(ff) and \Delta '   \Theta   is the transition
relation of the structure. \Delta is defined by considering two sub-relations:
represents the transition from a right-closed to a left-open interval;
represents the transition from a right-open to a left-closed interval.
propositional atoms. We define
The transition relation \Delta is the union of \Delta
or
Now we can define that the atom A is singular iff it contains a formula of the
symmetrically OE - OE.
Lemma 6 In the following, A and B are atoms:
(1) A is singular iff it is irreflexive (i.e.
(2) If A\Delta [ B, then A is not singular and (B is singular or
A is not singular and (B is singular or
singular, then there is at most one atom A such that
a unique C such that B \Delta ] C.
A is initial iff it contains : -?. It is then singular, since it contains ? -
?. A is monitored iff it contains ff, the formula of which we check floating
satisfiability.
Any atom A is exactly represented by the conjunction of the formulae that it
contains, written -
A. By propositional completeness, we have:
Lemma 7 ' W
A.
For any relation \Delta, we define the formula \Delta(A) to be W
B. The formula
B can be simplified to V
:flOE2A :OE, because in the propositional
structure, all other members of a B are allowed to vary freely and thus
cancel each other by the distribution rule.
Lemma
Proof.
Dually, W
B can be simplified to V
OE2A -OE. Therefore:
Lemma 9 ' -
Now let \Delta + be the transitive closure of \Delta. Since \Delta
Similarly,
Lemma
Using the disjunction rule for each reachable -
A, we obtain: '
(A). Now we can use the induction axiom
Using necessitation (33) and modus ponens (32), we obtain:
Lemma
An EventClockTL-consistent structure
We say that an atom A is EventClockTL-consistent if it is propositionally consistent
and consistent with the axioms and rules given in section 3. Now, we
consider the structure -
\Delta), where -
is the subset of propositional atoms
that are EventClockTL-consistent and -
\Lambdag.
Note that the lemmas above are still valid in the structure -
\Pi as only inconsistent
atoms are suppressed. We now investigate more deeply the properties
of the structure -
\Pi and show how we can prove from that structure that the
consistent formula ff is satisfiable.
We first have to define some notions.
ffl A maximal strongly connected substructure
(MSCS)\Omega is a non-empty set of
of the structure -
\Pi such that:
(1) for all
every atom can reach all atoms of \Omega\Gamma i.e.,
\Omega is strongly connected;
(2) for all
such that D 1
2\Omega then
i.e.,\Omega is maximal.
ffl A
MSCS\Omega is called initial if for all D 1
\DeltaD 2 and D 2
2\Omega then D 1 2 \Omega\Gamma i.e.
\Omega has no incoming edges.
ffl A
MSCS\Omega is called final if for all D 1
\DeltaD 2 and D 1
2\Omega then D 2 2 \Omega\Gamma
i.e.\Omega
has no outgoing edges.
ffl A
MSCS\Omega is called self-fulfilling if for every formula of the form OE 1 UOE 2 2 A
with A 2 \Omega\Gamma there exists B
2\Omega such that OE 2 2 B.
We now establish two properties of MSCS of our structure -
\Pi.
Every final
MSCS\Omega of the structure -
\Pi is self-fulfilling.
Proof. Let us make the hypothesis that there exists OE 1 UOE 2 2 A with A
2\Omega
and for all B 2 D, OE 2 62 B. By lemma 12 and as by hypothesis OE 2 62 B, for
theorem (46) and a propositional reasoning, we conclude
. Using the axiom (10) and the hypothesis that OE 1
we obtain ' -
by definition of \Sigma, we obtain ' -
contradiction with ' -
which is impossible since A is, by hypothesis,
consistent. \Xi
Lemma 14 Every non-empty initial
MSCS\Omega of the structure -
\Pi contains an
initial atom, i.e. there exists A
2\Omega such that -? 62 A.
Proof. By definition of initial MSCS, we know that for all D 1
\DeltaD 2 and D 2 2 \Omega\Gamma
then us make the hypothesis that for all A 2 \Omega\Gamma -? 2 A. By
the mirror of lemma 12 we conclude, by a propositional reasoning and the
hypothesis that -? 2 D for all D such that D -
contradicts axiom (12), so A 62 -
\Pi,
thus\Omega is empty. \Xi Actually such initial
MSCS are made of a single initial atom.
In the sequel, we concentrate on particular paths, called runs, of the structure
\Pi. A run of the structure -
\Delta) is a
is an infinite sequence of atoms and -
is an infinite sequence of intervals such that:
(1) Initiality: A 0 is an initial atom;
(2) Consecution: for every i - 0, A i
(3) Singularity: for every i - 0, if A i is a singular atom then I i is singular;
Alternation: I 0 I alternates between singular and open intervals,
i.e. for all i ? 0, I 2i is singular and I 2i+1 is open.
(5) Eventuality: the set fA n ; :::; A n+mg is a final MSCS.
Note that, for the moment, the timing information provided in -
I is purely
qualitative (singular or open); therefore any alternating sequence is adequate
at this qualitative stage. Later, we will construct a specific sequence satisfying
also the real-time constraints. In the sequel, given
I), ae(t) denotes the
atom A i such that t 2 I i .
Lemma 15 The transition relation -
\Delta of the structure -
\Pi is total, i.e. for all
atoms A 2 -
, there exists an atom
such that A -
\DeltaB.
Proof. We prove -
is consistent and can thus be completed to form an atom B. Assume it is not:
by definition
We can replace ? in (13), giving ' fl: -
\Phi.
By
\Phi. By (5), the set fflOEj fl OE 2 Ag [ ffl:OEj: fl OE 2 Ag is
inconsistent. Using (34) again, the set fflOEjflOE 2 Ag[f:flOEj:flOE 2 Ag ' A
is inconsistent, and thus A is inconsistent, contradicting A 2 -
. \Xi
Lemma 16 For every atom A of the structure -
\Pi, there is a run ae that passes
through A.
Proof.
(1) Initiality, i.e. every atom of -
\Pi is either initial or can be reached by an
initial atom. Let us consider an atom A, if A is initial then we are done,
otherwise, let us make the hypothesis that it can not be reached by an
initial atom, it means: for all B -
so by propositional
completeness -? 2 B. By lemma 12 and a propositional reasoning, we
Using axiom (12) we obtain a contradiction in A.
We use this path for the first part of the run.
(2) Consecution, by construction.
(3) Singularity: i.e., every odd atom is not singular. For the first and second
part of the run, we can obtain this by taking a simple path (thus without
self-loops). Since the first atom A 0 is initial, it is singular; from there on,
non-singular and singular states will alternate by lemma 6. For the final
repetition, this technique might not work when the MSCS is a single
atom. Then we know that this single atom is non-singular, and thus
Singularity is also verified.
Alternation: we can choose any alternating interval sequence, since the
timing information is irrelevant at this point.
Eventuality, i.e. every atom of -
\Pi can reach one of the final MSCS of -
\Pi.
It is a direct consequence of the fact that -
\Delta is total and the fact that -
is finite. We use this reaching path for the second part of the run, then
an infinite repetition of this final MSCS.
A run
I) of the structure -
\Pi has the qualitative Hintikka property if it
respects the semantics of the qualitative temporal operators which is expressed
by the following conditions (real-time operators will be treated in the following
H1 if A i is singular then I i is singular;
either I i is singular and there exists j ? i s.t. OE 2 2 A j and for all k s.t.
or I i is not singular and
(2) or there exists
either I i is singular and there exists and for all k s.t.
or I i is not singular and
(2) or there exists
We call such a run a qualitative Hintikka run. Next, we show properties of
some additional properties of runs related to the Hintikka properties above:
Lemma 17 For every run
I) of the structure -
\Pi, with -
for every i - 0 such that \SigmaOE 2 A
ffl either I i is singular and there exists
ffl or I i is non-singular and there exists j - i such that OE 2 A j .
Proof. First let us prove the following properties of the transition relation -
\Delta:
Recall that \SigmaOE j ?UOE,
and by definition of -
propositional reasoning, we obtain
that
definition
of -
the mirror of axiom (8) and a propositional reasoning, we obtain
By the two properties above, we have that if \SigmaOE 2 A i then either OE appears in
A j with j ? i if I i is singular (and thus right closed), j - i if I i is not singular
(and thus an open interval) or OE is never true and \SigmaOE propagates for the rest
of the run. But this last possibility is excluded by our definition of run: by
clause (5), every run eventually loops into a final (thus self-fulfilling by lemma
MSCS\Omega\Gamma Then either OE is realized before this looping or \SigmaOE
2\Omega and by
2\Omega and is thus eventually realized. \Xi
Lemma For every run
I) of the structure -
\Pi, for every position i
in the run if OE 1 UOE 2 2 A i then the right implication of property H2 is verified,
i.e:
ffl either A i is singular and there exists and for all k s.t.
ffl or A i is not singular and
(2) or there exists
Proof. By hypothesis we know that OE 1 UOE 2 2 A i and we first treat the case
where A i is singular.
ffl By the axiom (10) and lemma 17, we know that there exists j ? i such that
us make the hypothesis that A j is the first OE 2 -atom after A i .
ffl It remains us to show that: for all k s.t. We reason by
induction on the value of k.
Base case: By hypothesis we have OE 1 UOE 2 2 A i and also A i
(as A i is right closed) and thus for all flOE 2 A i ; OE 2 A i+1 by definition
of -
theorem (35) and axiom (5), and the fact that by hypothesis OE 2 62 A i+1 ,
(Prop) allows us to conclude that OE 1 2 A i+1 .
Induction case: induction hypothesis, we
know that OE 1 2 A k\Gamma1 and OE 1
as is the first position after i where OE 2 is verified).
To establish the result, we reason by cases :
I k is open and thus I k\Gamma1 is singular and right closed. We have A
and thus for all flOE 2 C(ff); flOE 2 A i by definition of
As OE 1 UOE 2 2 A k\Gamma1 by induction hypothesis and the axiom (7) we
conclude that OE 1 UOE 2 2 A k . Using the axiom (9), theorem (35), axiom
(5) and the fact that OE 2 62 A k , and (Prop), we conclude that OE 1 2 A k .
(2) I k is closed which implies that I k\Gamma1 is right open and A k\Gamma1
. By
definition of -
have that for all -OE 2 C(ff); -OE 2 A k
A
we have :OE 2 2 A k . Using those properties and the mirror of axiom
(8) we conclude that OE 1 - OE 1 UOE 2 2 A k .
We now have to treat the case where A i is not singular. By the axiom
and lemma 17 we know that there exists a later atom A j , i.e. j - i, such that
and we are done. Otherwise j ? i, and we must
prove that for all k s.t. this can be done by the reasoning
above. \Xi
We now prove the reverse, i.e. every time that OE 1 UOE 2 is verified in an atom
along the run then OE 1 UOE 2 appears in that atom. This lemma is not necessary
for qualitative completeness but we use this property in the lemmas over real-time
operators.
Lemma 19 For every run
I) of the structure -
\Pi, for every position
ffl either A i is singular and there exists and for all k s.t.
ffl or A i is not singular and
(2) or there exists
then
Proof. We reason by considering the three following mutually exclusive cases:
(1) A i is singular and there exists
We reason by induction to show that OE 1 UOE 2 2 A j \Gammal for all l s.t.
ffl Base case: l = 1. By hypothesis, we know that OE 2 2 A j . We now reason
by cases:
(a) if A j \Gamma1 is right closed then we have A j \Gamma1
by definition of
. Using the axiom (9) we deduce by (Prop) that
(b) if A j \Gamma1 is right open then we know that
by hypothesis) and thus OE 1 2 A j \Gamma1 . Also as A j \Gamma1
Using the mirror of axiom (8) and a propositional reasoning, we
by definition of -
ffl Induction case: 1 - l we have established the result
us show that we have the result for
A j \Gammal . First note that by hypothesis, OE 1 2 A j \Gamma(l\Gamma1) . We again reason by
cases:
(a) I j \Gammal is right closed. Then we have A j \Gammal
and by definition
of -
\Gammal and by axiom (7) we have that OE 1 UOE 2 2 A j \Gammal .
(b) A j \Gammal is right open. Then we have A j \Gammal -
and by definition
of -
\Gammal . We know
that by hypothesis, OE 1 2 A j \Gammal as singular and I j \Gammal
(by induction
hypothesis). Using the mirror of axiom (8) and a propositional
reasoning, we obtain -(OE 1 and by definition of -
that OE 1 UOE 2 2 A j \Gammal .
(2) A i is not singular and OE 2 2 A j . As A i is not singular, we have A i
definition of -
. By the axiom (9) and a proposition
reasoning, we obtain the desired result: OE 1 UOE 2 2 A i .
(3) A i is not singular, OE 2 62 A j , and there exists and for all
This case is treated by an inductive reasoning
similar to the first one above.
We have also the two corresponding mirror lemmas for the S-operator.
From the previous proved lemmas, it can be shown that the qualitative axioms
of section 3 are complete for the qualitative fragment of EventClockTL, i.e. the
logic LTR.
Lemma 20 A run ae has the Hintikka property for LTR formulae: for every
Proof. The Hintikka property was proved in the lemmas above, but expressed
without reference to time t. It remains to prove that this implies the usual
definition, by induction on formulae.
We must prove 9t 0 ?
from H2. Of course, we take t 0 somewhere in I j , so that t 0
can be divided in 3 parts: the part in I i , which is empty when I i
is singular, the part in some I k (i j), the part in I j . Each of them
(2) Conversely, the usual definition implies H2: First note that given t, if
ae(t) is not singular but I i is singular, it means that A
lemma 6. Thus we can merge I i ; I i+1 to ensure that I i is singular iff A i
is singular without loss of generality. Let j be the first index where OE 2 ,
I i is singular, or else j - i. We can take t 0 ? t in I j without loss
of generality. Since we need t 00 must
(H3) is symmetric. \Xi
Finally, we have the following theorem that expresses the completeness of the
qualitative axioms for the logic LTR:
Theorem 21 Every LTR formula that is consistent with the qualitative axioms
is satisfiable.
Proof. Let ff be a consistent LTR formula. We construct -
\Delta). Let
be an atom of the structure such that ff 2 -
. Such an atom B exists as
ff is consistent. By lemma 16, there exists a run
I) such that
for some i - 0. By lemma 20, we have (ae; t) thus ff is
We now turn to the completeness of real-time axioms.
4.2 Quantitative part
A run
I) of the structure -
\Pi has the timed Hintikka property if it
respects the Hintikka properties defined previously and the two following additional
properties:
H4 . I OE 2 ae(t) iff there exists t 0 2 t+I such that OE 2 ae(t 0 ) and
A run that respects those additional properties is called a well-timed run. In
the sequel, we will show that for each run of the structure -
\Pi, we can modify
its sequence of intervals, using a procedure, in such a way that the modified
run is well-timed.
Recall that given a tracked formula OE 2 R,
ffl . =1 OE is called its tick;
called its event (note that the second case need
not be considered thanks to the axioms (20),
ffl (OE -:OE) - (:OE - flOE) is called its reset.
The evolution of the real-time predicates is described by figure 2. We can now
see the status of this drawing:
Lemma 22 For any tracked formula OE 2 R, the projection of -
\Pi (restricted to
atoms containing the formulae COE) on OE; /!1 OE; / =1 OE; /?1 OE; \Sigma\GammaOE is contained in
figure 2.
Proof. It suffices to show that no further consistent atoms nor transitions can
be added to the figure.
ffl Atoms: from the axioms (15), (17), (14), (16).
ffl Transitions: We simply take all missing arrows of the figure, and show that
they cannot exist. As the proof is fairly long, we only show some excerpts.
(1) Assume that an atom A containing OE; / =1 OE is linked to an atom B containing
OE in this way: A -
B, by axioms (14),
(15), (16), we have : /!1 OE 2 B. Now by definition of -
and by (34), : fl /!1 OE 2 A. Now the main step: we use the mirror of
(23), negated on both sides. :fl? is impossible by (13), and thus we can
conclude contradicting OE 2 A.
(2) Now we show the only two transitions which are eliminated by the restriction
to COE. The first one is A -
contains /!1 OE; :OE; COE and
contains /!1 OE; OE. We prove using (9). In more detail, COE
abbreviates :OEU(OE -:OE). Applying (9) and unfolding U - , we obtain
using first disjunct is impossible,
by (5), (34), (38).
On the other hand, by definition of -
whence the contradiction

(3) The second transition eliminated is A -
contains /?1 OE; :OE; COE
and B contains /!1 OE; :OE. By definition of -
A. By axiom
(22), contradicting /?1 OE 2 A.
A constraint is a real-time formula of an atom A i . The begin of a constraint
is the index e at which its previous event, tick or reset occurred. The end of
a constraint is the index j at which its next event, tick or reset occurs. This
vocabulary refers to the order of time only: the begin is always before the
corresponding end, whether for history or prediction operators. Begins, ends,
ticks, resets, events are always singular. We say that (the history clock of) OE is
active between an event OE and the next reset of OE. It is small between its event
and the next tick or reset. After this, it is big. When it is big, it doesn't give
actual constraints, since it can stay big for any time, on one hand, and on the
other hand because it has passed first through a tick, which is forced to be 1
time unit apart from the event. Thus the monotonicity of time will ensure that
big constraints are indeed semantically true. We define the scope of a constraint
as the interval between the event and the next tick or reset, or equivalently
between its begin and its end. The same vocabulary applies symmetrically for
prediction operators. Actual constraints are either equalities (the time spend
in their scope must be 1), linking an event to a tick, or inequalities (the time
spend in their scope must be less than 1). An inequality is always linked to
a small clock. Constraints can be partially ordered by scope: it is enough to
solve constraints of maximal scope, as we shall see. A constraint of maximal
scope always owns indexes: they are found at the end of its scope. The scope
of an inequality extends from an event to a reset. Whether an atom A i is in
the scope of a constraint, and which, can be deduced from its contents. The
table below shows the contents of an atom A i that is the end of an equality.
We distinguish the prediction and history cases. The table is simplified by the
fact that we can assume that events are closed. The begin atom is the closest
one in the past to contain the indicated formulae.

Table
Equality constraints - ticking clocks
begin end in A i
. =1 OE (tick) OE; :OES . =1 OE (event)
The table below shows the contents of an atom A i indicating that the clock is
small. It is thus in the scope of a constraint, whose begin is before and whose
end is after. The begin (resp. end) is the closest atoms with the indicated
contents.

Table
Small clocks
begin in A i end
.
(tick or reset)
Note that the existence of the begin and ends is guaranteed by fig. 2: a clock
cannot stay small forever. In this section, we furthermore enforce that it will
not stay small more than 1 unit of time.
The proof shows that these constraints can be solved iff they are compatible
in the sense that the scope of an equality cannot be included in the scope
of an inequality, nor strictly in the scope of another equality. The axioms for
several clocks ensure this compatibility.
The previous section has built a run
I), where -
I is irrelevant, that
is qualitatively correct. From any such run
I), we now build a well-timed
run
J) by attributing a well-chosen sequence of intervals
to the atoms of the run, so as to satisfy the real-time
constraints.
Before, we introduce two lemmas on which the algorithm relies, that can also
be read from fig. 2:
Lemma 23 For every run
I) of the structure -
\Pi, we have that if
Proof. This lemma is a direct consequence of the mirrors of axioms (14) and
(17). \Xi
Lemma 24 For every run
I) of the structure -
\Pi, we have that if
-:/;/;:/S . =1 / 2 A i then there exists
Proof. This lemma is a direct consequence of the mirror of axiom (10). \Xi
The algorithm proceeds by induction along the run, attributing time points
As a consequence, an open interval (t attributed
when i is odd: we don't mention it, and just define t i for even i.
i.e. we attribute the interval [0; 0] to the initial atom A 0 .
(2) Induction: we identify and solve the tightest constraint containing i. We
define b as the begin of this tightest constraint, by cases:
(a) equality constraints:
(i) If there is an / =1 / 2 A i there has been a last (singular) atom
A b containing / before at time t b .
(ii) Else, if -:/;/;:/S . =1 / 2 A i there has been a last atom A b
containing . =1 / before A i , at time t b .
We set t
(b) If there are no equality constraints, we consider inequality constraints:
(i) We compute the earliest begin b of the small clocks using table 2.
t i has to be between t i\Gamma2 and t b + 1. We choose t
1)=2.
(ii) Otherwise, we attribute (say) t i\Gamma2 + 1=2 to A i .
The algorithm selects arbitrarily an equality constraint, but is still deterministic

Lemma 25 If two equality constraints have the same end i, their begins
are identical.
Proof. Four combinations of equality constraints are possible:
(1) The first constraint is / =1 OE
(a) The second constraint is / =1 /: A i contains thus /-1 / by (14). We
apply (26) to obtain :OES/.
We repeat this with /; OE inverted to obtain :/SOE. These formulae
imply by the mirror of Lemma 19 that / cannot occur before OE, and
conversely, thus they occur in the same atom.
(b) The second constraint is the event /; :-/ with :/S . =1 /: then A i
contains /-1 OE by (14). We apply (29) to obtain : . =1 /SOE.
Since A i contains :/U - / =1 OE since its eventuality / =1 OE is true
now. We apply (28) to obtain :OEZ(.
we know that the tick occurs first (perhaps ex-aequo) among the
possibilities that end the Z.
These formulae imply by Lemma 19 that . =1 / cannot occur before
OE, and conversely, thus they occur in the same atom.
(2) The first constraint is the event OE with :OES . =1 OE 2 A
(a) The second constraint is / This case is simply the previous
one, with OE; / inverted.
(b) The second constraint is the event / with :/S . =1 /: A i contains
since its eventuality OE is true now. We apply (27) to obtain
By :/S . =1 /, the tick . =1 / occurred first.
We repeat this with /; OE inverted. These formulae imply by Lemma 19
that . =1 / cannot occur before . =1 OE, and conversely, thus they occur
in the same atom.
Solving an equation at its end also solves current partial inequations:
Lemma 26 If A i is in the scope of an inequation, and the end of an equation,
then the begin A j of the inequation is after the begin A b of the equation (b ! j).
Proof. There are 3 possible forms of inequations in A i (see table 4.2):
its begin, i.e. =1 / 2 A j . We must show that b ! j. The
equation can be:
(a)
thus . The first case
is true as by hypothesis :/S must occur before /
in the past), and gives b - j.
(b) OE; :OES . =1 OE 2 A i and . =1 OE 2 A b :
using (27), we obtain : . =1 OEZ(. . The first case is true,
by hypothesis, and gives b - j.
We cannot assume because the mirror of lemma 25 then gives
its begin (its event), i.e. / 2 A j . We must show that b ! j.
The equation can be:
(a)
We apply (26) to obtain :OES/, meaning by the mirror of lemma 19
that b - j. :/SOE 62 A i , for otherwise we apply (30) yielding /!1 OE 2
contradicting / =1 OE 2 A i by (15), so we conclude b ! j.
(b) OE; :OES . =1 OE 2 A i and . =1 OE 2 A b :
by j. We cannot have the reverse
:/S . =1 OE, for otherwise we apply the mirror of (31) and deduce
its begin (a reset). Either .!1 / 2 A i already, or if the
event is in A i , we use axiom (23) to show . Since there is no
intervening / between j and i, the fig.2 implies .!1 / 2 A j+1 and thus
Because :(:/S . =1 /) 2 A i , we deduce .!1 / 2 A j .
Now, we must show that b ! j. The equation can be:
(a) / =1 OE 2 A i and its event OE 2 A b :
As apply (28) to obtain :OEZ(.
means b - j. Again because there are no intervening / between j
and i, using lemma 19 we have :/U / =1 OE 2 A j . Using the mirror
of (31), /!1 OE; :OE 2 A j , thus is impossible, since :OE 2 A j and
. We conclude b ! j.
(b) OE; :OES . =1 OE 2 A i and . =1 OE 2 A b :
so :/U - OE 2 A i , and we use (27) to obtain : . =1 OEZ(.
A i . The reset / occurs strictly before the tick, so the first case is
using
because there are no intervening / between positions j and i, we
have :/U / =1 OE 2 A j . Using the mirror of (30), .!1 OE 2 A j . The
second case is thus true, and means b - j. impossible, since
. We conclude b ! j.
We now show that the algorithm Attr assigns time bounds of intervals that
are increasing.
Lemma 27 The sequence t i built by Attr is increasing.
Proof. In the notation of the definition, this amounts to prove t
when b is defined, since t i is either (in the case of an equality) or the
middle point of (in the case of an inequality). If b is not defined
(no constraints) then it is trivially verified as we attribute t i\Gamma2 + 1=2 to t i . We
prove the non trivial cases by induction on i:
(1) base case: 2. Either:
(a) no constraint is active, b is undefined;
just have to prove 0 ! 1.
(2) induction: We divide in cases according to the constraint selected at
whose begin is called
(a) an equality: by lemmas 25, 26, its begin was before, i.e., b i\Gamma2 ! b.
By inductive hypothesis, t i is increasing: t b i\Gamma2 ! t b . Thus t
(b) an inequality: Thus the begin b i\Gamma2 - b i , since it was obtained by
sorting. By inductive hypothesis, t i is increasing: so t b i\Gamma2
. By
inductive hypothesis, t
+1. Thus t
Furthermore, the algorithm Attr ensures that time increases beyond any bounds:
Lemma 28 The sequence of intervals -
J of
J) built by our
algorithm has finite variability: for all t there exists an i - 0 such that
Proof. Although there is no lower bound on the duration of an interval, we
show that the time spend in each passage through the final cycle of -
is at least 1=2. Thus any real number t will be
reached before index 2tc, where c is the number of atoms in the final cycle.
We divide in cases:
(1) If the cycle A n A contains an atom which is not in the scope
of any constraint, the time spent there will be 1=2.
(2) Else, the cycle contains constraints, and thus constraints of maximal
scope. This scope, however, cannot be greater than one cycle. Let e the
end of such a constraint. Thus e is in the scope of no other constraint
with an earlier begin.
The time spent in the scope of the constraint until i is at least 1=2:
Let again b be the begin of the scope of the constraint. t e\Gamma2 - t b (since
the begin and end are singular and distinct), thus our algorithm gives
1=2. Since the scope cannot be greater than
one cycle, the time spent in a cycle is at least 1=2.
This procedure correctly solves all constraints:
Lemma 29 The interval attribution Attr transforms any run ae in a well-timed
run Attr(ae).
Proof. We show the two supplementary properties of a well-timed run:
We must show that the next / occurs in t \Gamma I. / I /
can be:
(a) /?1 /: These constraints are automatically satisfied because:
(i) the mirror of the eventuality rule (17) guarantees / has occurred.
us take the first such j, which is the
corresponding event.
(ii) According to fig.2, / will stay false, and eventually we will reach
(iii) the axiom (25) guarantees that satisfying the equality will entail
satisfying the greater-than constraint, since they refer to the
same tracked event, and since the equality is later. In formulae,
for any t i 2 I i ,
(b) / =1 /: Since this is an equality constraint, the algorithm Attr must
have chosen an equality constraint with begin b. Thus t 1. By
lemma 25, the begin event OE is also in A b .
(c) /!1 /: If i isn't even (singular), we know that the constraint will still
be active in the next atom because the end of a constraint is
always singular. By (22):
ffl It might become an equality (the clock may tick), in which case
it is treated as in the previous case (with i+1 instead of i). Then
the monotonicity of time will ensure that I
ffl If it is still the same inequality, it is treated below (with
instead of i). Then the monotonicity of time will ensure that
I
Thus at this point we can assume that i is even. Let j ! i be the
begin of the constraint, OE 2 A j . The constraint selected by Attr at i
can be:
(i) an equality: by lemma 26, its begin b ! j, so that t
(ii) or the constraint chosen in A i is an inequality. The pair /!1 / 2
is also an inequality in A i : let f be its begin. The
algorithm has selected the constraint with the earliest begin b.
(2) Let . I / 2 Very similarly, we must show that the next / occurs
I / can be:
(a) .?1 /: These constraints are automatically satisfied because:
(i) the eventuality rule (17) guarantees / will occur: 9j ? i
A j . We take the first such j, which is the corresponding event.
We can assume it is singular.

Figure

2 guarantees that there is first a tick: 9k
(iii) the reset rule (25) guarantees that satisfying the equality will
entail satisfying the greater-than constraint, since they refer to
the same end event, and since the equality is later. In formulae,
for any t i 2 I i ,
(b) . =1 /: let A j contain the next event of /. Since this is an equality con-
straint, the algorithm Attr must have chosen an equality constraint
at A j . By lemma 25, its begin is i. Thus t
(c) .!1 /: Let A j contain the next event of /. The constraint selected by
Attr at j can be:
(i) an equality: by lemma 26 its begin b ! i, so that t
(ii) or the constraint chosen in A j is an inequality. The pair .!1 / 2
is also an inequality in A j : let f be its begin. The
algorithm has selected the constraint with the earliest begin b.
The reader now expects a proof for the converse implication. This is not needed
thanks to (43). \Xi
As a consequence of the last lemmas, we have:
Lemma timed run built by Attr has the Hintikka property for Event-
Finally, we obtain the desired theorem:
Theorem 31 Every EventClockTL-consistent formula is satisfiable.
Proof. If ff is a EventClockTL-consistent formula then there exists an ff-monitored
atom A ff in -
\Pi. By lemma 16, there exists a set of runs \Sigma that pass through
A ff and by the properties of the procedure Attr, lemma 18, lemma 28 and
lemma 29, at least one run ( -
has the Hintikka property for Event-
ClockTL. It is direct to see that ( -
I) is a model for ff at time t 2 I ff (the
interval of time associated to A ff in ( -
I) ) and thus ff is satisfiable. \Xi
Corollary 32 The rule (1) and axioms (2)-(31) form a complete axiomatization
of EventClockTL.
4.3 Comparison with automata construction
In spirit, the procedure given above can be considered as building an automaton
corresponding to a formula. The known procedures [3] for deciding
use a similar construction, first building a timed automaton
and then its region automaton. We could not use this construction directly
here, because it involves features of automata that have no counterpart in the
logic, and thus could not be expressed by axioms. However, the main ideas are
similar. The region automaton will record the integer value of each clock: we
code this by formulae of the form .!1 . =1 ::: . =1 OE. It will also record the ordering
of the fractional parts of the clocks: this is coded here by formulae of the
form :. =1 :::. =1 OEU. =1 :::. =1 /. There are some small differences, however. For
simplicity we maintain more information than needed. For instance we record
the ordering of any two ticks, even if these ticks are not linked to the current
value of the clock. This relationship is only inverted for a very special case:
when a clock has no previous and no following tick, we need not and cannot
maintain its fractional information. It is easy to build a more careful and more
efficient tableau procedure, that only records the needed information.
The structure of atoms constructed here treats the eventualities in a different
spirit than automata: here, there may be invalid paths in the graph of atoms.
It is immediate to add acceptance conditions to eliminate them and obtain a
more classical automaton. But it is less obvious to design a class of automata
that is as expressive as the logic: this is done in [14].
4.4 Other time domains
As we have already indicated incidentally, our proofs are written to adapt to
other time domains Twith minimal change. We only consider totally ordered
dense time, however. For instance, we could use as time domain:
(1) The real numbers, T= R: We replace (12) by the mirror of (13).
(2) The rational numbers, T= Q: If we force the bounds of an interval to
be rational as well, nothing has to be changed. Otherwise, a transition
from an open interval to an open interval is now possible, if the common
bound is irrational. This defeats the induction axiom (11). We postpone
the study of this case to a further paper, but the basic ideas of the proof
still apply.
(3) A bounded real interval:
(a) closed For the qualitative part, we replace (13) by the
mirror of (12). For the quantitative part, we first remove the axiom
(25). If the duration of the interval
stating that the beginning is at distance d from the end. Otherwise,
we add the best approximation of this:
(b) open For the qualitative part, we replace (13) by the
mirror of (12): from a qualitative point of view, an open interval is
indistinguishable from an infinite one.
5 Translating MetricIntervalTL into EventClockTL
The logics have been designed from a different philosophical standpoint: MetricIn-
restricts the undecidable logic MetricTL by "relaxing punctuality",
i.e., forbidding to look at exact time values; EventClockTL, in contrast, forbids
to look past the next event in the future. However, we have shown in [14] that,
surprisingly, they have the same expressive power. The power given by nesting
connectives allows to each logic to do some of its forbidden work. Here, we
need more than a mere proof of expressiveness, we need a finite number of
axioms expressing the translation between formulae of the two logics. We give
below both the axioms and a procedure that use them to provide a proof of
the equivalence.
First, we suppress intervals containing 0:
U I /
U J /) with
Then we replace bounded untils -
U I with 0 62 I by simpler \Sigma I , provided
U I /
where l is the left endpoint of I, the intervals
Ig.
We suppress classical until using:
For infinite intervals, we reduce the lower bound l ? 0 to 0 using
For finite intervals with left bound equal to 0, we exclude it if needed with
(49), and we use the . operator:
Note that the formulae .!u OE and .-u OE can be reduced to formulae that only
use constant 1 using the axioms (18) and (19).
When the left bound of the interval is different from 0 and the right bound
different from 1, we reduce the length of the interval to 1 using:
Then we use the following rules recursively until the lower bound is reduced
to 0:
In this way, any MetricIntervalTL formula can be translated into a Event-
formula where bounds are always 0 or 1. Actually, we used a very
small part of EventClockTL; we can further eliminate .!1 OE:
showing that the very basic operators . have the same expressive power
as full MetricIntervalTL.
The converse translation is much simpler:
. I OE $ :\Sigma !I OE - \Sigma Inf0g OE (62)
OEU/
5.1 Axiomatization of MetricIntervalTL
To obtain an axiom system for MetricIntervalTL, we simply translate the axioms
of EventClockTL and add axioms expressing the translation.
Indeed, we have translations in each direction:
Therefore, to prove a MetricIntervalTL formula -, we translate it into Event-
and prove it there using the procedure of section 4. The proof - can
be translated back to MetricIntervalTL in T (-) proving T (S(-)). Indeed, each
step is a replacement, and replacements are invariant under syntax-directed
translation preserving equivalence:
To finish the proof we only have to add T (S(-))
- . Actually the translation axioms
above are stronger, stating T (S(-. In our case, T (defined by (62), (63))
is so simple that it can be considered as a mere shorthand. Thus the axioms
(1)-(29) and (49)-(60) form a complete axiomatization of MetricIntervalTL,
with . I ; U now understood as shorthands.
Theorem 33 The rule (1), axioms (2)-(29), and axioms (49)-(60) form a
complete axiomatization of MetricIntervalTL.
6 Conclusion
The specification of real-time systems using dense time is natural, and has
many semantical advantages, but discrete-time techniques (here proof techniques
[8,18]) have to be generalized. The model-checking and decision techniques
have been generalized in [2,3]. Unfortunately, the technique of [3] uses a
translation to automata which are more powerful and complex than temporal
logic, and thus is not suitable for building a completeness proof.
This paper provides complete axiom systems and proof-building procedures
for linear real time, extending the technique of [19]. This procedure can be
used to automate the proof construction of propositional fragments of a larger
first-order proof.
Some possible extensions of this work are:
ffl The proof rules are admittedly cumbersome, since they exactly reflect the
layered structure of the proof: for instance, real-time axioms are clearly separated
from the qualitative axioms. More intuitive rules can be devised if we
this constraint. This paper provides an easy way to show their com-
pleteness: it is enough to prove the axioms of this paper. This also explains
why we have not generalized the axioms, even when obvious generalizations
are possible: we prefer to stick to the axioms needed in the proof, to facilitate
a later completeness proof using this technique.
ffl The logics used in this paper assume that concrete values are given for real-time
constraints. As demonstrated in the HyTech checker [13], it is often
useful to mention parameters instead (symbolic constants), and derive the
needed constraints on the parameters, instead of a simple yes/no answer.
ffl The extension of the results of this paper to first-order variants of MetricIn-
should be explored. However, completeness is often lost in first-order
variants [23].
ffl The development of programs from specifications should be supported: the
automaton produced by the proposed technique might be helpful as a program
skeleton in the style of [24].



--R

the existence of refinement mappings.
Model checking in dense real time.
the benefits of relaxing punctuality.
A really temporal logic.
Logics and models of real time: a survey.
A really abstract concurrent model and its temporal logic.
Basic tense logic.
Automatic verification of finite-state concurrent systems using temporal-logic specifications
An axiomatization of the temporal logic with Until and Since over the real numbers.
Semantics and completeness of duration calculus.


the next generation.
the regular real-time languages
Tense Logic and the Theory of Order.
A complete proof systems for QPTL.
Specifying message passing and time-critical systems with temporal logic
Checking that finite-state concurrent programs satisfy their linear specification
the glory of the past.
the anchored version of the temporal framework.
Temporal Logic of Real-time Systems
State clock logic: a decidable real-time logic
Incompleteness of first-order temporal logic with until
Synthesis of Communicating Processes from Temporal-Logic Specifications
--TR
Automatic verification of finite-state concurrent systems using temporal logic specifications
Incompleteness of first-order temporal logic with until
Temporal logic for real time systems
Half-order modal logic: how to prove real-time properties
The existence of refinement mappings
Model-checking in dense real-time
The benefits of relaxing punctuality
Checking that finite state concurrent programs satisfy their linear specification
A really abstract concurrent model and its temporal logic
Specifying Message Passing and Time-Critical Systems with Temporal Logic
The Regular Real-Time Languages
State Clock Logic
The Glory of the Past
The anchored version of the temporal framework
Logics and Models of Real Time
Semantics and Completeness of Duration Calculus
A Complete Proof Systems for QPTL
HYTECH
Synthesis of communicating processes from temporal logic specifications

--CTR
Carsten Lutz , Dirk Walther , Frank Wolter, Quantitative temporal logics over the reals: PSpace and below, Information and Computation, v.205 n.1, p.99-123, January, 2007
axiomatization;completeness;real time;temporal logic