The following technical report is available from
http://aib.informatik.rwth-aachen.de/:
Christof Löding and Philipp Rohde
Solving the Sabotage Game is PSPACE-hard
2003-05
Abstract:
We consider the sabotage game presented by van Benthem in an essay on the
occasion of Jörg Siekmann's 60th birthday. In this game one player moves
along the edges of a finite, directed or undirected multi-graph and the other
player takes out a link after each step. There are several algorithmic tasks
over graphs which can be considered as winning conditions for this game, for
example reachability, Hamilton path or complete search. As the game definitely
ends after at most the number of edges (counted with multiplicity) steps, it
is easy to see that solving the sabotage game for the mentioned tasks takes at
most PSPACE in the size of the graph. We will show that on the other hand
solving this game in general is PSPACE-hard for all conditions. We extend this
result to some variants of the game (removing more than one edge per round and
removing vertices instead of edges). Finally we introduce a modal logic over
changing models to express tasks corresponding to the sabotage games. We will
show that model checking this logic is PSPACE-complete.
Regards,
Volker
--
http://www-i2.informatik.rwth-aachen.de/stolz/
The following technical report is available from
http://aib.informatik.rwth-aachen.de/:
Jürgen Giesl and Deepak Kapur
Deciding Inductive Validity of Equations
2003-03
Abstract:
Kapur and Subramaniam [CADE-00] defined syntactical
classes of equations where inductive validity can be
decided automatically. However, these classes are quite
restrictive, since defined function symbols with recursive
definitions may only appear on one side of the equations.
In this paper, we expand the decidable class of equations
significantly by allowing both sides of equations to be
expressed using defined function symbols. The definitions
of these function symbols must satisfy certain
restrictions which can be checked mechanically.
These results are crucial to increase the
applicability of decision procedures for induction.
Regards,
Volker
--
http://www-i2.informatik.rwth-aachen.de/stolz/ *** PGP *** S/MIME
rage against the finite state machine
The following technical report is available from
http://aib.informatik.rwth-aachen.de/:
Jürgen Giesl and Rene Thiemann
Size-Change Termination for Term Rewriting
2003-02
Abstract:
In [Lee, Jones & Ben-Amram, 2001], a new
size-change principle was proposed to verify
termination of functional programs automatically.
We extend this principle in order to prove termination
and innermost termination of arbitrary term
rewrite systems (TRSs). Moreover, we compare this approach
with existing techniques for termination analysis of TRSs
(such as recursive path orderings or dependency pairs).
It turns out that the size-change principle on its own
fails for many examples that can be handled by
standard techniques for rewriting, but there are also TRSs
where it succeeds whereas existing rewriting techniques fail.
In order to benefit from their respective advantages,
we show how to combine the size-change principle
with classical orderings and with dependency pairs.
In this way, we obtain a new approach for
automated termination proofs of TRSs which is
more powerful than previous approaches.
Regards,
Volker
--
http://www-i2.informatik.rwth-aachen.de/stolz/
The following technical report is available from
http://aib.informatik.rwth-aachen.de/:
Jürgen Giesl and Hans Zantema
Liveness in Rewriting
2002-11
Abstract:
In this paper, we show how the problem of verifying
liveness properties is related to termination of term
rewrite systems (TRSs). We formalize liveness in the
framework of rewriting and present a sound and
complete transformation to transform liveness problems
into TRSs. Then the transformed TRS terminates if and
only if the original liveness property holds. This
shows that liveness and termination are essentially
equivalent. To apply our approach in practice, we
introduce a simpler sound transformation which only
satisfies the `only if'-part. By refining existing
techniques for proving termination of TRSs we show
how liveness properties can be verified automatically.
As an example, we prove a liveness property of a
waiting line protocol for a network of processes.
Regards,
Volker
--
http://www-i2.informatik.rwth-aachen.de/stolz/
The following technical report is available from
http://aib.informatik.rwth-aachen.de/:
Jörg Dahmen
Invariant Image Object Recognition using Gaussian Mixture Densities
2002-07
Abstract:
In this work, a statistical image object recognition system is presented, which is based on the
use of Gaussian mixture densities in the context of the Bayesian decision rule. Optionally,
to reduce the number of free model parameters, a linear discriminant analysis is applied.
This baseline system is then extended with respect to the incorporation of invariances.
To do so, we start by suitably multiplying the available reference images. This idea
is then applied to the observations to be classified, too, yielding the novel `Virtual Test Data'
method, which has some desirable advantages over classical classifier combination approaches.
Furthermore, global invariances are incorporated by using the so-called tangent distance.
In this work, tangent distance is embedded into a statistical framework, which for instance
leads to a modified, more reliable estimation of the mixture density parameters.
Furthermore, tangent distance is extended to compensate not only for global, but also for
local image transformations (`distorted tangent distanceŽ).
A large part of the experiments was performed on the well known US Postal Service standard
corpus for handwritten digit recognition. Furthermore, the proposed classifier was successfully
applied to the recognition of medical radiographs, red blood cells as well as to the
Columbia University Object Image Library (COIL-20) and the Max-Planck Institute's Chair Image
Database. The obtained error rate of 2.2% on the US Postal Service corpus is the best error
rate published so far on this particular data set.
Regards,
Volker
The following technical report is available from
http://aib.informatik.rwth-aachen.de/:
Martin Leucker
Logics for Mazurkiewicz traces
2002-10
Abstract:
Linear temporal logic (LTL) has become a well established tool for
specifying the dynamic behavior of reactive systems with an
interleaving semantics and the automata-theoretic approach has proven
to be a very useful mechanism for performing automatic verification in
this setting. Especially alternating automata turned out to be a
powerful tool in constructing efficient yet simple to understand
decision procedures and directly yield on-the-fly model checking
procedures.
While this technique extends elegantly to richer domains where the
underlying computations are modeled as (Mazurkiewicz) traces, it does
so only for event- and location-based temporal logics. In this thesis,
we exhibit a decision procedure for LTL over Mazurkiewicz traces which
generalizes the classical automata-theoretic approach to a linear
temporal logic interpreted no longer over sequences but restricted
labeled partial orders. Specifically, we construct a (linear)
alternating Buechi automaton accepting the set of linearizations of
those traces satisfying the formula at hand. The salient point of our
technique is to apply a notion of independence-rewriting to formulas
of the logic. Furthermore, we show that the class of linear and
trace-consistent alternating Buechi automata corresponds exactly to
LTL formulas over Mazurkiewicz traces, lifting a similar result from
Loeding and Thomas formulated in the framework of LTL over words.
Additionally, a linear temporal logic with a different flavor is
introduced as Foata linear temporal logic (FLTL). It is designed for
specifying properties of synchronized systems that comprise clocked
hardware circuits or Petri nets supplied with a maximal step
semantics.
Distributed synchronous transition systems (DSTSs) are
introduced as formal models of these systems and are equipped with a
Foata configuration graph-based semantics, which provides a
link between these systems and the framework of Mazurkiewicz traces.
To simplify the task of defining DSTSs, we introduce a simple
calculus in the spirit of CCS.
We give optimal decision procedures for satisfiability of FLTL
formulas as well as for model checking, both based on alternating
Buechi automata. The model checking procedure further employs an
optimization which is similar to a technique known as partial
order reduction.
Regards,
Volker
The following technical report is available from
http://aib.informatik.rwth-aachen.de/:
Markus Mohnen
Interfaces with Default Implementations in Java
2002-09
Abstract:
With the interface construct, Java features a concept with high
potential for producing reusable code: Java's interfaces allow
the definition of class properties independently of class
inheritance. We propose an extension of Java for providing
default implementations in interfaces. Default implementations
are useful since they reduce the effort required to implement
an interface. They are especially interesting if there is a
canonical way to implement methods of the interface in terms of
some other methods. In these cases, an implementation can be
obtained by implementing the base methods and use the default
implementations of the other methods. We discuss the rationale
for our design and show that the extension can be implemented
both efficiently and conservatively, i.e. without modification
of the Java virtual machine.
Regards,
Volker
--
The following technical report is available from
http://aib.informatik.rwth-aachen.de/:
Markus Mohnen
An Open Framework for Data-Flow Analysis in Java
2002-08
Abstract:
We describe work in progress on a framework for data-flow based
program analysis. By using this framework, researchers and
developers can easily implement analyses, test their correctness,
and evaluate their performance. In addition, the framework allows
the definition of intraprocedural analyses for Java Virtual
Machine (JVM) code on a high level of abstraction. The framework
is provided as a set of APIs for Java. Through the extensive use
of Java interface concept, we established an open framework: For
instance, specific implementations of abstract domains can easily
be used in our framework.
Regards,
Volker
--
The following technical report is available from
http://aib.informatik.rwth-aachen.de/:
Henry N. Adorna
3-Party Message Complexity is Better than 2-Party Ones for Proving Lower
Bounds on the Size of Minimal Nondeterministic Finite Automata
2002-06
Abstract:
Despite the facts that automata theory is one of the oldest and most
extensively investigated areas of theoretical computer science, and finite
automaton is the simplest model of computation, there are still principal
open problems about finite automata. One of them is to estimate, for
a regular language L, the size of the minimal nondeterministic finite
automaton accepting L. Currently, we do not have any method that would
at least assure an approximation of this value. The best known technique
for proving lower bound on the size of the minimal nondeterministic
finite automata is based on communication and this technique covers all
previously used approaches. Unfortunately, there exist regular languages
with an exponential gap between the communication complexity lower
bound and the size of a minimal nondeterministic finite automaton. The
contribution of this paper is to improve the communication complexity
lower bound technique in order to get essentially better lower bounds
for some regular languages.
Regards,
Volker Stolz
--
Wonderful \hbox (0.80312pt too nice) in paragraph at lines 16--18
Volker Stolz * stolz(a)i2.informatik.rwth-aachen.de
Please use PGP or S/MIME for correspondence!
The following technical report is available from
http://aib.informatik.rwth-aachen.de/:
Horst Lichter, Thomas von der Maßen, Thomas Weiler
Modelling Requirements and Architectures for Software Product Lines
2002-05
Abstract:
The development of software product lines has become a new and promising
field in software development in the last few years. Market asks for
faster development of new software products which also must be cheap and
of high quality. Here software product line engineering offers software
companies the possibility to adress this market needs by also reducing
the development costs.
Software product line engineering is based on the domain
engineering which provides a basis of core assets (also called
platform), which in turn can be reused by thereon based
applications in the application engineering. Thereby it is
essential to model the variability which occurs among different
applications derived from the platform.
Within requirements engineering the specification of requirements only
in natural language isn't adequate to obtain a most possible complete
and consistent description of requirements. Because existing notations
aren't adequat for modeling requirements for software product lines a
new approach is required.
Also architecture modeling for software product lines requires new
concepts for modeling the common and variable parts of a software
product line. Therefore software architectures for software product
lines can be described by means of feature components which
represent a specific characteristic of the system to be modeled.
This report adresses these problems and offers new concepts for their
solution.
--
Wonderful \hbox (0.80312pt too nice) in paragraph at lines 16--18
Volker Stolz * stolz(a)i2.informatik.rwth-aachen.de
Please use PGP or S/MIME for correspondence!