June 2008 - tr-announce - lists.rwth-aachen.de

2008-15: A New Algorithm for Finding Trees with Many Leaves
by Peter Schneider-Kamp 25 Jun '08

25 Jun '08

The following technical report is available from http://aib.informatik.rwth-aachen.de: A New Algorithm for Finding Trees with Many Leaves Joachim Kneis, Alexander Langer, Peter Rossmanith AIB 2008-15 We present an algorithm that finds trees with at least k leaves in undirected and directed graphs. These problems are known as Maximum Leaf Spanning Tree for undirected graphs, and, respectively, Directed Maximum Leaf Out-Tree and Directed Maximum Leaf Spanning Out-Tree in the case of directed graphs. The run time of our algorithm is O(poly(|V|) + 4^k k^2) on undirected graphs, and O(4^k |V| |E|) on directed graphs. Currently, the fastest algorithms for these problems have run times of O(poly(n) + 6.75^k poly(k)) and 2^{O(k log k)} poly(n), respectively.

1 0

2008-14: Model Checking Software for Microcontrollers
by Peter Schneider-Kamp 18 Jun '08

18 Jun '08

The following technical report is available from http://aib.informatik.rwth-aachen.de: Model Checking Software for Microcontrollers Bastian Schlich AIB 2008-14 Software of microcontrollers is getting more and more complex. It is mandatory to extensively analyze their software as errors can lead to severe failures or cause high costs. Model checking is a formal method used to verify whether a system satisfies certain properties. This thesis describes a new approach for model checking software for microcontrollers. In this approach, assembly code is used for model checking instead of an intermediate representation such as C code. The development of [MC]SQUARE, which is a microcontroller assembly code model checker implementing this approach, is detailed. [mc]square has a modular architecture to cope with the hardware dependency of this approach. The single steps of the model checking process are divided into separate packages. The creation of the states is conducted by a specific simulator, which is the only hardware-dependent package. Within the simulator, the different microcontrollers are modeled accurately. This work describes the modeling of the ATMEL ATmega16 microcontroller and details implemented abstraction techniques, which are used to tackle the state-explosion problem. These abstraction techniques include lazy interrupt evaluation, lazy stack evaluation, delayed nondeterminism, dead variable reduction, and path reduction. Delayed nondeterminism introduces symbolic states, which represent a set of states, into [MC]SQUARE while still explicit model checking techniques are used. Thus, we successfully combined explicit and symbolic model checking techniques. A formal model of the simulator, which we developed to prove the correctness of abstraction techniques, is described. In this work, the formal model is used to show the correctness of delayed nondeterminism. To show the applicability of the approach, two case studies are described. In these case studies, we used programs of different sizes. All these programs were created by students in lab courses, during diploma theses, or in exercises without the intention to use them for model checking.

1 0

2008-13: Improving Context-Sensitive Dependency Pairs
by Peter Schneider-Kamp 17 Jun '08

17 Jun '08

The following technical report is available from http://aib.informatik.rwth-aachen.de: Improving Context-Sensitive Dependency Pairs Beatriz Alarcón, Fabian Emmes, Carsten Fuhs, Jürgen Giesl, Raúl Gutierrez, Salvador Lucas, Peter Schneider-Kamp, René Thiemann AIB 2008-13 Context-sensitive dependency pairs (CS-DPs) are currently the most powerful method for automated termination analysis of context- sensitive rewriting. However, compared to DPs for ordinary rewriting, CS-DPs suffer from two main drawbacks: (a) CS-DPs can be collapsing. This complicates the handling of CS-DPs and makes them less powerful in practice. (b) There does not exist a "DP framework" for CS-DPs which would allow to apply them in a flexible and modular way. This paper solves drawback (a) by introducing a new definition of CS-DPs. With our definition, CS-DPs are always non-collapsing and thus, they can be handled like ordinary DPs. This allows us to solve drawback (b) as well, i.e., we extend the existing DP framework for ordinary DPs to context- sensitive rewriting. We implemented our results in the tool AProVE and successfully evaluated them on a large collection of examples.

1 0

2008-12: Abstraction for stochastic systems by Erlang's method of stages
by Peter Schneider-Kamp 07 Jun '08

07 Jun '08

The following technical report is available from http://aib.informatik.rwth-aachen.de: Abstraction for stochastic systems by Erlang's method of stages Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf AIB 2008-12 This paper proposes a novel abstraction technique based on Erlang's method of stages for continuous-time Markov chains (CTMCs). As abstract models Erlang-k interval processes are proposed where state residence times are governed by Poisson processes and transition probabilities are specified by intervals. We provide a three-valued semantics of CSL (Continuous Stochastic Logic) for Erlang-k interval processes, and show that both affirmative and negative verification results are preserved by our abstraction. The feasibility of our technique is demonstrated by a quantitative analysis of an enzyme-catalyzed substrate conversion, a well-known case study from biochemistry.

1 0

2008-11: Fast Convergence of Routing Games with Splittable Flows
by Peter Schneider-Kamp 07 Jun '08

07 Jun '08

The following technical report is available from http://aib.informatik.rwth-aachen.de: Fast Convergence of Routing Games with Splittable Flows George B. Mertzios AIB 2008-11 In this paper we investigate the splittable routing game in a series-parallel network with two selfish players. Every player wishes to route optimally, i.e. at minimum cost, an individual flow demand from the source to the destination, giving rise to a non-cooperative game. We allow a player to split his flow along any number of paths. One of the fundamental questions in this model is the convergence of the best response dynamics to a Nash equilibrium, as well as the time of convergence. We prove that this game converges indeed to a Nash equilibrium in a logarithmic number of steps. Our results hold for increasing and convex player-specific latency functions. Finally, we prove that our analysis on the convergence time is tight for affine latency functions.

1 0