A really temporal logic.
We introduce a temporal logic for the specification of real-time systems. Our logic, TPTL, employs a novel quantifier construct for referencing time: the freeze quantifier binds a variable to the time of the local temporal context. TPTL is both a natural language for specification and a suitable formalism for verification. We present a tableau-based decision procedure and a model-checking algorithm for TPTL. Several generalizations of TPTL are shown to be highly undecidable.
Introduction
Linear temporal logic is a widely accepted language for specifying properties of reactive systems
and their behavior over time [Pnu77, OL82, MP92]. The tableau-based satisfiability algorithm
for its propositional version, PTL, forms the basis for the automatic verification and synthesis of
finite-state systems [LP84, MW84].
PTL is interpreted over models that abstract away from the actual times at which events
occur, retaining only temporal ordering information about the states of a system. The analysis
of systems with hard real-time requirements, such as bounded response time, calls, however, for
the development of formalisms with explicit time. Several attempts have been made to introduce
time explicitly in PTL, and to interpret it over models that associate a time with every system
state [BH81, PH88, Koy90, Ost90]. While these logics allow the specification of typical real-time
requirements, most of the important decidability and complexity questions have not been answered.
In particular, it has not been understood which timing constraints may be permitted in PTL
without sacrificing the decidability of the verification problem.
Our objective is the development of a real-time extension of PTL that admits a generalization
of the PTL-based tools for algorithmic verification. To begin with, a notational extension of PTL
must be capable of relating the times of different system states. One commonly proposed method
This research was supported in part by an IBM graduate fellowship to the second author, by the National Science
Foundation under grants CCR-8812595 and CCR-9200794, by the Defense Advanced Research Projects Agency under
contract N00039-84-C-0211, and by the United States Air Force Office of Scientific Research under contracts AFOSR-
88-0281 and F49620-93-1-0056.
y A preliminary version of this paper appeared in the Proceedings of the 30th IEEE Symposium on Foundations
of Computer Science (FOCS 1989), pp. 164-169, and an extended version appeared in The Journal of the ACM 41,
1994, pp. 181-204.
employs first-order temporal logic, with one of the state variables representing time [PH88, Ost90,
LA92]. We claim that the unconstrained quantification of time variables allowed by this approach
does not restrict the user to reasonable and readable specifications.
Instead, we propose a novel, restricted, form of quantification - we call it freeze quantification
- in which every variable is bound to the time of a particular state. Freeze quantification identifies,
so we argue, precisely the subclass of "intended" specifications, and it leads to a concise and readable
notation. For instance, the typical time-bounded response requirement that every request p is
followed by a response q within can be asserted by the formula
(read "whenever there is a request p, and the variable x is frozen to the current time, the request
is followed by a response q, at time y, such that y is at most x
Secondly, we need to identify how expressive a theory of time may be added, in this fashion,
to PTL without sacrificing its elementary complexity. Our main results are twofold: we develop a
near-optimal decision procedure and a model-checking algorithm for real-time PTL by restricting
both the syntax of the timing constraints and the precision of the time model, and we show that
these restrictions cannot be relaxed without losing decidability. In particular, adding to PTL
the theory of the natural numbers with successor, ordering, and congruence operations, yields
the EXPSPACE-complete real-time temporal logic TPTL. The tableau method for PTL can be
generalized to TPTL. However, allowing either addition over time or a dense time domain results
in highly undecidable (\Pi 1
logics.
Thus we lay out a theoretical basis for the automatic verification of finite-state real-time systems
and, simultaneously, identify a boundary between the decidability and undecidability of finite-state
formalisms with explicit time.
Alternative approaches to the automatic verification of real-time systems using temporal logic
include work on the branching-time logic RTCTL [EMSS89] and the explicit-clock logic XCTL
[HLP90]. RTCTL makes the simplifying assumption of modeling synchronous real-time systems,
all of whose events occur with the ticks of a global clock. In the case of XCTL, all formulas are
quantifier-free and their variables are implicitly universally quantified, which makes it difficult to
compose requirements, like asserting that an implementation implies a specification. We will find
both restrictions unnecessary.
Since an earlier version of this paper was published [AH89], many new results concerning real-time
temporal logics have been obtained [ACD90, AH90, AFH91, WME92]. We point to [Hen90]
for a complete axiomatization of TPTL and to [AH92] for a survey of recent results.
Timed Temporal Logic
We define Timed Propositional Temporal Logic, TPTL, and demonstrate its adequacy as a real-time
specification language.
2.1 Timed state sequences
The formulas of TPTL are interpreted over timed state sequences. Let P be a set of proposition
let N be the set of nonnegative integers. A state is an interpretation for
the propositions in P . A timed state sequence is an infinite sequence of states, each of which is
labeled with a time from the discrete time domain
(Timed state sequence) A state sequence oe is an infinite sequence
of states oe is an infinite sequence of times - i 2 T,
0, such that
Monotonicity
Progress for all t 2 T there is some i - 0 such that - i ? t.
A timed state sequence ae = (oe; -) is a pair consisting of a state sequence oe and a time sequence - .
By oe i [- i ] we denote the state [time] sequence that results from the state sequence oe [time
sequence - ] by deleting the first i elements. We let ae use the convention that
At this point, a few words about our model of time are in order. Time is discrete but not a
state counter; rather, the time between successive states of a timed state sequence may remain
the same, or it may increase by an arbitrary amount. While a state counter would suffice to
model synchronous real-time systems, the events of asynchronous processes take place in a dense
time domain. Reasoning about dense time, on the other hand, may be prohibitively difficult (see
Section 4). As a compromise, the fictitious-clock (or digital-clock) assumption for real-time systems
has enjoyed increasing popularity [AH92, HMP92]: the true, dense times of events are recorded with
the finite precision of a discrete clock. Our definition of timed state sequences is chosen sufficiently
general to accommodate the fictitious-clock assumption (states between successive clock ticks can
be labeled with identical times).
2.2 Syntax and semantics of TPTL
We are given an infinite supply V of variables (x; :). The formulas of TPTL are built from
proposition symbols and timing constraints by boolean connectives, temporal operators, and freeze
quantifiers.
of TPTL) The terms - and formulas OE of TPTL are inductively defined
as follows:
for constants c; d 2 N, d 6= 0.
The timing constraints. The timing constraints of TPTL are of the form - 1 - 2 and
is congruent to time - 2 modulo the constant d"). The abbreviations x (for
are defined as usual. If each term of a formula OE contains
a variable, we say that OE contains no absolute time references. On the other hand, each term of
a formula may contain at most one variable. While from a logical point of view, this restriction
confines TPTL to the successor operation on time, we do not define terms using a unary successor
rather, for determining the length of a formula, we assume that all constants are given in
a reasonably succinct (e.g., binary) encoding. The size of a formula will be important for locating
the computational complexity of problems whose input includes formulas of TPTL.
The temporal operators. TPTL is based on the two temporal operators of PTL [GPSS80].
The next formula flp asserts about a timed state sequence that the second state in the sequence
satisfies the proposition p. The until formula p U q asserts about a timed state sequence that there
is a state satisfying the proposition q, and all states before this q-state satisfy the proposition p.
Additional temporal operators are defined as usual. In particular, the eventually operator 3OE
stands for true U OE, and the always operator 2OE stands for :3:OE.
The freeze quantifier. A variable x can be bound by a freeze quantifier "x:", which "freezes"
x to the time of the local temporal context. Let OE(x) be a formula in which the variable x occurs
freely. Then x: OE(x) asserts about the timed state sequence ae = (oe; -) that OE(- 0 ) is satisfied by ae,
where the formula OE(- 0 ) is obtained from OE(x) by replacing all free occurrences of the variable x
with the constant - 0 . For example, in the formula
the variable x is bound to the time of a state in which the proposition p is "eventually" satisfied;
it asserts that p is satisfied in some state before time 10. Similarly, the formula
asserts that whenever the proposition p is satisfied in a state, then the time is at most 10 (i.e., p is
not satisfied after time 10).
This intuition is captured formally by the following definition.
Definition 3 (Semantics of TPTL) Let ae = (oe; -) be a timed state sequence and let
be an interpretation (environment) for the variables. The pair (ae; E) satisfies the TPTL-formula
where the satisfaction relation j= is inductively defined as follows:
ae
ae
ae
ae
ae
ae
ae
ae
Here E(x denotes the environment that agrees
with the environment E on all variables except x, and maps x to t 2 T.
A TPTL-formula is closed if every occurrence of a variable x is within the scope of a freeze
quantifier "x:". We shall henceforth consider only closed formulas of TPTL.
The truth value of a closed formula is completely determined by a timed state sequence alone.
The timed state sequence ae is a model of the (closed) TPTL-formula OE, denoted by ae if the
E) satisfies OE for any environment E . The formula OE is satisfiable [valid
[every] timed state sequence ae. Two formulas are equivalent if they have the same models.
2.3 TPTL as a specification language
We compare TPTL to alternative extensions of PTL with explicit time references. In particular,
we show that freeze quantification can be viewed as a constrained form of classical (i.e., universal
and existential) quantification.
versus first-order temporal logic
The freeze quantifier allows us to relate the times of different states. A typical real-time requirement
for a reactive system is that a multi-valued switch must be turned from position p to position q
In TPTL this condition can be expressed by the formula
Using standard first-order temporal logic with a state variable now that assumes the value of
the current time in every state, we may attempt to write the condition (1) as
or, in closer resemblance to the TPTL-formula (1),
The meaning of these formulas (i.e., their truth values over timed state sequences) depends on the
interpretation of the variables x and y. The explicit quantification of variables, however, is typically
omitted from first-order temporal specifications [PH88, Ost90]. Moreover, specification languages
are often restricted to formulas with implicit or explicit quantifier prefixes [Har88, HLP90].
The condition (2) is an example that the choice of quantifiers that provides the intended meaning
may not be obvious and, indeed, may not correspond to any prefix. In particular, the following
quantification of (2) yields a formula that is equivalent to (1):
(to be precise, a timed state sequence ae and an environment E satisfy the formula 9x: OE iff ae
OE for some t 2 T).
On the other hand, no quantifier prefix makes the formula (2) equivalent to (1). For example,
(1) does not imply the stronger condition
The difference is subtle: while the formula (1) asserts that every p-state of time x is followed by
p-states and, eventually, a q-state of time y demands more; that if there
is a p-state of time x, then there is a time y such that every p-state of time x is followed
by p-states and, eventually, a q-state of time y. For instance, the timed state sequence
(presented as a sequence of state-time pairs) satisfies (1) but not (4).
In general, TPTL identifies a fragment of the first-order temporal logic with the state variable
now . TPTL includes precisely those first-order temporal formulas in which each variable in V is,
immediately upon introduction, frozen to the time in the local temporal context (i.e., the value of
now the TPTL-formula x: OE is equivalent to the first-order temporal formula
or, equivalently, to the formula
In other words, TPTL restricts all time references to times of states, rather than permitting
quantification over the entire time domain. It is precisely this restriction that allows (and limits)
us to express timing constraints between states by concise and readable specifications (compare
(1) with (3)). It is also this restriction that leads to a generalization of the PTL-based tableau
algorithms for verification. While the tableau method for TPTL will be developed in Section 3,
the validity problem for TPTL with unconstrained classical quantification was recently shown to
be nonelementary [AH90].
versus bounded temporal operators
Several researchers have proposed to add an infinite supply of real-time modalities such as 3-ffi
("eventually within ffi time units") to PTL [PH88, Koy90] or branching-time logics [EMSS89].
These bounded temporal operators are definable in TPTL. For instance, the bounded-eventuality
operator 3-ffi OE can be expressed by the TPTL-formula
While bounded temporal operators always relate the times of adjacent temporal contexts, TPTL
admits constraints between distant contexts. For example, the formula
asserts that every p-state is followed by a q-state and, later, by an r-state, and the time difference
between the p-state and the corresponding r-state is at most 10.
For reasoning about synchronous real-time systems, "next state" can be identified with "next
time" and timing constraints may be expressed in PTL using the next operator. In this case,
bounded temporal operators are abbreviations for nested next formulas [EMSS89]. We can restrict
TPTL to the synchronous case by postulating
3 Timed Tableaux
We present a tableau-based decision procedure for TPTL. We then justify the doubly-exponential-
time cost of the decision procedure by showing that the validity problem for TPTL is EXPSPACE-
complete. Finally, we demonstrate how the tableau techniques can be applied to verify TPTL-
properties of real-time systems.
3.1 Decision procedure for TPTL
First we observe that to solve the validity problem for a formula, it suffices to check if its negation is
satisfiable. Throughout this subsection, we are given a formula OE of TPTL and wish to determine
if OE is satisfiable. The tableau method searches systematically for a model of OE. It originated with
the propositional calculus [Smu68] and was first applied to obtain a decision procedure for a modal
logic of computation in the case of dynamic logic [Pra80].
We follow the standard presentation of the tableau-based decision procedure for PTL [BMP81,
Wol83] and begin by constructing the initial tableau for OE. Checking the satisfiability of OE can then
be reduced to checking if the finite initial tableau for OE contains certain infinite paths. The tableau
method for PTL is, in fact, subsumed by our procedure as the special case in which OE contains no
timing constraints.
Preliminary assumptions
For the moment, we assume that
1. OE contains no absolute time references; that is, every term in OE contains a variable. Thus we
may perform simple arithmetic manipulations so that all timing constraints in OE are of the
nonnegative integers d ? c - 0.
2. OE contains only the temporal operators fl and 2; that is, the first argument of every occurrence
of the until operator U in OE is true .
While neither of the two restrictions is essential, they simplify the exposition of the decision pro-
cedure. Later we will accommodate both absolute time references and until operators. We also
assume that OE is of the form z: OE 0 ; this can be easily achieved, if necessary, by prefixing OE with any
variable z that does not occur freely in OE.
A timed state sequence ae = (oe; -) is \Delta-bounded, for a constant
that is, the time of the initial state of a \Delta-bounded timed state sequence is at most \Delta and
the time increases from a state to its successor state by no more than \Delta.
To begin with, we restrict ourselves to \Delta-bounded models for checking satisfiability. This case
has finite-state character: the times that are associated with states can be modeled by finitely many
(new) time-difference propositions Prev that represent in the initial state, the initial
time ffi , and in all other states, the time increase ffi from the predecessor state. Formally, we can
capture the (state and) time information in a timed state sequence ae = (oe; -) by a state sequence
oe with
for all i - 0. This reduction of timed state sequences to state sequences allows us to adopt the
tableau techniques for PTL. At the conclusion of this section we will show how we can find an
appropriate constant \Delta for the given formula OE.
Updating timing constraints
The key observation underlying the tableau method for PTL is that any formula can be split
into two conditions: a non-temporal ("present") requirement on the initial state and a temporal
("future") requirement on the rest of a model (i.e., the successor state). For example, the eventuality
3/ can be satisfied by either / or fl3/ being true in the initial state of a state sequence. Since
the number of conditions generated in this way is finite, checking for satisfiability is reducible to
checking for satisfiability in a finite structure, the initial tableau.
The splitting of TPTL-formulas into a present and a future (next-state) condition demands
more care; to obtain the requirement on the successor state, all timing constraints need to be
updated appropriately to account for the time increase ffi from the initial state to its successor.
Consider, for example, the formula x: 3y: /(x; y), and recall that the free occurrences of x in / are
references to the initial time. This eventuality can be satisfied either by having the initial state
satisfy y: /(y; y), with all free occurrences of x in / replaced by y, or by having the next state satisfy
the updated eventuality "x: 3y: naive replacement of x by
however, successively generate infinitely many new conditions. Fortunately, the monotonicity of
time can be exploited to keep the tableau finite; the observation that y is always instantiated, in
the "future," to a value greater than or equal to the initial time x, allows us to simplify timing
assertions of the form x x to true and false, respectively.
We define, therefore, the formula x: /(x) ffi that results from updating all references in / to the
initial time x by the time difference ffi. For instance, if x: / is the formula
then x: / 1 , x: / 5 , and x: / 6 are the following formulas:
In general, given a TPTL-formula x: / and ffi 2 N, the TPTL-formula x: / ffi is defined inductively
as follows:
results from x: / ffi by replacing every term of the form x
every subformula of the form x
and x j d y respectively, provided that the occurrence of x in the specified
terms and formulas is free in / ffi .
The following lemma confirms that this transformation has the intended effect and updates all
time references correctly; that is, the formula x: /(x) ffi expresses the condition "x:
be a timed state sequence, let E be an environment, and
Proof of Lemma 1 The proof proceeds by a straightforward induction on the structure of /.
Closure of a TPTL-formula
We collect all conditions that may arise by recursively splitting the formula OE into its present and
future parts in the closure of OE. It suffices to define the closure for formulas whose outermost symbol
is a freeze quantifier. The closure set Closure(z: OE 0 ) of the TPTL-formula z: OE 0 is the smallest set
of formulas containing z: OE 0 that is closed under the following operation Sub:
where the formula /[x := z] results from / by replacing all free occurrences of x with z. Note that
all formulas in a closure set are of the form z: /.
A constant c ? 0 occurs in the TPTL-formula OE if OE contains a subformula of the form
y, or OE contains the predicate symbol j c . Let C be the largest
constant that occurs in the formula OE. The closure set of OE is finite, because for all
all formulas z: / in Closure(OE), z: / ffi is z: / C .
The size of the closure set of OE depends on both the structure of OE and the constants that occur
in OE. We define k OE , the product of all constants that occur in the TPTL-formula OE, inductively as
follows:
, and k x:
Lemma 2 (Size of closure) Let be the number of boolean, temporal, and freeze operators in
the TPTL-formula OE, and let k be the product of all constants that occur in OE. Then jClosure(OE)j -
2nk.
Proof of Lemma 2 Given a formula z: OE 0 , we define, by induction on the structure of OE 0 , the set
of formulas that contains OE 0 and is closed under updating of timing constraints; the set C OE 0 is,
in addition, closed under subformulas:
Here set E of formulas; the other operators are applied to sets in an
analogous fashion. The case of formulas of the form x treated similarly to the timing
constraints x - y
Observe that D / ' C / . It is straightforward to show by induction on the structure of OE 0 that
(2) For all
OE 0 is closed under Sub.
From (1) and (3) it follows that Closure(z: OE 0
OE 0 . Thus, it suffices to show that jD OE
and jC OE 0 j - 2nk, which may again be done by induction on the structure of OE 0 .
Initial tableau of a TPTL-formula
Tableaux for TPTL are finite, directed state graphs (Kripke structures). Unlike the states of a
timed state sequence, which determine the truth values of all propositions, the vertices of a tableau
are labeled with arbitrary formulas of TPTL. The formulas that label a vertex of a tableau express
conditions on the annotated state and its successor states. In addition, every vertex is labeled with
a time-difference proposition Prev that denotes the time increase from the predecessor
states.
Formally, the vertices of a tableau for OE are the maximally consistent subsets of the finite
universe
Closure   \Deltag
of TPTL-formulas. A subset \Phi of Closure   (OE) is (maximally) consistent if it satisfies the following
conditions, where all formulas range only over the finite set Closure   (OE):
is in \Phi for precisely one is referred to as ffi \Phi .
c) is in \Phi iff 0 - c holds in N (for - being one of -, and j d ).
ffl z: false is not in \Phi.
is in \Phi iff either z: / 1 is not in \Phi or z: / 2 is in \Phi.
ffl z: 2/ is in \Phi iff both z: / and z: fl 2/ are in \Phi.
ffl z: x: / is in \Phi iff z: /[x := z] is in \Phi.
The initial tableau T (OE) for the TPTL-formula OE is a directed graph whose vertices are the
consistent subsets of Closure   (OE), and which contains an edge from \Phi to \Psi iff, for all formulas
z: fl / in Closure   (OE),
This definition ensures the global consistency of all temporal and real-time constraints in the
initial tableau. The significance of the (finite) initial tableau T (OE) for the formula OE is that every
model of OE corresponds to an infinite path through T (OE) along which all eventualities are satisfied
in time, and vice versa. This implies a finite-model property for TPTL, in the sense that every
satisfiable TPTL-formula OE is satisfied by a model whose state part, extended by the time-difference
propositions Prev ffi , is eventually periodic.
To be precise, an infinite path
through a tableau is a OE-path if it satisfies the following three conditions:
Initiality OE 2 \Phi 0 .
Fairness All eventualities are satisfied along \Phi in time or, equivalently, all missing invariances
are violated along \Phi in time; that is, for all z: 2/ 2 Closure   (OE) and i - 0,
Progress
Every OE-path in the initial tableau for OE can be reduced to a OE-path that is eventually periodic.
Moreover, the length of the period is bounded by the following lemma. This will prove to be
important for obtaining an upper bound on the complexity of TPTL.
Lemma 3 (Length of OE-paths) Suppose that the initial tableau T (OE) for the TPTL-formula OE
consists of m vertices. If T (OE) contains a OE-path, then it contains a OE-path of the form
for l - (2nk is the number of temporal operators in OE and k is the product of all
constants that occur in OE.
Proof of Lemma 3 Consider the infinite OE-path choose i to be the smallest
j such that \Phi j occurs infinitely often in \Phi. There are no more than nk invariances in Closure   (OE);
hence \Phi i lacks at most nk invariances z: 2/ l , each one of which is violated by some vertex \Psi l of
the infinite suffix \Phi i \Phi
be finite segments of \Phi that contain no other (i.e., inner) occurrences of \Phi i . Delete all
loops in every segment \Phi j , thus obtaining the finite sequences -
2nk, each of length at
most m+ 1. It is not hard to see that the result of deleting duplicated vertices (i.e., \Phi i ) from
is a OE-path of the desired form.
Tableau decision procedure
The following main lemma suggests a decision procedure for TPTL: to determine if the TPTL-
formula OE is satisfiable, construct the initial tableau T (OE) and check if it contains any OE-paths.
Lemma 4 (Initial tableau for TPTL)
(1) [Correctness] If the initial tableau T (OE) for the TPTL-formula OE contains a OE-path,
then OE is satisfiable.
(2) [Completeness] If OE has a \Delta-bounded model, then T (OE) contains a OE-path.
Proof of Lemma 4 The proof makes essential use of both directions of the time-step lemma,
Lemma 1. Let E be any environment.
(1) Given a OE-path through the initial tableau T (OE), define the timed state
sequence
. Note that
the time sequence - satisfies the progress condition because \Phi does. We show, by induction on the
structure of /, that / 2 \Phi i iff ae i
that ae is a model of OE.
For a proposition z: p 2 Closure   (OE), we have z: be one of -,
its negation. By the consistency of \Phi i , z: (z - z
This completes the base cases.
By the consistency of \Phi i , z: (/ . By the induction
hypothesis, this is the case iff either ae i 6j= z: / 1 or ae i
Now assume that z: fl/ 2 Closure   (OE) and let
. By the induction hypothesis, this is the case iff ae i+1 this is
the case iff ae i+1
For the case that z: 2/ 2 Closure   (OE), we first prove that z: 2/ 2 \Phi i iff z:
note that
by our choice of - .
We use induction on j to show that z: 2/ 2 \Phi i implies z: 2/
Suppose that z: 2/ for an arbitrary j - i. By the consistency of \Phi j , also
z: Invoking again the consistency of \Phi j ,
we conclude that z: /
On the other hand, suppose that z: 2/ 62 \Phi i . Since \Phi is a OE-path, there is some
By the induction hypothesis, it follows that z: 2/ 2 \Phi i iff ae j
this is the case iff ae j
Finally, consider the case that z: x: / 2 Closure   (OE). In this case, z: x: / 2 \Phi i iff z: /[x := z] 2
. By the induction hypothesis, this is the case iff ae i
be a \Delta-bounded model of OE. The subsets \Phi i , for i - 0, of Closure   (OE) are
defined as follows: Prev - i \Gamma- We show that
is a OE-path through the initial tableau T (OE).
By inspecting the consistency rules, it is evident that every \Phi i is (maximally) consistent. To
prove that \Phi is an infinite path through T (OE), we also have to show that there is an edge from \Phi i
to \Phi i+1 for all i - 0. Suppose that z: fl / 2 Closure   (OE) and let
this is the case iff ae i+1
the initial tableau for OE contains an edge from \Phi i to \Phi i+1 .
We now show that the infinite path \Phi is indeed a OE-path. It satisfies the progress condition
because the time sequence - does. To see that OE 2 \Phi 0 , observe that ae is a model of OE. It remains
to be established that all eventualities in \Phi are satisfied in time. Suppose that z: 2/ 2 Closure   (OE)
and z: 2/ 62 \Phi i ; that is, ae i
thus
. Then ae j 6j= z: / ffi by Lemma 1, which implies that z: / ffi 62 \Phi j .
After constructing the initial tableau T (OE) for the formula OE, we delete all vertices that are not
on a OE-path. This can be achieved by a straightforward modification of the standard techniques
for marking all vertices of a graph that lie on an infinite path along which all eventualities are
satisfied [Wol83]. The remaining state graph is called the final tableau for OE. It follows that a
TPTL-formula OE has a \Delta-bounded model iff its final tableau is not empty.
The procedure for finding the final tableau is polynomial in the size of the initial tableau, which
contains vertices, each of size O(nk), where is the number of operators in OE and
k is the product of all constants that occur in OE. Thus, provided that \Delta is dominated by 2 nk , the
initial T (OE) can be constructed and checked for OE-paths in deterministic time exponential in nk.
We show next that \Delta can indeed be bounded by k.
Bounding the time step-width
Given a formula OE, we finally determine the bound \Delta on the time increase between two successive
states such that the satisfiability of OE is not affected; that is, we choose the constant \Delta 2 N such
that OE is satisfiable iff it has a \Delta-bounded model.
Let c be the largest constant in OE that occurs in a subformula of the form x
y, and let j c 1
cm be all the congruence predicates that occur in OE. If the time
increase ffi between two states is greater than or equal to c, it obviously suffices to know the residues
of in order to update, in a tableau, all timing constraints correctly. Indeed, for
checking the satisfiability of OE, the arbitrary step-width ffi can be bounded by taking the smallest
representative for each of the finitely many congruence classes.
Lemma 5 (Bounded time increase) If the TPTL-formula OE is satisfiable and k is the product
of all constants that occur in OE, then OE has a k-bounded model.
Proof of Lemma 5 We can, in fact, derive the tighter bound c + k 0 - k, for the least common
multiple k 0 of all c i , 1 - i - m. Given a model ae = (oe; -) of OE, let the time sequence - 0 be such
that, for all
i to be the smallest
. It is easy to see that ae model of OE.
Combining this result with the tableau method developed above, we arrive at the conclusion
that the satisfiability of the TPTL-formula OE is decidable in deterministic time exponential in nk.
Moreover, Lemma 3 implies that every satisfiable formula OE is satisfiable in a model whose size is,
in the sense mentioned above, exponential in nk.
Remember that we have restricted OE to contain no until operators and no absolute time refer-
ences. We now show that both assumptions can be relaxed.
Until operators
First, let us address formulas that include until operators. We take the closure of a formula OE with
until operators to be closed under the operation
and add the following condition on the consistency of a set \Phi ' Closure   (OE) of formulas:
is in \Phi iff either z: / 2 is in \Phi, or both z: / 1 and z: fl (/ 1 U are in \Phi.
Finally, the fairness requirement on a OE-path \Phi 0 \Phi 1 is generalized to
for all i - 0. It is not hard to check that the Lemmas 2, 3, 4, and 5 allow the addition of until
operators in this way.
Absolute time references
Secondly, let us accommodate absolute time references. Instead of generalizing the tableau method
to constant terms, which contain no variable, we can use a simple observation. Suppose that we
test the formula OE for satisfiability. Let x be a variable that does not occur in OE and replace every
variable-free term c in OE with the term x+c, thus obtaining the new formula OE R (which may contain
free occurrences of x). The following lemma allows us to reduce the satisfiability problem for OE to
the satisfiability problem for the formula x: fl OE R , which contains no absolute time references.
Lemma 6 (Absolute time references) A TPTL-formula OE is satisfiable iff the formula x: flOE R
is satisfiable, where x does not occur in OE.
Proof of Lemma 6 (1) Let ae = (oe; -) be a timed state sequence. We define the timed state
sequence ae
then ae 0
be a timed state sequence. We define the timed state sequence ae
such that oe 0
Note that the transformation from OE to OE R does not increase the number of operators in OE nor
the product of all constants that occur in OE. The following theorem summarizes our results about
the tableau method.
Theorem 1 (Deciding TPTL) The validity problem for a (closed) TPTL-formula OE can be decided
in deterministic time exponential in nk, where is the number of boolean, temporal, and
freeze operators in OE, and k is the product of all constants that occur in OE.
Note that the length ' of any formula OE, whose constants are presented in a logarithmic (e.g.,
binary) encoding, is within constant factors of n log k. Thus we have a decision procedure
for TPTL that is doubly exponential in ' (although only singly exponential in n, the "untimed"
part and, therefore, singly exponential for PTL). The algorithm we have outlined can, of course,
be improved in many ways. In particular, we may avoid the construction of the entire initial
tableau by starting with the initial state, which contains OE, and successively adding new states only
when needed [Wol83]. This stepwise procedure, however, does not lower the doubly exponential
deterministic-time bound; as we will show in the following subsection, the decision problem for
TPTL is EXPSPACE-hard.
We also point out that while the monotonicity condition on timed state sequences is essential
for the tableau method to work, the progress condition on timed state sequences (and OE-paths) can
be omitted.
3.2 Complexity of TPTL
The following theorem establishes TPTL as being exponentially harder to decide than its untimed
base PTL, which has a PSPACE-complete decision problem [SC85]. The extra exponential is
caused by the succinct representation of time constants in TPTL and is typical for many real-time
specification languages [AH90].
Theorem 2 (Complexity of TPTL) The validity problem for TPTL is EXP-SPACE-complete
(with respect to polynomial-time reduction).
Proof of Theorem 2 The proof proceeds in two parts; we first show that TPTL is in EXPSPACE,
and then that it is EXPSPACE-hard. The first part follows the argument that PTL is in PSPACE,
which builds on a nondeterministic version of the tableau-based decision procedure [Wol83]; the
hardness part is patterned after a proof that the universality problem of regular expressions with
exponentiation is EXPSPACE-hard [HU79].
It suffices to show that the complementary problem of checking the satisfiability
of a TPTL-formula is in nondeterministic EXPSPACE and, hence, by Savitch's theorem, in
(deterministic) EXPSPACE.
In particular, it can be checked in nondeterministic singly exponential space if the initial tableau
contains a OE-path of the form stated in Lemma 3. In trying to construct such a OE-path
nondeterministically, at each stage only the current vertex, the "loop-back" vertex, and a vertex
counter have to be retained in order to construct a successor vertex, loop back, or, if the vertex
counter exceeds the maximal length of the loop, fail. Since both the size of each vertex and the
length of the loop have, by Lemma 2 and Lemma 3, respectively, (singly) exponential representations
in the length of OE, it follows that this nondeterministic procedure requires only exponential space.
[EXPSPACE-hardness] Consider a deterministic 2 n -space-bounded Turing machine M . For
each input X of length n, we construct a TPTL-formula OE X of length O(n \Delta log n) that is valid
accepts X . By a standard complexity-theoretic argument, using the hierarchy theorem for
space, it follows that there is a constant c ? 0 such that every Turing machine that solves the
validity problem for formulas OE of length ' takes space infinitely often. Thus it
suffices to construct, given the initial tape contents X ,
1. a sufficiently succinct formula OE X that describes the (unique) computation of M on X as an
infinite sequence of propositions, and
2. a sufficiently succinct formula OE ACCEPT that characterizes the computation of M on X as
accepting.
Then the implication
is valid iff the machine M accepts the input X .
We use a proposition p i and a proposition q j for every tape symbol i and machine state j of M ,
respectively. In particular, p 0 and q 0 correspond to the special tape symbol "blank" and the initial
state of M . We use the following abbreviations for formulas:
s:
We represent configurations of M by -
p-state sequences of length 2 n that are separated by s-states;
the position of the read-write head is marked by an r-state. The computation of M on X is
completely determined by the following two conditions:
(1) it starts with the initial configuration, and
(2) every configuration follows from the previous one by a move of M .
Both conditions can be expressed in TPTL. Take OE X to consist of 2x: fl y:
to resemble a state counter, and the following two conjuncts, which correspond to the requirements
(1) and (2), respectively:
Here P , Q, and R each range over the propositions -
refers to the
transition function of M . For instance, if M writes, in state j on input i 0 , the symbol k onto the tape,
moves to the right, and enters state j 0 , then f M (-p
The computation of M on X is accepting iff it contains the accepting state F , which is expressible
in TPTL by the formula
The lengths of OE INITIAL , OE MOVE , and OE ACCEPT are O(n \Delta log n), O(n), and O(1), respectively (recall
that constants are represented in binary), thus implying the desired O(n \Delta log n)-bound for OE X .
3.3 Real-time verification
Researchers have proposed a variety of different languages for defining real-time systems [AH92].
Instead of siding with a particular syntax, we represent finite-state real-time systems by abstract
state graphs with timing information. Typically, it is not difficult to compile a given concrete syntax
into timed state graphs (consult, for example, [Hen91] for the translation of timed transition systems
into timed state graphs).
Model checking is an algorithmic verification technique that compares the temporal-logic specification
of a system against a state-graph description of the system. Suppose that a system S is
represented as a finite state graph T S ; that is, all possible runs of S correspond to infinite paths
through T S that meet certain fairness conditions. Furthermore, suppose that the specification of S
is given as a formula OE of a linear temporal logic. The verification problem asks if all possible runs
of the system S satisfy the specification OE.
In the case of PTL, the tableau construction can be used to solve the verification problem
[LP84]. The initial tableau T (:OE) for the negated specification :OE captures precisely the models
of the formula :OE. Hence the system S meets the specification OE iff there is no infinite path that
is common to both finite state graphs, T S and T (:OE), and that corresponds both to a possible
run of S and a model of :OE. This question is answered by constructing the product of the two
state graphs T S and T (:OE) and checking if it contains an infinite path that meets certain fairness
conditions.
We generalize the PTL-algorithm to check if a timed state graph meets a TPTL-specification.
We then show that the problem of checking if a TPTL-formula OE is satisfied by all paths in a given
structure is EXPSPACE-complete, and thus, in general, equally hard as deciding if OE is satisfied
by all timed state sequences. The practitioner will note that complexity of the model checking
problem is doubly exponential only in the size of the formula, which is typically much smaller than
the size of the structure.
Timed state graphs
We represent finite-state real-time systems by finite, directed state graphs (Kripke structures) whose
vertices (locations) are labeled with sets of propositions. Each location is labeled with a state and
a time-difference proposition Prev ffi or Prev -0 , which indicates that the time difference from the
predecessor location is either exactly ffi time units or unspecified, respectively.
Definition 4 (Timed state graph) A timed state graph consists of
ffl a finite set L of locations;
ffl a state labeling function that labels every location ' 2 L with a state - ' '
ffl a time labeling function - that labels every location ' 2 L with a time-difference proposition - ' ,
which is either Prev ffi for some
ffl a set L 0 ' L of initial locations;
ffl a set T ' L 2 of transitions.
A timed state sequence ae = (oe; -) is a computation of the timed state graph T if there is
an infinite path ' such that for all i - 0, oe
A TPTL-formula OE is satisfied [valid ] in the timed state graph T if some [all] computations of
are models of OE. The problem of model checking is to determine if a formula is valid in a timed
state graph.
Model checking
We are given a timed state graph T S and a TPTL-formula OE. Let k be the product of all constants
in OE, and recall that k is the largest constant ffi for which the initial tableau T (OE) for OE contains a
time-difference proposition Prev ffi .
We define the product of the two structures T S and T (OE) to be a finite, directed
graph whose vertices are pairs of T S -vertices and T (OE)-vertices. Each vertex ('; \Phi) of T consists of
a location ' of T S and a vertex \Phi of T (OE) such that
ffl The state information in ' and \Phi is compatible; that is, propositions
ffl The time information in ' and \Phi is compatible; that is, either
The product T contains an edge from the vertex to the vertex contains an
edge from ' 1 to ' 2 and T (OE) contains an edge from \Phi 1 to \Phi 2 .
The size of the product T S \Theta T (OE) is clearly linear in the product of the sizes of T S and T (OE).
An infinite path through the product T S \Theta T (OE) is a OE-path if its second projection is a OE-path
through T (OE); it is an initialized OE-path if, in addition, it starts at a vertex whose first projection
is an initial vertex of T S . The following lemma, which follows immediately from Lemma 4 and the
proof of Theorem 1, confirms that our product construction has the intended effect.
Lemma 7 (Tableau product) The timed state graph T S satisfies the TPTL-formula OE iff the
product contains an initialized OE-path.
This lemma suggests a model checking algorithm. To see if all runs of a finite-state real-time
system S satisfy a TPTL-formula OE:
1. Construct the timed state graph T S for S.
2. Construct the initial tableau T (:OE) for the negated formula :OE.
3. Construct the tableau product
4. Check if T contains an initialized :OE-path. The system S meets the specification OE iff this is
not the case.
According to different notions of system fairness, various variants of computations through timed
state graphs can be defined, and checked for, as in the untimed case [LP84].
Since a structure can be checked for OE-paths in polynomial time, the running time of the model
checking algorithm is determined by the size of the tableau product T , which contains O(jT
vertices. The size of T S typically is exponentially larger than the description of S itself [Hen91];
we have seen that the size of T (OE) can be two exponentials larger than OE.
Theorem 3 (Model checking) The problem if a TPTL-formula OE is valid in a timed state graph
T can be decided in deterministic time linear in the size of the T and doubly exponential in the
length of OE.
Complexity of model checking
Theorem 4 (Complexity of model checking) The problem of deciding if a TPTL-formula is
valid in a timed state graph is EXPSPACE-complete.
Proof of Theorem 4 [EXPSPACE] The given timed state graph T satisfies the TPTL-formula
OE iff the product T \Theta T (:OE) contains an initialized :OE-path. It is easy to see that nondeterministic
singly exponential space suffices to check for the desired :OE-path. The EXPSPACE bound follows.
To reduce the validity problems for TPTL to model checking, it suffices
to give a timed state graph T of constant size such that formula OE is valid iff OE is valid in T . Simply
choose to be the complete graph over all subsets of P , and label all
locations with the time-difference proposition Prev -0 .
4 Undecidable Real-time Properties
At last, let us justify our decisions to restrict the semantics of TPTL to the discrete time domain
N and to restrict the syntax of the timing constraints to successor, ordering, and congruence
operations. Indeed, both decisions seem overly limiting for real-time specification languages. For
example, without addition of time values the property that "the time difference between subsequent
p-states increases forever" cannot be defined. We show, however, that both restrictions are necessary
to obtain verification algorithms.
We consider two natural extensions of TPTL, a syntactic one (allowing addition over time)
and a semantic one (interpreting TPTL-formulas over a dense time domain). Both extensions are
shown to be \Pi 1
1 -complete, by reducing a \Sigma 1
-hard problem of 2-counter machines to the respective
satisfiability problems. It follows that they cannot even be (recursively) axiomatized (for an
exposition of the analytical hierarchy consult [Rog67]).
4.1 A \Sigma 1-complete problem
A nondeterministic 2-counter machine M consists of two counters C and D, and a sequence of n
instructions, each of which may increment or decrement one of the counters, or jump, conditionally
upon one of the counters being zero. After the execution of a non-jump instruction, M proceeds
nondeterministically to one of two specified instructions. We represent the configurations of M by
are the current values of the location counter
and the two counters C and D, respectively. The consecution relation on configurations is defined
in the obvious way. A computation of M is an infinite sequence of related configurations, starting
with the initial configuration h0; 0; 0i. The computation is recurring if it contains infinitely many
configurations with the value of the location counter being 0.
The problem of deciding if a nondeterministic Turing machine has, over the empty tape, a
computation in which the starting state is visited infinitely often, has been shown \Sigma 1
[HPS83]. Along the same lines we obtain the following result.
Lemma 8 (Complexity of 2-counter machines) The problem of deciding if a given nondeterministic
2-counter machine has a recurring computation, is \Sigma 1
Proof of Lemma 8 Every \Sigma 1-formula is equivalent to a \Sigma 1-formula - of the form
for a recursive predicate g [HPS83]. For any such - we can construct a nondeterministic 2-counter
machine M that has a recurring computation iff - is true.
Let M start by computing indefinitely, by nondeterministically guessing
the next value of f . At each stage, M checks whether f(x) and f(x + 1) satisfy g, and if (and
only if ) so, it jumps to instruction 0. Such an M exists, because 2-counter machines can, being
universal, compute the recursive predicate g. It executes the instruction 0 infinitely often iff a
function f with the desired properties exists.
4.2 Encoding computations of 2-counter machines
We show that the satisfiability problem for several extensions of TPTL is \Sigma 1
-complete. First, we
observe that the satisfiability of a formula OE can, in all cases, be phrased as a \Sigma 1
asserting
the existence of a model for OE. Any timed state sequence ae for OE can be encoded, in first-order
arithmetic, by finitely many infinite sets of natural numbers; say, one for each proposition p in OE,
characterizing the states in which p holds, and one to encode pairs of state numbers and associated
times. It is a routine matter to express, as a first-order predicate, that OE holds in ae. We conclude
that satisfiability is in \Sigma 1
1 .
To show that the satisfiability problem of a logic is \Sigma 1
1 -hard, it suffices, given a nondeterministic
2-counter machine M , to construct a formula OE M such that OE M is satisfiable iff M has a recurring
computation. We demonstrate the technique of encoding recurring computations of M by showing
that the monotonicity constraint on time is necessary for the decidability of TPTL.
Theorem 5 (Nonmonotonic time) Relaxing the monotonicity condition for time sequences renders
the satisfiability problem for
Proof of Theorem 5 We encode a computation \Gamma of M by the "time" sequence - such that, for
for the k-th configuration hi; c; di
of \Gamma. The sequence - satisfies the progress condition, but not the monotonicity condition.
It is not difficult to express, by a TPTL-formula OE M , that - encodes a recurring computation
of M . First specify the initial configuration, by
(we abbreviate a sequence of m next operators by fl m ). Then ensure proper consecution by adding
a 2-conjunct OE i for every instruction i of M . For instance, the instruction 1 that increments the
counter C and proceeds, nondeterministically, to either instruction 2 or 3, contributes the conjunct
fly:
The recurrence condition can be expressed by a 23-formula:
Clearly, the conjunction OE M of these n+2 formulas is satisfiable iff M has a recurring computation.
Note that this proof does not require any propositions. It follows that first-order temporal
logic with a single state variable ranging over the natural numbers is \Pi 1
-complete, provided the
underlying assertion language has at least successor (in addition to equality) as a primitive.
4.3 Presburger TPTL
We show that a certain extremely modest relaxation of the syntax of timing constraints leads to a
highly undecidable logic. Consequently, TPTL with addition over time is undecidable.
Theorem 6 (Presburger TPTL) If the syntax of TPTL is extended to allow multiplication by
2, the satisfiability problem becomes \Sigma 1
Proof of Theorem 6 To encode computations of M , we use the propositions
precisely one of which is true in any state; hence we may identify states with propositions. The
configuration hi; c; di of M is represented by the finite sequence
2 of states.
The initial configuration (p 0 ) as well as the recurrence condition (23p 0 ) can be easily expressed
in PTL. The crucial property that allows a temporal logic to specify the consecution relation of
configurations, and thus the set of computations of M , is the ability to copy an arbitrary number
of r-states. In real-time temporal logics, the times that are associated with a state sequence can
be used for copying. With the availability of multiplication by 2, we are able to have the k-th
configuration of a computation correspond, for all k - 0, to the finite sequence of states that is
mapped to the time interval [2 First, we force the time to increase by a strictly positive
amount between successive states (2x: fly: y ? x), to ensure that every state is uniquely identifiable
by its time. Then we can copy groups of r-states by establishing a one-to-one correspondence of
clearly there are enough time gaps to accommodate an
additional r j -state when required by an increment instruction.
For instance, the instruction 1 that increments the counter C and proceeds, nondeterministically,
to either instruction 2 or 3, can be expressed as follows:
where
The first conjunct / 1 ensures the proper progression to one of the two specified instructions, 2 or
3; the second one / 2 establishes a one-to-one correspondence between states in successive intervals
representing configurations, while the formula / 3 (r) copies r-states. The last conjunct / 4 adds,
finally, an r 1 -state at the end of the successor configuration, as required by the increment operation.
We can modify this proof by reducing time to a state counter (2x: fl y:
letting all propositions be false in the resulting additional (padding) states. Thus, the satisfiability
problem for TPTL with multiplication by 2 is \Sigma 1
1 -hard even if time is replaced by a state counter.
As a corollary we infer that the first-order theory of the natural numbers with -, multiplication
by 2, and monadic predicates is \Pi 1
similar result has been obtained independently
in [Hal91], where it is shown that Presburger arithmetic becomes \Pi 1
-complete with the addition of
a single unary predicate.
The proof technique we used to show Presburger TPTL undecidable can be applied to many
real-time specification languages, including the logics RTL [JM86], GCTL [Har88], RTTL [Ost90],
and MTL [Koy90]. All of these formalisms admit addition over time as a primitive, which renders
them undecidable (see [AH90]).
4.4 Dense TPTL
An alternative way of extending the expressive power of TPTL is to relax the semantics by adopting
a dense time domain; that is, between any two given points in time there is another time point.
We show that the resulting logic is, again, highly undecidable.
Theorem 7 (Dense TPTL) If TPTL is interpreted over the rational numbers (i.e.,
the satisfiability problem becomes \Sigma 1
Proof of Theorem 7 The proof depends, once more, on the ability to copy groups of r-states.
This time, we are able to have the k-th configuration of a computation of M correspond, for all
- 0, to the finite sequence of states that is mapped to the time interval
time allows us to squeeze arbitrarily many states into every interval of length 1. Again, we identify
every state with a unique time, and can then establish a one-to-one correspondence of r j -states
In fact, we may simply replace all occurrences of multiplication
by 2 in the Presburger-TPTL formula encoding the recurring computations of M , by a successor
operation, in order to obtain the desired dense-TPTL formula OE M .
This proof goes through for any time domain (T; OE; S) such that (T; OE) is a dense linear order,
and S is a unary function over T that satisfies the following two first-order axioms:
To show that, for arbitrary dense time domains, the satisfiability problem is in \Sigma 1
1 , a standard
L-owenheim-Skolem argument is necessary to infer the existence of countable models.

Acknowledgements

. We thank Zohar Manna, Amir Pnueli, and David Dill for their guidance.
Moshe Vardi and Joe Halpern gave us very helpful advice for refining our undecidability results; in
particular, they pointed out to us the \Sigma 1-completeness of a problem on Turing machines.



--R

Model checking for real-time systems
The benefits of relaxing punctuality.
A really temporal logic.

Logics and models of real time: a survey.

The temporal logic of branching time.
Quantitative temporal reason- ing
On the temporal analysis of fairness.
Presburger arithmetic with unary predicates is
Temporal analysis of real-time systems

The Temporal Specification and Verification of Real-time Systems

What good are digital clocks?
Propositional dynamic logic of regular programs.
Introduction to Automata Theory
Safety analysis of timing properties in real-time systems
Specifying real-time properties with metric temporal logic

Checking that finite-state concurrent programs satisfy their linear specification
The Temporal Logic of Reactive and Concurrent Systems: Specification.
Synthesis of communicating processes from temporal-logic specifications
Proving liveness properties of concurrent programs.
Temporal Logic of Real-time Systems
Applications of temporal logic to the specification of real-time systems
The temporal logic of programs.


The complexity of propositional linear temporal logics.

Asynchronous propositional temporal logic.
Temporal logic can be more expressive.
--TR
The complexity of propositional linear temporal logics
Safety analysis of timing properties in real-time systems
Theory of recursive functions and effective computability
Applications of temporal logic to the specification of real time systems (extended abstract)
Temporal logic for real time systems
Half-order modal logic: how to prove real-time properties
Specifying real-time properties with metric temporal logic
The benefits of relaxing punctuality
Presburger arithmetic with unary predicates is <inline-equation> <f> <g>P</g><sup>1</sup><inf>1</inf></f> </inline-equation> complete
The temporal logic of reactive and concurrent systems
The temporal specification and verification of real-time systems
Checking that finite state concurrent programs satisfy their linear specification
Proving Liveness Properties of Concurrent Programs
Synthesis of Communicating Processes from Temporal Logic Specifications
On the temporal analysis of fairness
The temporal logic of branching time
Introduction To Automata Theory, Languages, And Computation
What Good Are Digital Clocks?
Quantitative Temporal Reasoning
Logics and Models of Real Time
An Old-Fashioned Recipe for Real Time
Proving real-time properties of programs with temporal logic

--CTR
Gaoyan Xie , Cheng Li , Zhe Dang, Linear reachability problems and minimal solutions to linear Diophantine equation systems, Theoretical Computer Science, v.328 n.1-2, p.203-219, 29 November 2004
Farn Wang , Chia-Tien Lo, Procedure-Level Verification of Real-time Concurrent Systems, Real-Time Systems, v.16 n.1, p.81-114, Jan. 1999
Denis Lugiez , Philippe Schnoebelen, Decidable first-order transition logics for PA-processes, Information and Computation, v.203 n.1, p.75-113, November 25, 2005
Roberto Barbuti , Nicoletta De Francesco , Antonella Santone , Gigiola Vaglini, Logic Based Abstractions of Real-Time Systems, Formal Methods in System Design, v.17 n.3, p.201-220, Dec. 2000
Oscar H. Ibarra , Zhe Dang , Pierluigi San Pietro, Verification in loosely synchronous queue-connected discrete timed automata, Theoretical Computer Science, v.290 n.3, p.1713-1735, 3 January
Andreas Schfer, Axiomatisation and decidability of multi-dimensional Duration Calculus, Information and Computation, v.205 n.1, p.25-64, January, 2007
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
Zhe Dang , Tevfik Bultan , Oscar H. Ibarra , Richard A. Kemmerer, Past pushdown timed automata and safety verification, Theoretical Computer Science, v.313 n.1, p.57-71, 16 February 2004
Zhe Dang , Oscar H. Ibarra , Richard A. Kemmerer, Generalized discrete timed automata: decidable approximations for safety verification, Theoretical Computer Science, v.296 n.1, p.59-74, 4 March
Kees van Hee , Olivia Oanea , Alexander Serebrenik , Natalia Sidorova , Marc Voorhoeve, LogLogics: A logic for history-dependent business processes, Science of Computer Programming, v.65 n.1, p.30-40, March, 2007
Stphane Demri , Deepak D'Souza, An automata-theoretic approach to constraint LTL, Information and Computation, v.205 n.3, p.380-415, March, 2007
Stphane Demri, LTL Over integer periodicity constraints, Theoretical Computer Science, v.360 n.1, p.96-123, 21 August 2006
F. Laroussinie , Ph. Schnoebelen , M. Turuani, On the expressivity and complexity of quantitative branching-time temporal logics, Theoretical Computer Science, v.297 n.1-3, p.297-315, 17 March
Nicolas Markey , Jean-Franois Raskin, Model checking restricted sets of timed paths, Theoretical Computer Science, v.358 n.2, p.273-292, 7 August 2006
Sascha Konrad , Betty H. C. Cheng, Real-time specification patterns, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA
Roberto Barbuti , Luca Tesei, A decidable notion of timed non-interference, Fundamenta Informaticae, v.54 n.2-3, p.137-150, February
Alur , Toms Feder , Thomas A. Henzinger, The benefits of relaxing punctuality, Journal of the ACM (JACM), v.43 n.1, p.116-146, Jan. 1996
Roberto Barbuti , Luca Tesei, A Decidable Notion of Timed Non-Interference, Fundamenta Informaticae, v.54 n.2-3, p.137-150, April
Zhe Dang, Pushdown timed automata: a binary reachability characterization and safety verification, Theoretical Computer Science, v.302 n.1-3, p.93-121, 13 June
Alur , Thomas A. Henzinger , Pei-Hsin Ho, Automatic Symbolic Verification of Embedded Systems, IEEE Transactions on Software Engineering, v.22 n.3, p.181-201, March 1996
Zhe Dang , Pierluigi San Pietro , Richard A. Kemmerer, Presburger liveness verification of discrete timed automata, Theoretical Computer Science, v.299 n.1-3, p.413-438,
Ruggero Lanotte , Andrea Maggiolo-Schettini, Monotonic hybrid systems, Journal of Computer and System Sciences, v.71 n.1, p.34-69, July 2005
Ruggero Lanotte , Andrea Maggiolo-Schettini , Simone Tini, Information flow in hybrid systems, ACM Transactions on Embedded Computing Systems (TECS), v.3 n.4, p.760-799, November 2004
Roberto Barbuti , Nicoletta De Francesco , Luca Tesei, Timed Automata with non-Instantaneous Actions, Fundamenta Informaticae, v.47 n.3-4, p.189-200, August 2001
F. Laroussinie , N. Markey , Ph. Schnoebelen, Efficient timed model checking for discrete-time systems, Theoretical Computer Science, v.353 n.1, p.249-271, 14 March 2006
Stphane Demri , Ranko Lazi , David Nowak, On the freeze quantifier in Constraint LTL: Decidability and complexity, Information and Computation, v.205 n.1, p.2-24, January, 2007
discrete time;dense time;real-time requirements;linear-time temporal logic;model checking;EXPSPACE-completeness