The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Quantitative Testing
Henrik Bohnenkamp, Marielle Stoelinga
AIB 2008-01
We investigate the problem of specification based testing with dense
sets of inputs and outputs, in particular with imprecision as they
might occur due to imprecise measurements, numerical instability
or noisy channels. Using quantitative transition systems to describe
implementations and specifications, we introduce implementation relations
that capture a notion of correctness "up to epsilon", i.e. that allow
deviation of the implementations behavior from that of the specification
as long as it does not deviate more than epsilon. The deviations are
described as Hausdorff distances between certain sets of traces. The
implementation relations are conservative extensions of the well-known
ioco relation. We develop a testing algorithm that we show to be sound
and exhaustive with respect to the implementation relations introduced.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Uncoordinated Two-Sided Markets
Heiner Ackermann, Paul W. Goldberg, Vahab S. Mirrokni, Heiko Röglin, and Berthold Vöcking
AIB 2007-22
Various economic interactions can be modeled as two-sided markets.
A central solution concept to these markets are stable matchings,
introduced by Gale and Shapley. It is well known that stable matchings
can be computed in polynomial time, but many real-life markets lack a
central authority to match agents. In those markets, matchings are formed
by actions of self-interested agents. Knuth introduced uncoordinated
two-sided markets and showed that the uncoordinated better response
dynamics may cycle. However, Roth and Vande Vate showed that the random
better response dynamics converges to a stable matching with probability
one, but did not address the question of convergence time.
In this paper, we give an exponential lower bound for the convergence
time of the random better response dynamics in two-sided markets. We also
extend these results to the best response dynamics, i.e., we present
a cycle of best responses, and prove that the random best response
dynamics converges to a stable matching with probability one, but its
convergence time is exponential. Additionally, we identify the special
class of correlated two-sided markets with real-life applications for
which we prove that the random best response dynamics converges in
expected polynomial time.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Three-Valued Abstraction for Probabilistic Systems
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, and Verena Wolf
AIB 2007-20
This paper proposes a novel abstraction technique for fully probabilistic
systems. The models of our study are classical discrete-time and
continuous time Markov chains (DTMCs and CTMCs, for short). A DTMC is
a Kripke structure in which each transition is equipped with a discrete
probability; in a CTMC, in addition, state residence times are governed
by negative exponential distributions. Our abstraction technique fits
within the realm of three-valued abstraction methods that have been
used successfully for traditional model checking. The key ingredients
of our technique are a partitioning of the state space combined with an
abstraction of transition probabilities by intervals. The uncertainty of
intervals is resolved by history-dependent schedulers that may choose
extreme values only. It is shown that this provides a conservative
abstraction for both negative and affirmative verification results for a
three-valued semantics of PCTL (Probabilistic Computation Tree Logic). In
the continuous-time setting, the key idea is to apply abstraction on
uniform CTMCs which are readily obtained from general CTMCs. In a similar
way as for the discrete case, this is shown to yield a conservative
abstraction for a three-valued semantics of CSL (Continuous Stochastic
Logic). The verification of abstract DTMCs is inspired by the standard
MDP (Markov Decision Process) model-checking problem. Abstract CTMCs
can be verified by computing time-bounded reachability probabilities in
continuous-time MDPs. Some experiments on an infinite-state stochastic
Petri net indicate the feasibility of our abstraction technique.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
The DP Framework for Proving Termination of Term Rewriting
René Thiemann
AIB 2007-17
Termination is the fundamental property of a program that for each input,
the evaluation will eventually stop and return some output. Although
the question whether a given program terminates is undecidable,
many techniques have been developed which can be used to answer the
question of termination for many programs automatically. Especially,
termination of term rewriting is an interesting and widely studied area:
Since the basic evaluation mechanism of many programming languages is term
rewriting, one can successfully apply the termination techniques for term
rewriting to analyze termination of programs automatically. Nevertheless,
there still remain many programs that cannot be handled by any current
technique that is amenable to automation.
In this thesis, we extend existing techniques and develop new methods
for mechanized termination analysis of term rewrite systems. Currently,
one of the most powerful techniques is the dependency pair approach. Up
to now, it was regarded as one of several possible methods to prove
termination. We show that dependency pairs can instead be used as
a general concept to integrate arbitrary techniques for termination
analysis. In this way, the benefits of different techniques can be
combined and their modularity and power are increased significantly. We
refer to this new concept as the "dependency pair framework" to
distinguish it from the old "dependency pair approach".
Moreover, this framework facilitates the development of new methods
for termination analysis. To demonstrate this, we design several novel
techniques within the dependency pair framework. They can successfully
be applied to prove termination of previously challenging programs. For
example, our work describes new ways how to handle programs using
accumulators, programs written in higher-order languages, and programs
which only terminate w.r.t. a given evaluation strategy. We additionally
show how to disprove termination, even under strategies.
All presented techniques are formulated in a uniform setting and
are implemented in our fully automated termination prover AProVE. The
significance of our results is demonstrated at the annual international
Termination Competition, where the leading automated tools try to
analyze termination of programs from different areas of computer science:
Without the contributions of this thesis, AProVE would not have reached
the highest scores both for proving and disproving termination in the
years 2004-2007.
Bisimulation and Logical Preservation for Continuous-Time Markov Decision
Processes
Martin Neuhäußer, Joost-Pieter Katoen
AIB 2007-10
This paper introduces strong bisimulation for continuous-time Markov
decision processes (CTMDPs), a stochastic model which allows for a
nondeterministic choice between exponential distributions, and shows that
bisimulation preserves the validity of CSL. To that end, we interpret the
semantics of CSL - a stochastic variant of CTL for continuous-time Markov
chains - on CTMDPs and show its measure-theoretic soundness. The main
challenge faced in this paper is the proof of logical preservation that
is substantially based on measure theory.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Temporal assertions for sequential and current programs
Volker Stolz
AIB 2007-15
In this thesis, we present an extension to the well-known concept of
assertions: temporal assertions allow the specification and validation of
modal safety properties of an application at runtime. We see this as a
necessary step in enforcing the growing number of implicit requirements
of software specifications, which are often only informally defined in
the documentation of application program interfaces (API) and are beyond
the reach of type checkers, compilers, or model checkers.
Also, we show how our techniques can be applied to existing programs
without modifying the source code. Although, like assertions, our
approach cannot prove the absence of errors, it gives the programmer
a more powerful means of automatically checking assumptions about his
program at runtime.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Adaptive Channel Assignment to Support QoS and Load Balancing for Wireless
Mesh Networks
Sadeq Ali Makram, Mesut Güneç, Martin Wenig, Alexander Zimmermann
AIB 2007-16
One of the most promising wireless technologies are Wireless Mesh
Networks (WMN). The aggregate capacity of wireless mesh networks
can be improved significantly be equipping each node with several
Wireless Network Interfaces (WNICs) and by using multiple channels in
order to minimize the interference and to provide high performance in
such networks. To achieve these benefits it requires a good channel
assignment planning. The channels have to be assigned in such a way,
that interference is decreased and performance is increased at the same
time. Since the number of available channels is limited, it is desired
to allocate and reallocate channels dynamically on-demand.
In this paper, a dynamic channel assignment, is proposed to the
aforementioned problem which is adaptive to the load in the wireless
mesh network. The algorithm add or select a channel for those heavy
loaded nodes, based on the local informations of the neighbor nodes.
The selected or the added channel that minimizes the interference and
insure the network connectivity. The simulation results show that our
algorithm improve the network capacity by approximately 50% in comparison
to a static channel assignment.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
6. Fachgespräch Sensornetzwerke
Klaus Wehrle (editor)
AIB 2007-11
This report contains the proceedings of the 6. Fachgespräch
Sensornetzwerke of the der GI/ITG Fachgruppe "Kommunikation und Verteilte
Systeme", which was held on July 16-17, 2007 in Aachen, Germany.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
OpenAD/F: A Modular, Open-Source Tool for Automatic Differentiation of
Fortran Codes
Jean Utke, Uwe Naumann, Mike Fagan, Nathan Tallent, Michelle Strout,
Patrick Heimbach, Chris Hill, and Carl Wunsch
AIB 2007-14
The OpenAD/F tool allows the evaluation of derivatives of functions
defined by a Fortran program. The derivative evaluation is performed by
a Fortran code resulting from the analysis and transformation of the
original program that defines the function of interest. OpenAD/F has
been designed with a particular emphasis on modularity, flexibility,
and the use of open source components. While the code transformation
follows the basic principles of automatic differentiation, the tool
implements new algorithmic approaches at various levels, for example,
for basic block preaccumulation and call graph reversal. Unlike most
other automatic differentiation tools, OpenAD/F uses components provided
by the OpenAD framework, which supports a comparatively easy extension
of the code transformations in a language-independent fashion. It uses
code analysis results implemented in the OpenAnalysis component. The
interface to the language-independent transformation engine is an
XML-based format, specified through an XML schema. The implemented
transformation algorithms allow efficient derivative computations using
locally optimized cross-country sequences of vertex, edge, and face
elimination steps. Specifically, for the generation of adjoint codes,
OpenAD/F supports various code reversal schemes with hierarchical
checkpointing at the subroutine level. As an example from geophysical
fluid dynamics a nonlinear time-dependent scalable, yet simple, barotropic
ocean model is considered. OpenAD/F's reverse mode is applied to compute
sensitivities of some of the model's transport properties with respect
to gridded fields such as bottom topography as independent (control)
variables.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Second-Order Adjoints by Source Code Manipulation of Numerical Programs
Uwe Naumann, Michael Maier, Jan Riehme, and Bruce Christianson
AIB 2007-13
The analysis and modification of numerical programs in the context
of generating and optimizing adjoint code automatically probably
ranges among the technically and theoretically most challenging
source transformation algorithms known today. A complete compiler
for the target language (Fortran in our case) is needed to cover the
technical side. This amounts to a mathematically motivated semantic
transformation of the source code that involves the reversal of the
flow of data through the program. Both the arithmetic complexity and
the memory requirement can be substantial for large-scale numerical
simulations. Finding the optimal data-flow reveral schedule turns out to
be an NP-complete problem. The same complexity result applies to other
domain-specific peephole optimizations. In this paper we present a first
research prototype of the NAGWare Fortran compiler with the ability to
generate adjoint code automatically. Moreover, we discuss an approach
to generating second-order adjoint code for use in Newtontype algorithms
for unconstrained nonlinear optimization. While the focus of this paper
is mostly on the compiler issues some information on the mathematical
background will be found helpful for motivational purposes.