BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR93-1345
ENTRY:: 1993-10-14
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: Parametric Real-Time Reasoning
AUTHOR:: Alur, Rajeev
AUTHOR:: Henzinger, Thomas A.
DATE:: May 1993
PAGES:: 15
ABSTRACT::
Traditional approaches to the algorithmic verification of real-time systems 
are limited to checking program correctness with respect to concrete timing 
properties (e.g., ``message delivery within 10 milliseconds''). We address 
the more realistic and more ambitious problem of deriving symbolic constraints 
on the timing properties required of real-time systems (e.g., ``message 
delivery within the time it takes to execute two assignment statements''). To 
model this problem, we introduce parametric timed automata - finite-state 
machines whose transitions are constrained with parametric timing 
requirements.

The emptiness question for parametric timed automata is central to the 
verification problem. On the negative side, we show that in general this 
question is undecidable. On the positive side, we provide algorithms for 
checking the emptiness of restricted classes of parametric timed automata. 
The practical relevance of these classes is illustrated with several 
verification examples. There remains a gap between the automata classes for 
which we know that emptiness is decidable and undecidable, respectively, and 
this gap is related to various hard and open problems of logic and automata 
theory.
END:: CORNELLCS//TR93-1345
BODY::
Parametric Real-Time Reasoning*
Rajeev Alur
Thomas A. Henzinger**
Moshe Y. Vardi
TR 93-1345
May1993
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
*An abbreviated version of this paper appeared in the Proceedings of the 25th
Annual ACM Symposium on Theory of Computing (STOC 1993).
**Supported by the National Science Foundation under grant CCR-9200794 and by
the United States Air Force Office of Scientific Research under contract F49620-93-1 -
0056.
Parametric R?ea1-tirne Reascning*
Rajeev Alur
AT&T Bell Laboratories
Murray Hill, NJ
Thomas A. Herizingert
Department of Computer Science
Cornell University, Ithaca, NY
Moshe Y. Vardi
IBM Almaden R?esearch Center
San Jose, CA
Abstract. Traditional approaches to the algorithmic verification of real-time sys-
tems are limited to checking program correctuess with respect to concrete timing prop-
erties (e.g., "message delivery within 10 milliseconds"). We address the more realistic
and more ambitions problem of deriving symbolic constraints on the timing properties
required of real-time systems (e.g., "message delivery within the time it takes to execute
two assignment statements"). To model this problem, we introduce pararnetric tirned
autornata finite-state machines whose transitions are constrained with parametric
timing requirements.
The emptiness question for parametric timed automata is central to the verification
problem. On the negative side, we show that in general this question is undecidable. On
the positive side, we provide algorithms for checking the emptiness of restricted classes
of parametric timed automata. The practical relevance of these classes is illustrated
with several verification examples. There remains a gap between the automata classes
for which we know that emptiness is decidable and undecidable, respectively, and this
gap is related to various hard and open problems of logic and automata theory.
1 Introduction
Over the last fifteen years, an extensive amount of research has gone into providing foundations for
the verification of reactive and concurrent systems (cf. [MP92]). Most of this research, however,
is focused on the verification of qualitative properties such as "safety" and "liveness," rather than
timing properties, as is needed for the verification of real-time systems. This deficiency has been
addressed over the last few years, and numerous formal approadies to the verification of real-
time systems have been advocated (cf. [Koy90, Ost9O, Alu9l, Hen91, Hoo91, AL92, SflM92j).
Essentially all algorithmic approaches suffer, however, from a serious flaw: they are addressed at
verifying concrete specifications, such as "an acknowledgement will be sent 10 milliseconds after
a message has been received." Concrete timing constraints can be expressed and algorithmically
An abbreviated version of th? paper appeared in the Proceedings of the 25th Annual ACM Symposium on Theory
of Computing (STOC 1993).
t5upported by the National Science Foundation under grant CCR-92o()794 and by the United States Air Force
Office of Scientific Research under contract F4962o-93-1-0o56.
verified using real-time temporal logics [AH89, AH9O, EMSS9o, llLP9O, AFH9l, IINSY92, WME92]
or time-constrained finite-state machines [Dil89, Lew9O, AD9O, ACD9o, A1192].
In reality, however, real-time systems are typically embedded in larger environments, and the
system designer has to design the system relative to certain parameters of the environment. Thus
arises the real need for verifying pararnetric specifications. For example, "given a real-time system 5,
one may wish to verify a property p of the system as long as the deadline d of an action is less than
the delay ? in receiving an acknowledgement, r> d" [Jah89j. The design of a robust system requires
the verification of the desired behavior of the system without concrete values for the parameters ?
and d. Indeed, when studying the literature on real-time protocols, one sees that the desired timing
properties for protocols are almost invariably parametric (cf. [SDC9o, ADLS9l, WZ92]), because
concrete timing constraints make sense only in the context of a given concrete environment.
In this paper, we attempt to lay the foundations for a theory of parametflc reasoning about real
time. The main reason that previous research has concentrated on concrete rather than parametric
timing constraints is the extreme difficulty of the parametric verification problem. In fact, it is
not hard to show that standard real-time temporal logics become undecidable even when a single
parameter is introduced. Hence, rather than temporal logic, we use finite-state machines with
parametric timing constraints pararnetric tim?d automate as a basis for our theory. Our
results will be threefold. First, we present an algorithm for solving a nontrivial class of parametric
verification problems. Second, we prove a large class of parametric verification problems to be
undecidable. Third, we show that the remaining (intermediate) class of parametric verification
problems, for which we have neither decision procedures nor undecidability results, is closely related
to various hard and open problems of logic and automata theo?y.
Parametric timed automata generalize the timed automata of [AD9oj, which have emerged as
an attractive model for real-time systems (see [ACD9o, CY9l, AH92, HNSY92j for extensions and
applications). Timed automata are finite-state machines that are equipped with clocks, which are
used to constrain the accepting runs by imposing timing requirements on the transitions. While
the timing requirements of timed automata are concrete say, a transition is enabled for 10 time
units the timing requirements of parametric timed automata are parametric a transition is
enabled for d time units, for some parameter d.
A parametric timed automaton characterizes a set of parameter values, namely, those for which
the automaton has an accepting run. Thus, a parametric timed automaton is, like a system of
equations or inequalities, simply a constraint on admissible parameter values. Our focus in this
paper is on the basic problem of emptiness for parametric timed automata: given a parametric timed
automaton, are there concrete values for the parameters so that the automaton has an accepting
run? The solution of this problem allows the verification of parametric real-time specifications,
which we demonstrate by providing parametric verifications of a railroad gate controller and of
Fischer's timing-based mutual-exclusion protocol.
Our investigation of the emptiness problem reveals that the number of clocks in a parametric
timed automaton is critical to the decidability of the problem. For automata with one parametri-
cally constrained clock (and possibly many concretely constrained clocks), emptiness is decidable.
In contrast, we show that three parametrically constrained clocks are sufficient to bring about unde-
cidability. We describe, however, a symbolic fixpoint computation procedure to solve the emptiness
problem. The procedure is sound, and though its termination is not guaranteed in general, it termi-
nates for many examples of practical interest. The decidability in the case of two clocks is open, and
it reveals intriguing connections with hard decision problems in logic (existential Presburger arith-
metic with divisibility) and automata theory (special classes of nondeterministic two-way 1-counter
machines).
2
Since clocks are used to measure delays between events, the number of clocks is a fair indicator
of the structural complexity of the timing constraints imposed on a system. Our results indicate
that the hope for automated parametric real-time reasoning should be limited to systems with
timing constraints of limited complexity.
2 Parametric Timed Automata
Timed automata provide an abstract model for real-time systems [AD90]. While ordinary automata
generate (or accept) sequences of events (or states), timed automata are additionally constrained by
timing requirements and generate timed sequences. A timed automaton operates with finite control
__ a finite set of states and a finite set of clocks. All clocks proceed at the same rate and measure
the amount of time that has elapsed since they were started (or reset). Each transition of the
automaton may reset some of the clocks, and it puts certain constraints on the values of the clocks:
a transition can be taken only if the current clock values satisfy the corresponding constraints. All
clock constraints of standard timed automata are boolean combinations of atomic conditions that
compare clock values with constants. Parametric timed automata allow within clock constraints
the use of parameters i.e., unknown constants in place of constants.
Definitions
For the simplicity of presentation, we consider automata over finite words only. Throughout we
will use x, y, z as names for clocks, and a, b, c as names for parameters. We use T to denote
the domain of time values. The choices for I we are most interested in are the set N of natural
numbers and the set R+ of nonnegative reals. Unless explicitly specified, our results will apply for
both instances of I.
Let P be a set of parameters. A parameter valuation for P is an assignment of values in I to
the parameters in P; we will use ? to denote a parameter valuation. We model delays using timing
constraints of the form x E I, where x is a clock and I is a symbolic intervaL A symbolic interval
is specified by (1) its type, which can be one of the following four possible choices: open, closed,
left-open right-closed, or left-closed right-open; and (2) its left and right endpoints, each of which
is either a natural number or a parameter; for right-open intervals, the right endpoint may also be
00. Thus examples of symbolic intervals are [2, a), (a, b], (c, 00), etc. We use 1(P) to denote the set
of all symbolic intervals that use the parameters in P. For a symbolic interval I and a parameter
valuation ?, we obtain an interval ?(f) of I.
A parametric timed automaton is a tuple A = (?, S, 5o, C, P, t E), where ? is a finite input
alphabet, 5 is a finite set of states, 5o ? 5 is a set of initial states, C is a finite set of clocks, P is a
finite set of parameters, F C 5 is a set of final (or accepting) states, and  C 5 x ? x 5 x 2? x
1(P)] is a finite set of edges. Each edge (s, a, 5', A, ?) represents a transition from state s to state
on the input symbol a. The set A c c specifies the clocks to be reset, and for each clock x ?
the symbolic interval jt(?) specifies the bounds on the value of x.
A configuration of the automaton A is represented by a pair (s, v), where s ? 5 gives the
state and v: C T gives values for all clocks. The behavior of the automaton depends upon
the current configuration and the values of the parameters. Each parameter valuation ? for P
induces a transition relation ? over the configurations of A as follows: a configuration (s', v') is a
(a, t)-successor of (s, v), where a E ? and t E I, with respect to a parameter valuation ?, wntten
E ??(s,v,(?t)), iff there is an edge (s,Q51,A,[) E  such that for all clocks x E
3
1. v(x)+t E ?(jt(x)), and
x = a, x := 0
Figure 1: A parametric timed automaton
2. if x E A then v'(x) = 0, else v'(x) = v(x) + t.
A timed word w E (? x I)* is a finite sequence of pairs of input symbols and time values,
which represent the delays (i.e., time increments) between successive input symbols. The transition
relation 6? can be extended to timed words:
1. (s,v) E ??(s,v,e), and
2. (s', v') E ??(s, v, (a, t).w) iff for some configuration (s", v"), both (s", v") E ??(s, v, (a, I)) and
(s', v') E 6?(s?, v11, w).
A timed language is a set of timed words. Given a parametric timed automaton A and a
parameter valuation ?, the timed language accepted by A with respect to ?, denoted by L?(A),
consists of all timed words w such that (s', v') E 6?(s, v0, w) for some initial state s e S0, some
accepting state 5' E F, and the initial clock values v0 defined by v0() = 0 for all x C C. A
parameter valuation ? is consistent with A iff L?(A) is nonempty. Thus, a parameter valuation ?
is consistent with A iff there exists a path from an initial state to a final state such that all the
constraints on the clock values, as specified by the choice ? for parameter values, are satisfied along
the path. We denote the set of parameter valuations consistent with A by F(A).
Two parametric timed automata A and B are equivalent iff L?(A) = L?(B) for all parameter
valuations ?. Notice that if A and B are equivalent, then F(A) =
An example
As an example, consider the parametric timed automaton shown in Figure 1. The automaton
consists of three states; ?o is the only initial state, and 52 is the only final state. The input alphabet
is unary, the set of clocks is [x, yy, and the set of parameters is (a, b, c]. An edge (s, a, s', A, ?) is
shown by an arrow from state s to state s'. Since the alphabet is unary, the edges are not labeled
with any input symbols. The edges are labeled with constraints x E jt(x), and with assignments
x := 0 for each x ? A. Constraints of the form x E [0, oc) are suppressed, and the constraint x = a
means ji(x) = [a, a].
For a parameter valuation ?, the final state 52 is reachable from the initial state (i.e., ? E F(A))
iff ?(c) = n.?(a) + ?(b) for some n E N.
Real-time verification
Parametric timed automata can be used to solve verification problems for real-time systems. In
automata-theoretic verification (cf. [V?786, AD9O, Kur9O]), a finite-state system is modeled by an
automaton: the set of words accepted by the automaton corresponds to the possible behaviors of
the system. While automata on infinite words can be used to deal with nonterminating processes,
for verifying safety properties it suffices to consider automata over finite words.
4
We specify each concurrent process of a finite-state real-time system as a parametric timed
automaton. For a given parameter valuation, the possible behaviors of the system are those timed
words whose projections are accepted by the component automata. Let Li, i 1,2, be two
timed languages over the aiphabets `Si. We write L1 A L2 for the timed language over the alphabet
?i u"'2 that contains all timed words whose ?1-projection is in L1 and whose ?2-pWjection is in L2
(the ?i?prQecti0n of a timed word is obtained by repeatedly replacing each two-element substring
(a, t) . (a', t') with a ? ?i by the pair (a', t t t')). Given two parametric timed automata A1 and
A2, we can define another parametric timed automaton, the product automaton A1 0 A2 (using a
product construction similar to the one in [AD9o]), such that for all parameter valuations ?,
L?(A10A2) = L?(A1)nL?(A2).
A system is modeled, then, by a product automaton 0Aj. We specify the correctness condition
of the system by another parametric timed automaton, B, which accepts the "bad" or undesirable
behaviors (i.e., the complement of the safety property to be verified). It follows that for a parameter
valuation ?, the system is incorrect precisely when the automaton 0Aj generates a bad behavior
that is accepted by the automaton B; that is, iff? ? F(A) for the product automaton A =
Equivalently, the system is correct for given delay values ? iff ? ?
In a typical parametric verification problem, we want to prove that a system satisfies its speci-
fication for all parameters values that meet a given set of constraints. In other words, given a set
A c [P Tj of possible parameter valuations, we wish to verify that no ? e A is consistent with
A; that is, A n F(A) = ?. In a typical parametric synthesis problem, we want to find all parame-
ter valuations F(A) that are consistent with A, or we want to find a parameter valuation that is
consistent with A and is optimal with respect to some criterion. For instance, one can pose the
problem of finding minimum or m?ximum delays in this form. Later, we will present two examples
of the parametric synthesis problem and their solutions.
3 Decision Problems
Given a parametric timed automaton A, different types of questions can be asked about the set
F(A) of consistent parameter valuations. The membership question --H? 1.e.,the question of deciding
whether a specific parameter valuation ? is consistent with A ---H can be solved using the techniques
developed in [AD9O]. The method applies to both cases T = N and T = R+, provided that the
valuation ? assigns rational numbers to all parameters in the latter case. In fact, given a parameter
valuation ?, one can construct a finite-state automaton A? that accepts L?(A). Then ? ? F(A) iff
A? accepts some string. The membership question is known to be PSPACE-complete.
The solution of the membership question allows the solution of the parametric verification
problem for finite sets A of possible parameter valuations. In this paper, we concentrate on solving
the parametric verification problem for the universal set A containing all parameter valuations;
that is, we wish to solve the emptiness question,
Is there some parameter valuation consistent with A?
The following result applies to both integer and real-number time doinains.
THEoREM [Recursive enumerability of nonemptiness]. Given a parametric timed an-
tomaton A, the question if F(A) is not empty is recursively enumerable.
PROOF. From the decidability of the membership problem, we conclude that emptiness is co-
r.e. for T = N. In the case of T = R+, the same observation follows from the fact that if F(A) is
not empty then it contains a parameter valuation all of whose values are rational. i
5
To solve the parametric verification and synthesis problem, it is useful to obtain an explicit
representation of F(A) in a, possibly decidable, logical formalism. Notice that the input alphabet
plays no role in the definition of F(A) and, henceforth, we will assume that j?j = 1 and omit
the edge labels a. We will use existentially quantified formulas of arithmetic with addition and
order for defining sets of parameter valuations. To be precise, a 1in?ar formula ? over a set X of
variables is of the form (?Y ?), where ? is a quantifier-free formula over the variables in X u Y
that is formed using the primitives =, <, +, A, V, and integer constants. Such a formula ? specifies
IX -tuples of values from T. Given a linear formula ?, it is decidable to check if ? is satisfiable in
both cases in which the variables are interpreted over the natural numbers or the nonnegative reals,
respectively [End72]. Also for formulas ? and ? with the same set of free variables, it is decidable
to check if ? and ? specify the same sets.
3.1 A Decidability Result
A crucial resource of a parametric timed automaton is the number of clocks it employs. In this
section, we show that if an automaton A uses only one clock, then the question if F(A) is empty
is decidable. By itself, the class of automata with just one clock may not seem very interesting;
however, over a discrete time domain, if in an automaton only one clock is involved in a constraint
that contains parameters, then we can construct an equivalent automaton that uses only one clock.
Thus we can solve the real-time verification problem for systems that contain one parametrically
constrained clock. Also the problems of computing minimum and maximum delays in fully specified
systems [CY91] can be posed as synthesis problems on timed automata with one parametric clock.
Throughout Subsection 3.1 let T =
Eliminating nonparametric clocks
A clock ? E C is parametncaliy co?strained iff for some edge (a, a, 5', A, ?) E F, one of the endpoints
of the interval jt(x) is a parameter in P. We first show how clocks that are not parametrically
constrained can be eliminated.
With each transition the values of the clocks increase by a natural number. To eliminate the
nonparametric timing constraints, we label edges with time increments. Indeed, we show that it
suffices to assume that with every transition the clocks increase by at most 1. Hence we define
0/1-automata. A parametric timed 0/1-automaton A = (5, So, C, P, P, E) is a timed automaton
whose edges (a, a', A, ?, t) are additionally labeled with a time increment t E [0, t?. As before, a
configuration of the automaton A is represented by a pair (a, v), where a E 5 gives the state and
v: C :` N gives values for all clocks. The transition relation over the configurations is defined as
before, except that the increase in the clock values is determined by the edge label t. The following
lemma shows that we can eliminate all clocks that are not involved in a parametric constraint.
LEMMA [Eliminating nonparametric clocks]. Given a parametric timed automaton A
(5, So, C, P, F, ), we can effectively construct another parametric timed 0/1-automaton A' --H
(5', St, c', p, pi, E') such that C' C C contains only the parametrically constrained clocks of A
and I'(A) = I'(A'). 1
Disjunctive path constraints
Consider a parametric timed 0/i-automaton A = (5, So, C, P, P, F) that contains only a single
clock r. Suppose that 5 = [ai,.. .a??. For all 1 < i,j < n we define a formula ?? over the free
variables [x, r'J UP. The intended meaning of this formula is that for every parameter valuation ?,
6
the formula Y'i5 specifies a binary relation over N: for clock values t and t', the machine configuration
(sj, t') is reachable from (si, t) with respect to ? iff 4)ij holds for the interpretation ?[x := t][x' :=
Our goal is to show that the formulas 4)?3 are linear formulas of a special form. To define these
formulas in a dynamic-programming fashion, we use auxiliary formulas %, 0 < k < n, where
holds for the interpretation ?[x := t][r' := t'] iff the configuration (s5,t') can be reached, with
respect to ?, from (st, t) without visiting any state indexed higher than k.
Let V be a new set of variables. A linear term is of the form n1i1 + + nmim + nm+1, where
...... im E V and ..... . n?+1 E N. We will build formulas from linear terms using equalities and
inequalities and, ultimately, we will quantify existentially over the variables in V. The abbreviation
e E I, where e is an expression and I is a symbolic interval, denotes a formula; for instance, if
I = (2, a], then eEl stands for the conjunction (2 ? e) A (e ? a).
A (simple) path constraint 4) has one of two forms:
1. 4) is a conjunction (x' = x + a') A 4), where a is a linear term, and 4) is a conjunction of atomic
formulas of the form (x + (3 E 1), with (3 being a linear term and I being a symbolic interval;
or
2.
4) is a conjunction (x' = a) A ?,`, where 0 is a linear term, and ? is a conjunction of atomic
formulas of the form (x + (3 E I) or ((3 E I), with (3 being a linear term and I being a symbolic
interval.
A disjunctive path constraint is a disjunction of simple path constraints.
Every formula 4) over the free variables V u P u fx, x'? defines, for a fixed parameter valuation
?, a binary relation R?(4)) over N: (1,1') belongs to R?(4)) iff (aV; 4)) holds for the interpretation
t']. The operations of composition and transitive closure over binary relations
can, then, be applied to formulas. We say that a formula 4) defines the composition 4)i 4)2 iff for
every parameter valuation ?,the relation R?(4)) is the composition of the relation R?(4)1) with the
relation ft?(4)2). Similarly, a formula 4) defines 4) iff for every ?, the relation ??(4)) is the reflexive
and transitive closure of ?(4)). Thus 4)* is the infinite disjunction
(x'= x)v4)v(4)4))v(4).4).4))v....
The following closure allows us to replace this infinite disjunction by a finite disjunction.
LEMMA [Disjunctive path constraints]. The set of disjunctive path constraints is closed
under disjunction, composition, and refiexive-transitive closure.
PRoOF. Disjunctive path constraints are closed under disjunction by definition.
The composition of two simple path constraints 4)i and 4)2 is defined as follows. We assume
that the variables in V that appear in 4)i and in 4)2 are disjoint; otherwise, renaming is necessary.
Suppose that 4)i contains the conjunct (x' = (3) for some term (3 (here, (3 may contain x). Then
4)i 4)2 is 4)'i A (4)2[x := (3]), where the formula 4)2[r := (3] is obtained from 4)2 by replacing every
occurrence of ? with (3, and the formula 4)'i is obtained from 4)i by omitting the conjunct (x' = (3).
it is easy to check that for a given parameter valuation ?, (?V. 4)1?4)2) holds for the interpretation
:= t][x' := t'] iff there exists a clock value t" E N such that (?V. 4)i) holds for ?[x := t][x' :=
and (?V. 4)2) holds for ?[x := t"][x' := t']. Composition can easily be extended to disjunctive path
constraints, because composition distributes over disjunction.
For alinear term a = n1i1 +			+ nmim + nn?+i, let 0* be the linear term n1i1 +			+ flm?m +
flm+1?m+1, where im+1 E V is a variable not appearing in a. The reflexive and transitive closure
of a disjunctive path constraint 4) is defined as follows:
7
(1) Suppose that ? contains a disjunct ? of the form (r' = 0) A X. Let ? be ? v ?` (note
that disjunction commutes, and ?` may be false). Then ? is ??? V (?`?.?.?`?), where false*is
(2) Suppose that ?is V1=1,,??, where each ? is oftheform (x' = x+o1) A i'i Let ? = 1i, Ik
be a sequence such that 1 < < n for each 15 and each integer appears at most twice in the sequence
. There are only finitely many such sequences. For each such sequence ?, the formula 4)* contains
a disjunct
??: ?t1 ,x,?			9lk?1??(k--H1?Y'lk
The formula Xi, for 1 < i ? k, stands for
(x'=x+?5?1 .nt)
where each term P' is if there exist 1 ? k1 ? < k2 ? k such that 1k1 = 1k2 = j, and ??3 is 0
otherwise. `
Computing consistent parameter valuations
We use the closure properties of disjunctive path constraints to define the formulas ?? in a dynamic-
programming fashion. For e = (s,s',A,?,t) E , if x E A, then let y(e) be the formula (x' --H
0) A (x + t E ti(x)); otherwise, let ?(e) be the formula (x' = x + t) A (x + t E ii(x)). Now, for
1 <i,j < n, ? ? j, define
and for 1<? j,kS n, define
?`t9j : Ve?(si,??s? A,p?t)EE
: [V?=(si?a,si,;\?iit)EE ?(e)]*;
%: $yl v KkiFl?(9k4Tl)*?Qffil]
Each formula is a disjunctive path constraint. The following lemma explains the meaning of
these formulas.
LEMMA [Computing F(A)]. For all 1 < ?,j ? n, 0 < k < n clock values 1,t' ? N, and
parameter valuations ?, the configuration (s?, ?`) can be reached from the configuration (si, t)
with respect to ?, without visiting any state in fsk+1nY along the way, iff the interpretation
tj[x' := t'] satisfies the formula (?V. %). ?
The desired formula ?? is for all 1 ? i,j < n. Observe that
F(A) =
u
?i,5jsiESo,s,EF?
Thus we have an algorithm for computing the set F(A) of consistent parameter valuations for
discrete-time automata with one parametrically constrained clock.
THEOREM [Deciding the single?clock case]. For a parametric timed automaton A that
contains only one parametrically constrained clock, if T = N, then the set F(A) can be defined by
a linear formula, and testing emptiness of L(A) is decidable.
We point out that in the case of real-number time, a similar dynamic-programming construction
can be used to show that for a parametric timed automaton A with a single clock, the set L(A) is
definable by a linear formula and testing emptiness of L(A) is decidable.
8
approach			1y:=O			?oaP).0aoc			(5
down			raise			lower
x<b			x>a c<y<d			c<y<d			e<z<f			e<z<f
_________			y:=O			z:=O
out
TRAIN			GATE			CONTROLLER
Figure 2: Railroad gate controller
Verification example: computing delay bounds
We wish to design a controller that opens and closes a gate at a railroad crossing [LS85]. The
system is composed of three components: TRAIN, GATE, and CONTROLLER. The automata
that model the three components are shown in Figure 2.
The input alphabet for TRAIN is ?approach, exit, in, out?. The train communicates with the
controller via the two events (input symbols) approach and exit. The events in and out mark the
events of entry and exit of the train with respect to the railroad crossing. The train is required to
send the signal approach at least a minutes before it enters the crossing, and the maximum delay
between the signals approach and exit is b minutes. The alphabet for GATE is (raise, lower, up,
down?. The gate is open in state 0 and closed in state 2. It communicates with the controller using
the signals lower and raise. The events up and down denote the opening and the closing of the
gate. The response time of the gate is in the interval (c, d;). Finally, for the controller, the alphabet
is (approach, exit, raise, Thwer). Whenever the controller receives the signal approach from the
train, it responds by sending the signal Thwer to the gate, and whenever it receives the signal exit,
it responds with the signal raise. The response time of the controller has a lower bound e and an
upper bound f.
One of the correctness requirements for the system is the following safety condition:
Whenever the train is inside the gate, the gate should be closed.
To test this safety property, we obtain an automaton A from the product TRAIN 0 GATE &
CONTROLLER by requiring that a state (5i, 52,53) of the product is an accepting state iff si = 2
(i.e., the train is inside the crossing) and ?2 # 2 (i.e., the gate is not closed). A parameter valuation
? belongs to I'(A) iff the safety property does not hold. The reader can check that ? ? F(A) iff
<?(d) + ?(f).
Suppose we are given particular values for the train and gate delays a, b, c, and d. Then only
the controller clock z is parametrically constrained. Thus we may use the algorithm outlined above
to automatically derive necessary and sufficient bounds e and f on the controller delays, namely,
3.2 Undecidability of Emptiness
We now show that the emptiness problem for parametric timed automata is in general undecidable.
Indeed, undecidability ensues even if we restrict the number of clocks to three, and the proof applies
to both possible choices of the time domain T.
9
z := 0
Figure 3: Undecidability proof
x=b
x:=O
THEOREM [Undecidability of emptiness]. Given a parametric timed automaton A, the
problem of deciding if F(A) is empty is undecidable.
PRooF. We reduce the halting problem for 2-counter machines to the problem of testing if there
exists a consistent parameter valuation. Consider a 2-counter machine M with two counters C1
and C2. The control variable ? for M ranges over the set ....... inj. Each instruction of WI can
either increment or decrement one of the counters, test if one of the counters equals 0, and change
the location of control. A configuration of M is given by the triple (l?, c?, c2), specifying the values
of?, C1, and C2, respectively. The initial configuration of ?i is (1i, 0,0). The halting problem is to
decide if M reaches a configuration (i?, c1, c2) for some c1 and c2. We construct a parametric timed
automaton AM with three clocks such that F(AM) is nonempty iff M halts. The theorem follows.
The automaton AM uses three clocks x, y, z, and the set ofparameters is [a, a?1, a+1, b, b?1, b+1J.
The automaton has a start state 5o, a state l? corresponding to each possible value of the control
variable , and some auxiliary states. We want that for a parameter valuation ?, a configuration
(ij,v) of AM is reachable iff v(x) = 0 and the configuration (ii,?(b) --H v(y),?(b --H a) --H v(z)) is
reachable for ill.
Using some auxiliary states and appropriate edges between them, we add a path between 5o and
ii such that for a given ?, the configuration (i?, v) is reachable from (so, v') iff ?(a) = ?(a?1) + 1 =
--H 1, ?(b) = ?(b?1) + 1 = ?(b+1) --H 1, v(x) = 0, v(y) = ?(b), and v(z) = ?(b --H a). This sets
up the initial configuration.
For every instruction of M we add a path between the appropriate states lj of AM. For instance,
consider an instruction of M of the form 4f ? = l? then C1 := C1 + 1 and ? := ii." Corresponding
to this instruction, AM contains a path from state i? to state i? as shown in Figure 3. Consider
a configuration (li, v) of AM with v(x) = 0. It encodes the configuration (i?, c1c2) of M with
c1 = ?(b) --H v(v) and c2 = ?(b --H a) --H v(z). The path can be traversed if ?(a) > c1 + 1, and the
new configuration is (I?, v') with v'(r) = 0, v'(y) = v(y) --H 1, and v'(z) = v(z). Thus the new
configuration correctly encodes the configuration (ij, c1 + 1, c2) of j?.
If the instruction is "if ? = Ij then C1 := C1 --H 1 and ? := i?," then the path will be as shown
in Figure 3 with the constraint y = b+1 replaced by y = b?1. And if the instruction is ?f ` = ii
and C1 = 0 then  := ii," then the path will be as shown in Figure 3 with the constraint y = b+1
replaced by (y = b) A (x = 0).
The accepting state of AM is i?. If WI does not halt, then there is no way to reach in in
AM, and F(A) = ?. If M halts, and suppose the values of C1 and C2 never exceed c1 and c2,
respectively. Then for a parameter valuation ?, ? ? F(A) iff ?(a) = ?(a?1) + 1 = ?(a+1) --H 1, and
?(b)= ?(b?1)+ 1 =?(b+1)--H 1, and ?(a) > c1, and ?(b--Ha) > c2. .
Symbolic computation
Even though the problem of testing the emptiness of F( A) is in general undecidable, we can attempt
to construct a logical formula that explicitly represents the set F(A). Methods that use symbolic
fixpoint computation for this purpose have been developed for analyzing timed automata [HNSY92]
and hybrid automata [ACHH93].
10
Consider a parametric timed automaton A = (?, 5, 5o, C, P, F, E). For > 0 and 5 ? 5, define
the set ?(s) E [(C u P) i, T] of clock and parameter valuations such that a final state can be
reached from the states within at most i transitions: (v,?) ? ?i(5) iff (5', ii') E &,(s, v,w) for some
final state s' E P, some clock values v', and some timed word w with WI < 2..
THEOREM [Bounded reachability]. For all > 0 and s E 5, the set #(s) can be defined by
a linear formula over the free variables C u P..
PROOF. We define the formulas #(s) by induction on ?. First we set, for s E F, ?O(s) := true
and for s ? P, ?O(s) := false. Then we compute the formula
??(s): ?i?1(5) V (VbJEs pre(s,s',???1(s'))),
where pre(s, 5', ?) defines the set of clock and parameter valuations such that from 5 some transition
leads to 5' and a clock and parameter valuation satisfying u'. For every linear formula ?, and for
either choice of time domain, the set pre(s, 5', i") is definable by a linear formula [AC11H93]. I
Since there are algorithms for checking the equivalence of linear formulas, we obtain a procedure
for computing the set F(A): if for all states 5 e 5, the successive approximations #(s) and ??1(s)
are equivalent, then a fixpoint is reached, and we let F(A) := Vseso (?C. #(s)). if a fLxpoint
is reached within a finite number of iterations, then the linear formula F(A) correctly defines the
desired set of parameter valuations. This gives us a semidecision procedure for solving the emptiness
problem for parametric timed automata. Also, techniques for linear programming can be used to
obtain parameter values that are optimal with respect to (linear) cost functions.
Termination of the fixpoint computation is, however, not guaranteed in general. For instance,
the procedure will not terminate for the autoniaton of Figure 1. This is because for ? > 1, (?, v) e
?i(51) iff ?(c) equals (i --H 1) . ?(a) + ?(b). ?ence for all > 1 the formulas ?i+1(51) and ?i(51)
are inequivalent, and the fixpoint is never reached. Notice that even if the parameters a and b are
replaced by constants, the fixpoint computation will not terminate. Thus the procedure cannot be
used to decide the emptiness problem even in the case of a single parametrically constrained clock.
The fixpoint computation does terminate in many cases of practical interest, including the
following example with two parametrically constraint clocks.
Verification example: timing-based mutual exclusion
We consider Fischer's protocol for mutual exclusion [Lam87]. The mutual-exclusion problem is to
design a protocol that guarantees mutually exclusive access to a critical section among competing
processes P1 and P2. Fischer proposed a very simple protocol that exploits the knowledge about
the timing delays of a system. In this protocol, a shared variable lock is used for communication;
initially lock has the value 0. Each process Pj, ? = 1, 2, follows the following algorithm whenever it
wants access to the critical section:
repeat
await lock = 0; lock :=
until lock =
Critical section;
lock := 0
The correctness of this protocol depends on the assumptions about the time taken by each read
and write operation. Suppose that for each process, the read operation in the test lock = i has
a delay in the interval (a,b), and the write operation in the assignment lock := i has a delay in
11
null
Automaton for P_1
set(O), set(O)'
set(2)'
set(2)'
set(l)
set(O)'
is(O), is(O)'			is(l), is(l)'			is(2),is(2)'
Automaton for lock
Figure 4: Timing-based mutual exclusion
the interval (c, d), The protocol can then be modeled by a product of three component automata
with two parametrically constrained clocks, one for each process, The component automata are
shown in Figure 4, There is one automaton Aj for each process Pj, and an automaton Alock for the
shared variable lock. For process P1, there is an idling event null, and for each possible value j of
the variable, there is a read event is(j) and a write event set(j). Process P2 has analogous primed
events.
The mutual-exclusion requirement asserts that it should never be the case that the automaton
A1 is in state 4 at the same time as the automaton A2 is in its state 4, To test the mutual-exclusion
property we obtain an automaton A from the product A1 ? A2 ? Alock by requiring that a state
(si, 52,53) of the product is an accepting state iff si = 4 and 52 = 4, Then a parameter valuation
? is consistent with A iff the mutual-exclusion property is violated, While the decision procedure
of Subsection 3.1 does not apply in this case, the fixpoint computation procedure outlined above
will terminate. By symbolic computation we can thus derive the necessary and sufficient parameter
constraint that ensures mutual exclusion: ? E F(A) iff ?(d) > ?(a),
3.3 The Gap between Decidability and Undecidability
We proved that testing the emptiness of F(A) is undecidable if A contains three clocks, and decidable
if A contains one clock. It is an open question whether testing the emptiness of F(A) is decidable
if A contains two clocks. Note that two clocks are sufficient to give rise to complex nonlinear
constraints, as is the case for the automaton of Figure 1, To illustrate the hardness of the two-clock
emptiness problem, we present some intriguing connections with difficult and open problems in
logic and automata theory,
Presburger arithmetic with divisibility
In [Lip78j, Lipshitz gives an algorithm for deciding the satisfiability of quantifler-free formulas
involving addition and the divisibility relation over the natural numbers, Our problem is at least
as hard.
12
THEOREM [Existential Presburger arithmetic with divisibility]. Let (p be a quantifier
free formula over the primitives of addition, the integer divisibility relation, comparisons, and
integer constants, and let T = N. ?`e can construct a parametric timed automaton A? with two
clocks such that the formula ? is satisfiable over the natural numbers iff L(A) is nonempty. I
PRooF. First we transform the formula ? into a formula ? such that ? is satisfiable iff ? is
satisfiable, and ? is a positive boolean combination of atoms of the form (? = a), ? < a, aib, and
?(aIb), where ? is a linear term (with positive coefficients), and a, b are variables with b > 0. This
can be achieved in a straightforward way by introducing extra variables.
We now construct a parametric timed automaton A?? with two clocks x and y such that the
parameters of A?? are the variables of ?. For an atom 4Y = (kiai + ... + krnarn + km+i = a), the
automaton A? consists of a single path whose transition labels form the following sequence:
(x,y := 0); (x = a1,x := 0)ki.x = am,x := 0)km; (x = km+1,Y = a).
Atoms of the form (? < a) are handled similarly. For an atom `y' = (aib), the automaton A? is
(r,y := 0);(x = a, x := o)*;(x = a, y =
resembling the automaton of Figure 1. The atom ? = ?(aIb) is equivalent to (a > b) v ?`, where
= ?(aIb) A a < b. The automaton A4 is
(x,y:= 0);(x=a,y? b,x:=0);(r= a,y> b).
Disjunction corresponds to nondeterminism, and conjunction corresponds to sequential composition
of automata. ?
While in certain cases, given a parametric timed automaton A, we can construct a formula
bA that characterizes F(A), and then use Lipshitz's algorithm to test the emptiness of F(A), the
reduction from parametric timed automata with two clocks to existential Presburger arithmetic
with divisibility does not seem to exist in general.
A restricted class of i-register machines
We consider a simple class of (nondeterministic) i-register machines. Such a machine consists of a
finite-state control and one register that can hold any integer value. The input to the machine is an
interpretation ? that assigns natural numbers to a finite set P of input variables; the initial value
of the register is 0. Each instruction can add one of the input variables to the register, subtract one
of the input variables from the register, or nondeterministically change the location of the control
depending on whether the register value is negative, zero, or positive. The machine accepts the
input ? iff a sequence of instructions leads from an initial state to a final state.
A i-register machine is restricted iff whenever an input variable is added to the register, the
resulting register value must be nonnegative, and whenever an input variable is subtracted, the
resulting register value must be nonpositive. We can reduce the emptiness problem for restricted
i-register machines to the emptiness problem for parametric timed automata with two clocks.
THEoREM [Restricted i-register machines]. Given a restricted i-register machine M with
k input variables, we can construct a parametric timed automaton AAf with two clocks and k
parameters such that M accepts an input ? iff ? e F(A). I
PRooF. The automaton AM has two clocks, x and y, and a state for each control location of the
i-register machine M. The value of the register is encoded by the clock difference x--Hy. The register
13
machine instruction that adds (or subtracts) the input variable a to the register corresponds, then,
to a transition labeled with (y = a, y 0) (or (x = a, x := 0), respectively). Transition labels of
the form (x y), for N? ?=, <, >?, which correspond to test instructions, can be eliminated by
duplicating each state so that all states have at most one incoming transition. I
In certain cases, given a parametric timed automaton A, we can construct a restricted 1-
register machine MA that accepts F(A), and thus reduce the emptiness problem for parametric
timed automata with two clocks to the emptiness problem for restricted 1-register machines. A
recent result in [IJTW93] shows that the emptiness problem is decidable for deterministic restricted
i-register machines. The problem is still open for nondeterministic restricted i-register machines.
References
[ACD9Oj R. Alur, C. Courcoubetis, and D.L. Dill. Model-d?cking for real-time systems. In
Proc. 5th JEFE LICS, 1990.
[ACHH93]
R. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho. Hybrid automata: An algorith-
mic approach to the specifIcation and verification of hybrid systems. In Proc. ?Vorkshop
on Theory of Hybrid Systems, LNCS. Springer, 1993. To appear.
[AD9O] R. Alur and D.L. Dill. Automata for modeling real-time systems. In Proc. 17th ICALP,
LNCS 443. Springer, 1990.
[ADLS9l] H. Attiya, C. Dwork, N. Lynch, and L. Stockmeyer. Bounds on the time to reach
agreement in the presence of timing uncertainty. In Proc. 23rd ACM STOC, 1991.
[AFH9l] R. Alur, T. Feder, and T.A. Heuzinger. The benefits of relaxing punctuality. in
Proc. 10th ACM PODC, 1991.
[AH89] R. Alur and T.A. Henzinger. A really temporal logic. In Proc. 30th IEEE FOCS, 1989.
[AH9O] R. Alur and T.A. Henzinger. Real-time logics: Complexity and expressiveness. In
Proc. 5th IFEE LICS, 1990.
[AH92] R. Alur and T.A. Henzinger. Back to the future: Towards a theory of timed regular
languages. in Proc. 33rd IEEE FOCS, 1992.
[AL92j M. Abadi and L. Lamport. An old-fashioned recipe for real time. In Proc. REX Work-
shop on Real Time, LNCS 600. Springer, 1992.
[Alu91] R. Alur. Techniques for Automatic Venfication of Real-time Systems. PhD thesis,
Stanford Univ., 1991.
[CY91] C. Courcoubetis and M. Yannakakis. Minimum and maximum delay problems in real-
time systems. in Proc. 3rd CAV, LNCS 575. Springer, 1991
[Dil89] D.L. Dill. Timing assumptions and verification of finite-state concurrent systems. in
Proc. 1st CAV, LNCS 407. Springer, 1989.
[EMSS9Oj E.A. Emerson, A.K. Mok, A.P. Sistla, and J. Srinivasan. Quantitative temporal rea-
soning. in Proc. 2nd CAV, LNCS 531. Springer, 1990.
[End72] H. Enderton. A Alathematical Introduction to Logic. Academic Press, 1972.
14
[11en91] T.A. llenzinger. The Temporal Specification and Verification of Real-time systems. PliD
thesis, Stanford Univ., 1991.
[HLP9O] E. Harel, 0. Liclitenstein, and A. Pnueli. Explicit-clock temporal logic. In Proc. 5th
IEEE LICS, 1990.
[HNSY92] T.A. Henzinger, X. Nicollin, J. Sifakis, and 5. Yovine. Symbolic model-checking for
real-time systems. In Proc. 7th JEEE LICS, 1992.
[Hoo91] J. Hooman. Specification and compositional verification of real-time systems. LNCS
558. Springer, 1991.
[IJTW93j 0. Ibarra, T. Jiang, N Tran and H. Wang. New decidability results concerning two-
way counter macbines and applications. In Proc. 20th ICALP, LNCS. Springer, 1993.
To appear.
[Jah89] E. Jahanian. Verifying properties of systems with variable timing constraints. In
Proc. 10th IFEE RTSS, 1989.
[Koy90] R. Koymans. Specifying real-time properties with metric temporal logic. J. Real-time
Systems, 2:255--H299,1990.
[Kur90] R. P. Kurshan. Analysis of discrete-event coordination. In LATCS 430. Springer, 1990.
[Lam87j L. Lamport. A fast mutual exclusion algontlim. ACAf Trans. Computer Systems, 5:1-
11, 1987.
[Lew9O] H.R. Lewis. A logic of concrete time intervals. In Proc. 5th JEEE LICS, 1990.
[Lip78] L. Lipshitz. The diopliantine problem for addition and divisibility. Trans. AAIS,
235:271--H283,1978.
[L585]
N. Leveson and J. Stolzy. Analyzing safety and fault tolerance using timed Petri nets.
In Proc. Int. Conf. Theory and Practice of Safiware Development, LNCS 186. Spnnger,
1985.
[MP92] Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems.
Springer, 1992.
[Ost90] J. Ostroff. Temporal Logic of Real-time Systems. Research Studies Press, 1990.
[5BM92] F.B. Schneider, B. Bloom, and K. Marzullo. Putting time into proof outlines. In
Proc. REX Workshop on Real Time, LNCS 600. Springer, 1992.
[5DC90] R. Strong, D. Dolev, and V. Cristian. New latency bounds for atomic broadcast. In
Proc. 11th IEEE RTSS, 1990.
[VW86] M.Y. Vardi and P. Wolper. An automata-theoretic approach to autornatic program
verification. In Proc. 1st IEEE LICS, 1986.
[WME92] V. Wang, A.K. Mok, and E.A. Emerson. Real-time distributed system specification and
venfication in APTL. In Proc. 12th Int. Conf. Software Engineering, 1992.
[WZ92] H.B. Weinberg and L.D. Zuck. Timed Ethernet: Real-time formal specification of
Ethernet. In Proc. 3rd CONCUR, LNCS 630. Springer, 1992.
15
