The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Doctoral Symposium on Systems Software Verification (DS SSV'09)
Ralf Huuck, Gerwin Klein, Bastian Schlich (eds.)
AIB 2009-14
This report contains the proceedings of the Doctoral Symposium on
Systems Software Verification (DS SSV'09), which was held during the
4th International Workshop on Systems Software Verification (SSV'09)
in Aachen, Germany, June 22-24, 2009.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Time-optimal Winning Strategies for Poset Games
Martin Zimmermann
AIB 2009-13
We introduce a novel winning condition for infinite two-player games
on graphs which extends the request-response condition and better
matches concrete applications in scheduling or project planning. In
a poset game, a request has to be responded by multiple events in an
ordering over time that is compatible with a given partial ordering
of the events. Poset games are zero-sum, but there are plays that
are more desirable than others, i.e., those in which the requests
are served quickly. We show that optimal strategies (with respect to
long term average accumulated waiting times) exist. These strategies
are implementable with finite memory and are effectively computable.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Automatic Verification of the Correctness of the Upper Bound of a
Maximum Independent Set Algorithm
Felix Reidl, Fernando Sánchez Villaamil
AIB 2009-10
Kneis, Langer and Rossmanith presented a new exact algorithm for the
Maximum Independent Set problem. As part of the proof of the upper
runtime bound millions of special cases were automatically generated.
In this technical report we present a verification method that checks
the correctness of this case distinction. We focus on the theoretical
aspects of this verification and give a general overview of its
implementation.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Implementation of an Automated Proof for an Algorithm Solving the
Maximum Independent Set Problem
Michael Nett
AIB 2009-09
Kneis, Langer, and Rossmanith proposed an algorithm that solves the
maximum independent set problem for graphs with $n$ vertices in
$O^*(1.2132^n)$. This bound is obtained by precisely analyzing
all cases that the algorithm may encounter during execution. Since
the number of cases exceeds several millions, a computer aided proof
is used to generate and evaluate all cases. In this paper, we present
a program that fulfills this task and give a detailed description of
the principles underlying our method. Moreover, we prove that the set
of generated cases includes all relevant cases.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Entwurf eingebetteter Software mit abstrakten Zustandsmaschinen und
Business Object Notation
Daniel Klünder
AIB 2009-04
The ever increasing presence of information technology along with the
pervasion of hardware and software into everyday life boosts the need
for engineering methods and tools for the development of high quality
embedded systems. This trend is further amplified by the rising
complexity of such systems and their usage for safety critical tasks.
However, classical software engineering methods lack support for the
peculiarities of embedded systems. This thesis therefore extends these
methods with support for verification and requirements that arise
through interaction with the physical world.
Abstract state machines (ASMs) are used for functional modeling and
extended with an abstract notion for feedback control algorithms by
utilizing non-deterministic choose. For their verification this thesis
presents a novel approach to model checking ASMs that directly supports
them by utilizing their notion of run. The simulator CoreASM is adapted
to branch into all possible successor states and integrated into the
model checker [mc]square. On the one hand, this enables the approach to
present counterexamples and witnesses directly as sequences of ASM
states, to be easily extendable, and at the same time supports the
whole CoreASM syntax. On the other hand, it suffers from the
simulator's design that was built with the goals of comprehensiveness
and extendibility in mind and hence is not optimized for performance in
a model checker.
The Business Object Notation (BON) is used for structural modeling and
extended with the representation of concurrent classes. Requirements
that arise through the execution of the embedded system on a physical
platform are represented in preconditions while those that arise
through reactions to the physical environment are modeled in
postconditions. The former is only useful for short methods.
While ASMs can easily be transformed into an implementation, timed and
concurrent BON models need an extra runtime environment for a
semi-automatic translation. Therefore, simple concurrent
object-oriented programming (SCOOP) is implemented on a real-time
operating system and extended with the runtime checking of time
assertions in postconditions. Because of the unpredictability of
runtimes it is only practical for soft real-time systems and improves
the system's reusability at the expense of its resource usage.
For evaluating the approach an adaptive cruise control which includes
two closed loop controllers, interaction with the environment via
sensors and actuators, time requirements, and safety critical functions
is successfully implemented.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Time-Bounded Reachability in Continuous-Time Markov Decision Processes
Martin Neuhäußer, Lijun Zhang
AIB 2009-12
This paper solves the problem of computing the maximum and minimum
probability to reach a set of goal states within a given time bound
for locally uniform continuous-time Markov decision processes (CTMDPs).
As this model allows for nondeterministic choices between exponentially
delayed transitions, we define total time positional (TTP) schedulers
which rely on the CTMDP's current state and the total elapsed time
when taking a decision. In this paper, TTP schedulers are proved to
be sufficient to maximize timed reachability even w.r.t. fully
time- and history-dependent schedulers; further, they allow us
to derive a fixed point characterization of the optimal
timed-reachability probability.
The main contribution of this paper is a discretization technique
which, for an a priori given error bound epsilon, induces a
discrete-time MDP that approximates the optimal timed reachability
probability in the underlying CTMDP up to epsilon.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
The Longest Path Problem is Polynomial on Interval Graphs
Kyriaki Ioannidou, George B. Mertzios, Stavros D. Nikolopoulos
AIB 2009-11
The longest path problem is the problem of finding a path of
maximum length in a graph. Polynomial solutions for this problem are
known only for small classes of graphs, while it is NP-hard on general
graphs, as it is a generalization of the Hamiltonian path problem.
Motivated by the work of Uehara and Uno in~\cite{Ueh04}, where they left
the longest path problem open for the class of interval graphs, in this
paper we show that the problem can be solved in polynomial time on
interval graphs. The proposed algorithm runs in $O(n^4)$ time, where $n$
is the number of vertices of the input graph, and bases on a dynamic
programming approach.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
The Recognition of Tolerance and Bounded Tolerance Graphs is NP-complete
George B. Mertzios, Ignasi Sau, Shmuel Zaks
AIB 2009-06
Tolerance graphs model interval relations in such a way that
intervals can tolerate a certain degree of overlap without being in
conflict. This class of graphs has been extensively studied, due to both
its interesting structure and its numerous applications (in
bioinformatics, constrained-based temporal reasoning, resource
allocation, and scheduling problems, among others). Several efficient
algorithms for optimization problems that are NP-hard in general graphs
have been designed for tolerance graphs. In spite of this, the
recognition of tolerance graphs -namely, the problem of deciding whether
a given graph is a tolerance graph- as well as the recognition of their
main subclass of bounded tolerance graphs, are probably the most
fundamental open problems in this context (cf.~the book on tolerance
graphs~\cite{GolTol04}) since their introduction almost three decades
ago~\cite{GoMo82}. In this article we resolve this problem, by proving
that both recognition problems are NP-complete, even in the case where
the input graph is a trapezoid graph. For our reduction we extend the
notion of an acyclic orientation of permutation and trapezoid graphs.
Our main tool is a new algorithm (which uses an approach similar
to~\cite{Cheah96}) that transforms a given trapezoid graph into a
permutation graph, while preserving this new acyclic orientation property.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Satellites and Mirrors for Solving Independent Set on Sparse Graphs
Joachim Kneis, Alexander Langer
AIB 2009-08
We study the well-known Maximum Independent Set (MIS) problem and
introduce the notion of satellites of a node. Branching on nodes with
satellites is extremely simple. Nevertheless, satellites can be used to
overcome a couple of hard cases in previous algorithms. Together with
the notion of mirrors, introduced by Fomin, Grandoni, and Kratsch,
they can be used to solve MIS in time bounded by O^*(1.1928^{m-n}),
which is O^*(1.0922^n) for cubic graphs. This improves over previous
results for sparse graphs.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Derandomizing Non-uniform Color-Coding I
Joachim Kneis, Alexander Langer, Peter Rossmanith
AIB 2009-07
Color-coding, as introduced by Alon, Yuster, and Zwick, is a well-known
tool for algorithm design and can often be efficiently derandomized using
universal hash functions. In the special case of only two colors, one
can use (n,k)-universal sets for the derandomization. In this paper,
we introduce (n,k,l)-universal sets that are typically smaller and can
be constructed faster. Nevertheless, for some problems they are still
sufficient for derandomization and faster deterministic algorithms can
be obtained. This particularly works well when the color-coding does
not use a uniform probability distribution. To exemplify the concept, we
present an algorithm for the Unique Coverage problem introduced
by Demaine, Feige, Hajiaghayi, and Salavatipour. The example also shows
how to extend the concept to multiple colors.