Parosh Abdulla
Jurgen Giesl
Radu Grosu
Neil Jones
Orna Kupferman
Kim Larsen
Chin Soon Lee
Axel Legay
Berhard Steffen
Wang Yi
On Model Checking of Parameterized Timed Systems
Parosh Abdulla
We consider verification of safety properties for parameterized
systems of timed processes, so called timed networks.
A timed network consists of a finite state process, called a controller,
and an arbitrary set of identical timed processes.
We show that checking safety properties and some simple classes of liveness
properties are decidable in the case where each timed process is equipped
with a single realvalued clock.
We show that these problems become undecidable when each
timed process has two clocks.
On the other hand, we show that the problems are decidable when clocks
range over a discrete time domain. The decidability results hold when
processes have any finite number of clocks.
Termination and Liveness in Term Rewriting
Juergen Giesl
RWTH Aachen
Germany
A "liveness property" states that eventually (after a finite number of steps)
some requirement holds. One of the most essential liveness properties in
software verification is termination. Methods for automated termination
analysis have been studied for decades in areas like logic programming and
term rewriting. We give an overview on techniques to prove termination
of term rewrite systems automatically. Starting from classical
approaches, we also present new methods like the "dependency pair" approach,
which extends the applicability of classical techniques for automated
termination analysis significantly. The talk also includes a demonstration
of our automated termination prover AProVE which illustrates that the techniques
discussed can be mechanized efficiently.
Moreover, we demonstrate that techniques for termination analysis are also useful
to verify other liveness properties as well. To this end, we show how
dependency pairs were applied at Ericsson Telecom in order to verify
liveness properties of a protocol for concurrent telecommunication processes.
Monte Carlo Model Checking
Radu Grosu
SUNY at Stony Brook
Joint work with Scott Smolka.
We present what we believe to be the first randomized, Monte Carlo
algorithm for model checking, the problem of deciding whether or not a
property specified in temporal logic holds of a system specification.
Given an epsilon, delta, a succinct representation S of the system
under investigation, and a Linear Temporal Logic formula varphi, our
algorithm computes an estimate of the probability that S satisfies
varphi within a factor of 1 +/ epsilon with probability at least 1 
delta. It does so using a number of samples N that is optimal to within
a constant factor, and in expected time O(N*(S+varphi)) and
expected space O(S+varphi).
Safety and Liveness in Critical Software (from a grant
application)
Neil Jones
Real software in application areas, such as avionic
controls, primarily concerns {\em reactive systems} that are intended
to run indefinitely in acontext of continual interactions,e.g., with
an operatingsystem, with the outside world via sensors/actuators, and
with inputs provided online by humans.
{\em Safety properties} ensure that nothing can go wrong (e.g.,divide
by zero or dereference an invalid pointer), and {\em
livenessproperties} ensure that the system will continue to
provideservices, and thus be responsive (rather than loop indefinitely
or ignorecertain kinds of requests).
We propose to develop and experiment with {\em resourceusage
analyses}wellsuited to the kinds of problems of interest to real
software systems,in particular unboundedness of resource
usage. Resourceusage analyses will require detection methods stronger
than traditional abstract interpretation or program flow analysis in
optimising compilers. Some relevant concepts come from
modelchecking(although it is most often applied to circuits and
embedded systems).Safety and liveness cannot be studied in isolation,
since (un)safety can have an impact on liveness. Roughly: an unsafe
systemthat crashes due to a single illegal operation can no longer
respond, and is thus no longer live. Further, an {\em unbounded
usage} of a limited resource will {\em eventually compromise liveness
by violating safety}, once an overrun occurs. Such ``overflow'' can be
of: stack or heap size, buffer size, or integer or floating point word
sizes.The core problem is how to detect potentially unbounded resource
usage. This is not solvable in practice by assigning fixed a priori
limits to buffer length, stack size, etc. since the number of
possibleconfigurations in real systems is far too large to analyse
exhaustively.We plan to address some problems by analytic and
typebased methods: Program termination (stronger, and applicable to
more programs).  Avoiding unboundedness in values of variables.
Avoiding unboundedness in stack and heap usage. Bounding program
running times. A novel program analysis that is particularly relevant
is ``quasitermination analysis.'' This analysis determines whether a
program, for every one of its inputs, executes within a finite total
state space, and therefore can be executed if given sufficiently large
resources.

Relating Liveness and Probability
Orna Kupferman
Joint work with Marcin Jurdzinski and Thomas Henzinger
Two basic liveness properties are reachability (T holds eventually)
and repeated reachability (T holds infinitely often). The talk relates
reachability in a probabilistic setting with repeated reachability in
a nonprobabilistic setting. Intuitively, requiring an event T to hold
eventually with probability 1 has the same flavor as requiring events
that lead to T to hold infinitely often. The intuition can be
formalized by means of reductions between probabilistic reachability
games and nonprobabilistic repeated reachability games. The above
phenomenon of probability being traded for a stronger fairness
condition, and viceversa, is general, and can be shown for other
fairness conditions.
Reachability Testing, Liveness and Beyond for Timed Automata
Kim Larsen
A Worstcase Quadratictime Approximation of Sizechange Termination
Chin Soon Lee
The "sizechange" approach for termination analysis of firstorder
functional programs with wellfounded data, as proposed by Lee, Jones
and BenAmram (2001), is divided into 2 stages.
In the first stage, abstract interpretation is used to deduce parameter
sizechanges observed at potential function calls. (Of interest are
size decreases and nonincreases.) This information is summarized in a set
of "sizechange graphs." In the second stage, it is decided _precisely_
whether every infinite call sequence would give rise to infinite
descent
in the size of some parameter values, _according to the graphs_. If
this
is the case, the graphs are said to satisfy "sizechange termination"
(SCT). It follows that no infinite call sequence is possible, therefore
the subject program is terminating.
Since this work, SCT has been incorporated in the Agda Theorem Prover
(Wahlstedt 2000), adapted for termrewriting systems (Thiemann and
Giesl
2001), used in a runningtime analysis (Frederiksen and Jones 2003),
and applied to higherorder programs (Jones and Bohr 2004). Part of the
attractiveness of the SCT approach is its simplicity. Wahlstedt,
Thiemann
and Giesl also believe it to be an efficient way to "simulate the main
ingredients of RPOS, i.e., the concept of lexicographic and multiset
comparison."
However, the SCT condition is complete for PSPACE. Moreover, "permuted
arguments" trigger exponential behaviour in its decision procedure. In
this talk, we present a worstcase quadratictime approximation that
captures common parameterdescent behaviours. We have empirical
evidence
that the approximation is efficient and sufficiently precise in
practice.
Handling Liveness Properties in (Omega)Regular Model Checking
Axel Legay
Joined work with Pierre Wolper and Ahmed Bouajjani
Since the topic emerged several years ago, work on regular model
checking has mostly been devoted to the verification of state
reachability and safety properties. Though it was known that liveness
properties could also be checked within this framework, little has
been done about working out the corresponding details, and
experimentally evaluating the approach. This work addresses these
issues in the context of regular model checking based on the encoding
of states by finite or infinite words. It works out the exact
constructions to be used in both cases, and solves the problem
resulting from the fact that infinite computations of unbounded
configurations might never contain the same configuration twice, thus
making cycle detection problematic. Several experiments showing the
applicability of the approach were successfully conducted.
Liveness Properties for Program Optimization
Berhard Steffen
The talk will discuss what (liveness) properties make sense as a basis
for optimizing program transformations. In this course it will
distinguish three kinds of liveness properties
 bounded liveness
 conditional liveness
 unconditional liveness
"Synthesis of Timed Admission Controllers"
Wang Yi
P.S. Thiagarajan, Shaofa Yang and Wang Yi
In many realtime computing environments, there are some tasks
that are timecritical and others that are not. To ensure that
every critical task is completed before its deadline, it may be
necessary to deny entry  into the ready queue  for some
noncritical tasks. We address an abstract version of this problem
in the framework of controller synthesis. Our goal is to come up
with an \emph{admission controller} which admits or rejects a task
request, so that no admitted task misses its deadline and the admitted
patterns of task releases satisfy an LTL specification. We show that
it is decidable to determine if such an admission controller exists.
Further, if the answer is positive, it is possible to effectively
construct a controller in the form of a timed automata that has
a finite number of control locations and clock variables.
