May 2009 - tr-announce - lists.rwth-aachen.de

2009-13: Time-optimal Winning Strategies for Poset Games
by Carsten Fuhs 27 May '09

27 May '09

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.

1 0

2009-10: Automatic Verification of the Correctness of the Upper Bound of a Maximum Independent Set Algorithm
by Carsten Fuhs 18 May '09

18 May '09

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.

1 0

2009-09: Implementation of an Automated Proof for an Algorithm Solving the Maximum Independent Set Problem
by Carsten Fuhs 18 May '09

18 May '09

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.

1 0

2009-04: Entwurf eingebetteter Software mit abstrakten Zustandsmaschinen und Business Object Notation
by Carsten Fuhs 13 May '09

13 May '09

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.

1 0

2009-12: Time-Bounded Reachability in Continuous-Time Markov Decision Processes
by Carsten Fuhs 11 May '09

11 May '09

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.

1 0