Parametric Analysis of Computer Systems.
A general parametric analysis problem which allows the use of parameter variables in both the real-time automata and the specifications is proposed and solved. The analysis algorithm is much simpler and can run more efficiently in average cases than can previous works.
Introduction
A successful real-world project management relies on the satisfaction of various timing and nontiming restraints
which may compete with each other for resources. Examples of such restraints include timely re-
sponses, budget, domestic or international regulations, system configurations, environments, compatibilities,
In this work, we define and algorithmically solves the parametric analysis problem of computer systems
which allows for the formal description of system behaviors and design requirements with various timing and
nontiming parameter variables and asks for a general conditions on all solutions to those parameter variables.
The design of our problem was influenced by previous work of Alur et al. [AHV93] and Wang [Wang95]
which will be discussed briefly later. Our parametric analysis problem is presented in two parts : an automaton
with nontiming parameter variables and a specification with both timing and nontiming parameter
variables. The following example is adapted from the railroad crossing example and shows how such a
platform can be useful.
The popular railroad crossing example consists of a train monitor and gate-controller. In figure 1, we give
a parametric version of the automaton descriptions of the monitor and controller respectively. The ovals
represent meta-states while arcs represent transitions. By each transition, we label the transition condition
and the clocks to be reset to zero on the transition. The global state space can be calculated as the Cartesian-
product of local state spaces.
The safety requirement is that whenever a train is at the crossing, the gate must be in the D mode (gate
is down). The more money you spend on monitor, the more precise you can tell how far away a train is
approaching. Suppose we now have two monitor types, one costs 1000 dollars and can tell if a train is coming
to the crossing in 290 to 300 seconds; the other type costs 500 and can tell if a train is coming to the crossing
in 200 to 350 seconds.
We also have two gate-controller types. One costs 900 dollars and can lower the gate in 20 to 50 seconds
and skip the U mode (gate is up) when a train is coming to the crossing and the controller is in the R mode
(gate-Raising mode). The other type costs 300 dollars and can lower the gate in 100 to 200 seconds and
cannot skip the U mode once the controller is in the R mode.
Suppose now the design of a rail-road crossing gate-controller is subjected to the budget constraint : the
cost of the monitor ($ M ) and that of controller ($ C ) together cannot exceed 1500 dollars. We want to make
sure under this constraint, if the safety requirement can still be satisfied. This can be expressed in our logic
Monitor
U
Controller
A
R

Figure

1: Railroad Gate Controller Example
D). Here 82 is a modal operator from CTL [CE81, CES86] which
means for all computations henceforth, the following statement must be true. k
Our system behavior descriptions are given in statically parametric automata (SPA) and our specifications
are given in parametric computation tree logic (PCTL). The outcome of our algorithm are Boolean expressions,
whose literals are linear inequalities on the parameter variables, and can be further processed with standard
techniques like simplex, simulated extract useful design feedback.
In the remainder of the introduction, we shall first briefly discuss related work on the subject, and then
sketch an outline of the rest of the paper.
1.1 Related work
In the earliest development [CE81, CES86], people use finite-state automata to describe system behavior and
check to see if they satisfy specification given in branching-time temporal logic CTL. Such a framework is
usually called model-checking. A CTL (Computation Tree Logic) formula is composed of binary propositions
Boolean operators (:; -), and branching-time modal operators (9U ; 9fl; 8U ; 8fl). 9 means
"there exists" a computation. 8 means "for all" computations. U means something is true "until" something
else is true. fl means "next state." For example, 9pUq says there exists a computation along which p is true
until q is true. Since there is no notion of real-time (clock time), only ordering among events are considered.
The following shorthands are generally accepted besides the usual ones in Boolean algebra. 93OE 1 is for
9true U Intuitively 3 means "eventually"
while 2 means "henceforth."
CTL model-checking has been used to prove the correctness of concurrent systems such as circuits and
communication protocols. In 1990, the platform was extended by Alur et al. to Timed CTL (TCTL) model-checking
problem to verify dense-time systems equipped with resettable clocks [ACD90]. Alur et al. also
solve the problem in the same paper with an innovative state space partitioning scheme.
In [CY92], the problems of deciding the earliest and latest times a target state can appear in the computation
of a timed automaton was discussed. However, they did not derive the general conditions on parameter
variables.
In 1993, Alur et al. embark on the reachability problem of real-time automata with parameter variables
[AHV93]. Particularly, they have established that in general, the problem has no algorithm when three clocks
are compared with parameter variables in the automata [AHV93]. This observation greatly influences the
design of our platform.
In 1995, Wang propose another platform which extends the TCTL model-checking problem to allow for
timing parameter variables in TCTL formulae [Wang95]. His algorithm gives back Boolean conditions whose
literals are linear equalities on the timing parameter variables. He also showed that his parametric timing
analysis problem is PSPACE-hard while his analysis algorithm is of double-exponential time complexity.
Henzinger's HyTech system developed at Cornell also has parametric analysis power[AHV93, HHWT95].
However in their framework, they did not identify a decidable class for the parametric analysis problem and
their procedure is not guaranteed to terminate. In comparison, our framework has an algorithm which can
generate the semilinear description of the working solutions for the parameter variables.
1.2 Outline
Section 2 presents our system behavior description language : the Statically Parametric Automaton (SPA).
Section 3 defines Parametric Computation Tree Logic (PCTL) and the Parametric Analysis Problem. Section
4 presents the algorithm, proves its correctness, and analyzes its complexity. Section 5 concludes the
paper.
We also adopt N and R + as the sets of nonnegative integers and nonnegative reals respectively.
Statically parametric automata (SPA)
In an SPA, people may combine propositions, timing inequalities on clock readings, and linear inequalities of
parameter variables to write the invariance and transition conditions. Such a combination is called a state
predicate and is defined formally in the following. Given a set P of atomic propositions, a set C of clocks,
and a set H of parameter variables, the syntax of a state predicate j of P , C, and H, has the following syntax
rules.
a
are state predicates. Notationally,
we let B(P; C; H) be the set of all state predicates on P , C, and H. Note the parameter variables considered
in H are static because their value do not change with time during each computation of an automaton. A
state predicate with only
a literals is called static.
Statically Parametric Automata
A Statically Parametric Automaton (SPA) is a tuple (Q; -) with the following restrictions.
ffl Q is a finite set of meta-states.
is the initial meta-state.
ffl P is a set of atomic propositions.
ffl C is a set of clocks.
ffl H is a set of parameters variables.
function that labels each meta-state with a condition true in that meta-state.
Q is the set of transitions.
defines the set of clocks to be reset during each transition.
defines the transition triggering conditions. k
An SPA starts execution at its meta-state q 0 . We shall assume that initially, all clocks read zero. In between
meta-state transitions, all clocks increment their readings at a uniform rate. The transitions of the SPA may
be fired when the triggering conditon is satisfied. With different interpretation to the parameter variables,
it may exhibit different behaviors. During a transition from meta-state q i to q j , for each x 2 ae(q
reading of x will be reset to zero. There are state predicates with parameter variables on the states as well as
transitions. These parameters may also appear in the specifications of the same analysis problem instance.
A state s of SPA -) is a mapping from P [ C to ftrue; falseg [ R + such that for
each for each x 2 C, s(x) is the set of nonnegative real
numbers. k
The same SPA may generate different computations under different interpretation of its parameter vari-
ables. An interpretation, I, for H is a mapping from N [H to N such that for all c 2 N ,
-) is said to be interpreted with respect to I, when all state predicates in A have
their parameter variables interpreted according to I.
Satisfaction of interpreted state predicates by a state
predicate j is satisfied by state s under interpretation I, written as s
a
a
Now we are going to define the computation of SPA. For convenience, we adopt the following conventions.
An -) is unambiguous iff for all states s, there is at most one q 2 Q such
that for some I, s Ambiguous SPA's can be made unambiguous by incorporating meta-state names
as propositional conjuncts in the conjunctive normal forms of the -state predicate of each meta-state. For
convenience, from now on, we shall only talk about unambiguous SPA's. When we say an SPA, we mean an
unambiguous SPA.
Given an SPA - ), an interpretation I for H, and a state s, we let s Q be the
meta-state in Q such that s there is no meta-state q 2 Q such that s
undefined.
Given two states s; s 0 , there is a meta-state transition from s to s 0 in A under interpretation I, in symbols
are both defined,
Also, given a state s and a ffi be the state that agrees with s in every aspect except for
all
of interpreted SPA
Given a state s of SPA -) and an interpretation I, a computation of A starting
at s is called an s-run and is a sequence ((s of pairs such that
ffl for each t there is an i 2 N such that t i - t; and
ffl for each integer i - 1, s Q
i is defined and for each real 0 -
ffl for each i - 1, A goes from s i to s i+1 because of
- a meta-state transition, i.e. t
3 PCTL and parametric analysis problem
Parametric Computation Tree Logic (PCTL) is used for specifying the design requirements and is defined
with respect to a given SPA. Suppose we are given an SPA
OE for A has the following syntax rules.
Here j is a state predicate in B(P; C; H), OE 1 and OE 2 are PCTL formulae, and ' is an element in N [ H.
Note that the parameter variable subscripts of modal can also be used as parameter variables
in SPA. Also we adopt the following standard shorthands
for
8true U-' OE 1 , 92-' OE 1 for :83-':OE 1 .
With different interpretations, a PCTL formula may impose different requirements. We write in notations
s I OE to mean that OE is satisfied at state s in A under interpretation I. The satisfaction relation is defined
inductively as follows.
ffl If OE is a state predicate, then s I OE iff OE is satisfied by s as a state predicate under I.
there are an in A, an i - 1, and a
s.t.
- for all
- for all
- for all
- for all
Given an SPA A, a PCTL formula OE, and an interpretation I for H, we say A is a model of OE under I,
written as A j= I OE, iff s I OE for all states s such that s
We now formally define our problem.
Statically Parametric Analysis Problem
Given an SPA A and a specification (PCTL formula) OE, the parametric analysis problem instance for A
and OE, denoted as PAP(A, OE), is formally defined as the problem of deriving the general condition of all
interpretation I such that A j= I OE. I is called a solution to PAP(A; OE) iff A
We will show that such conditions are always expressible as Boolean combinations of linear inequalities of
parameter variables.
4 Parametric analysis
In this section, we shall develop new data-structures, parametric region graph and conditional path graph,
to solve the parametric analysis problem. Parametric region graph is similar to the region graph defined in
[ACD90] but it contains parametric information. A region is a subset of the state space in which all states
exhibit the same behavior with respect to the given SPA and PCTL formula.
Given a parametric analysis problem for A and OE, a modal subformula OE 1 of OE, and the parametric region
(v; v)
(v; w)

Figure

2: Railroad Gate Controller Example
graph with region sets V , the conditional path graph for OE 1 is a fully connected graph of V whose arcs
are labeled with sets of pairs of the form : (-; T ) where - is a static state predicate and T is an integer
set. Conveniently, we call such pairs conditional time expressions (CTE). Alternatively, we can say that the
conditional path graph J OE 1
for OE 1 is a mapping from V \Theta V to the power set of CTE's. For a v; v
is satisfied by I, then there is a finite
s-run of time t ending at an s 0 2 v 0 such that OE 1 is satisfied all the way through the run except at s 0 . In
subsection 4.2, we shall show that all our modal formula evaluations can be decomposed to the computation
of conditional time expressions.
The kernel of this section is a Kleene's closure procedure which computes the conditional path graph. Its
computation utilizes the following four types of integer set manipulations.
g.
g.
means the addition of i consecutive T 1 .
is the complement of T 1 , i.e., g.
It can be shown that all integer sets resulting from such manipulations in our algorithm are semilinear. 1
Semilinear expressions are convenient notations for expressing infinite integer sets constructed regularly.
They are also closed under the four manipulations. There are also algorithms to compute the manipulation
results. Specifically, we know that all semilinear expressions can be represented as the union of a finite
number of sets like a + c . Such a special form is called periodical normal form (PNF). It is not difficult to
prove that given operands in PNF, the results of the four manipulations can all be transformed back into
PNF. Due to page-limit, we shall skip the details here.
The intuition behind our algorithm for computing the conditional path graph is a vertex bypassing scheme.
Suppose, we have three regions u; v; w whose connections in the conditional path graph is shown in Figure 2.
Then it is clear that by bypassing region v, we realized that J OE 1
should be a superset of
(v; w); D ' J OE 1
(v; v)g
Our conditional path graph construction algorithm utilizes a Kleene's closure framework to calculate all the
arc labels.
In subsection 4.1, we kind of extend the regions graph concepts in [ACD90] and define parametric region
graph. In subsection 4.2, we define conditional path graph, present algorithm to compute it, and present
our labelling algorithm for parametric analysis problem. In subsections 4.3 and 4.4, we briefly prove the
seminlinear integer set is expressible as the union of a finite number of integer sets like
for some a;
algorithm's correctness and analyze its complexity.
4.1 Parametric region graph
The brilliant concept of region graphs were originally discussed and used in [ACD90] for verifying dense-time
systems. A region graph partitions its system state space into finitely many behavior-equivalent subspaces.
Our parametric region graphs extend from Alur et al's region graph and contains information on parameter
variable restrictions. Beside parameter variables, our parametric region graphs have an additional clock -
which gets reset to zero once its reading reaches one. - is not used in the user-given SPA and is added when
we construct the regions for the convenience of parametric timing analysis. It functions as a ticking indicator
for evaluating timed modal formulae of PCTL. The reading of - is always between 0 and 1, that is, for every
state s, 0 - s(- 1.
The timing constants in an SPA A are the integer constants c that appear in conditions such as
and x - c in A. The timing constants in a PCTL formula OE are the integer constants c that appear in
subformulae like x \Gamma y - c; x - c; 9OE 1 U-c OE 2 , and 8OE 1 U-c OE 2 . Let KA:OE be the largest timing constant used in
both A and OE for the given parametric analysis problem instance.
For each ffi 2 R + , we define fract(ffi) as the fractional part of ffi, i.e.
Regions
Given an SPA -) and a PCTL formula OE for A, two states s; s 0 of A, s - =A:OE s 0
(i.e. s and s 0 are equivalent with respect to A and OE) iff the following conditions are met.
ffl For each
ffl For each x \Gamma y - c used in A or OE,
ffl For each
ffl For every x; y
[s] denotes the equivalent class of A's states, with respect to relation - =A:OE , to which s belongs and it is called
a region. k
Note because of our assumption of unambiguous SPA's, we know that for all s Using the
above definition, parametric region graph is defined as follows.
Graph (PR-graph)
The Parametric Region Graph (PR-graph) for an SPA -) and a PCTL formula
OE is a directed graph such that the vertex set V is the set of all regions and the arc set F
consists of the following two types of arcs.
ffl An arc (v; v 0 transitions in A. That is, for every s 2 v, there is an s
such that s ! s 0 .
ffl An arc (v; v 0 ) may be a time arc and represent passage of time in the same meta-state. Formally, for
every s 2 v, there is an s 0 2 v 0 such that
- there is no -
s and -
s, and
Just as in [Wang95], propositional value-changings within the same meta-states are taken care of automatically

For each (v; v 0 ) in F , we let ffl(v; v 0 ) =" if going from states in v to states in v 0 , the reading of - increments
from a noninteger to an going from states in v to states in v 0 , the reading of - increments
from an integer to a noninteger; otherwise ffl(v; v 0 is an
KClosure OE 1
/* It is assumed that for all regions v 2 V , we know the static state predicate condition L OE 1 (v) which makes
1 satisfied at v. */
f
(1) For each (v; w) 2 F , if ffl(v; w) =", f
(2) else let J OE 1
0)g.
(2) for each v 2 V , do f
(1) for each u; w
(v; w);

Table

1: Construction of the conditional path graph
integer.
Also we conveniently write v Similarly,
we let v Q be the meta-state such that for all s 2 v(v
Since regions have enough informations to determine the truth values all propositions and clock inequalities
used in a parametric analysis problem, we can define the mapping from state predicates to static state
predicates through a region. Formally, given a region v and a state predicate j, we write v(j) for the static
predicate constructed according to the following rules.
ffl v(false) is false.
ffl v(p) is true iff 8s 2
c) is false otherwise.
c) is false otherwise.
a
a
For convenience, we let h-iv be the region in a PR-graph that agrees with v in every aspect except that for
all Given a PCTL formula OE and a path is called a OE-path
(OE-cycle) iff there is an interpretation I such that for each 1 -
4.2 Labeling Algorithm
To compute the parametric condition for a parametric modal formula like 9OE 1 U-' OE 2 at a region, we can
instead decompose the formula into a Boolean combinations of path conditions and then compute those path
conditions. For example, suppose under interpretation I, we know there exists a OE 1 -path v 1
Then a sufficient condition for all states in v 1 satisfying 9OE 1 U-' OE 2 is that I(') - 5-v n
Now we define our second new data structure : conditional path graph to prepare for the presentation of the
algorithm.
Conditional path graph
Given a region graph of OE, the conditional path graph for OE 1 , denoted as
is a mapping from V \Theta V to the power set of conditional time expressions such that for all v; v
there is a finite s-run of time
t ending at an s 0 2 v 0 such that OE 1 is satisfied all the way through the run except at s 0 . k
The procedure for computing J OE 1
() is presented in table 1. Once the conditional path graph has been
constructed for using KClosure OE 1
(), we can then turn to the labeling algorithm in table 2 to calculate
the parametric conditions for the modal formulas properly containing OE 1 . However, there is still one thing
which we should define clearly before presenting our labeling algorithm, that is : "How should we connect
the conditional time expressions in the arc labels to parametric conditions ?" Suppose, we want to examine
if from v to v 0 , there is a run satisfying the parametric requirement of - '. The condition can be derived
as
expressions T in PNF and (numerical or variable)
parameter ' is calculated according to the following rewriting rules.
is a new integer variable never used before.
Note since we assume that the operands are in PNF, we do not have to pay attention to the case of +;  ; .

Table

2 presents the labeling alogrithm for L OE (v). This algorithm maps pairs of vertices and temporal
logic formulas to a Boolean combination of linear inequalities with parameter variables as free variables. Also
note the labeling algorithm relies on the special case of 92-0 OE j which essentially says there is an infinite
computation along which OE j is always true.
Also the presentation in table 2 only covers some typical cases. For the remaining cases, please check the
appendix.
4.3 Correctness
The following lemma establishes the correctness of our labeling algorithm.
Given PAP(A; OE), an interpretation I for H, and a vertex v in GA:OE , after executing L OE (v) in
our labeling algorithm, I satisfies L OE (v) iff v
proof : The proof follows a standard structural induction on OE, which we often saw in related model-checking
literature, and very much resembles the one in [Wang95]. Due to page-limit, we shall omit it here. k
4.4 Complexity
According to our construction, the number of regions in GA:OE , denoted as jG A:OE j, is at most 3jQj
coefficient 3 and constant +1 reflect the introduction of ticking indicator -. The
inner loop of KClosure OE 1
will be executed for jG A:OE j 3 times. Each iteration takes time proportional to
(v; w)j2 jJ OE 1 (v;v)j . The conditional path graph arc labels, i.e. J OE 1
roughly corresponds to
the set of simple paths from u to v, although they utilize the succinct representation of semilinear expressions.
Thus according to the complexity analysis in [Wang95], we find that procedure KClosure OE 1
() has complexity
doubly exponential to the size of GA:OE , and thus triply exponential to the size of input, assuming constant
time for the manipulation of semilinear expressions.
We now analyze the complexity of our labeling procedure. In table 2, procedure L OE i () invokes KClosure OE j ()
at most once. Label(A; OE) invokes L OE i () at most jGA jjOEj times. Thus the complexity of the algorithm is
roughly triply exponential to the size of A and OE, since polynomials of exponentialities are still exponential-
ities.
Finally, PCTL satisfiability problem is undecidable since it is no easier than TCTL satisfiability problem[ACD90].
(1) construct the PR-graph
(2) for each v 2 V , recursively compute L OE (v);
case (false), L false (v) := false;
case (p) where
case or y is zero in v, evaluate x \Gamma y - c as in the next case; else x \Gamma y - c is evaluated
to the same value as it is in any region u such that (u; v) 2 F .
case
case ( P
a
a
a
case
case
case
(1) KClosure OE j (V; F );
(2) let L 92-0 OE j (v) be W
ii W
case
(1) KClosure OE j (V; F );
(2) let L 9OE j U-' OE k (v) be W
ii W
case
These cases are treated in ways similar to the above case and are left in table ?? which is appended at the
end of the paper.
case
(1) KClosure OE j (V; F );
(2) let L 8OE j U-' OE k (v) be
case
These cases are treated in ways similar to above case and are left in table ?? which is appended at the end
of the paper.

Table

2: Labeling algorithm
5 Conclusion
With the success of CTL-based techniques in automatic verification for computer systems [Bryant86, BCMDH90,
HNSY92], it would be nice if a formal theory appealing to the common practice of real-world projects can
be developed. We feel hopeful that the insight and techniques used in this paper can be further applied to
help verifying reactive systems in a more natural and productive way.

Acknowledgements

The authors would like to thank Prof. Tom Henzinger. His suggestion to use dynamic programming to solve
timing analysis problem triggered the research.



--R


"Automata, Languages and Programming: Proceedings of the 17th ICALP,"
"Proceedings, 5th IEEE LICS."
"Proceedings, 25th ACM STOC,"
Symbolic Model Checking: 10 20 States and Beyond

"Proceedings, Workshop on Logic of Programs,"
Automatic Verification of Finite-State Concurrent Systems using Temporal-Logic Specifications
"Proceedings, 3rd CAV,"
the next generation.
Symbolic Model Checking for Real-Time Systems
"Proceedings, 10th IEEE Symposium on Logic in Computer Science."
--TR
Automatic verification of finite-state concurrent systems using temporal logic specifications
Graph-based algorithms for Boolean function manipulation
Automata for modeling real-time systems
Parametric real-time reasoning
Model-checking in dense real-time
Parametric timing analysis for real-time systems
Minimum and Maximum Delay Problems in Real-Time Systems
Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic
HYTECH

--CTR
Farn Wang , Hsu-Chun Yen, Reachability solution characterization of parametric real-time systems, Theoretical Computer Science, v.328 n.1-2, p.187-201, 29 November 2004
real-time systems;parameters;verification;model-checking