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

2008-01: Quantitative Testing
by Peter Schneider-Kamp 25 Jan '08

25 Jan '08

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.

1 0

2007-22: Uncoordinated Two-Sided Markets
by Peter Schneider-Kamp 18 Dec '07

18 Dec '07

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.

1 0

2007-20: Three-Valued Abstraction for Probabilistic Systems
by Peter Schneider-Kamp 04 Dec '07

04 Dec '07

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.

1 0

2007-17: The DP Framework for Proving Termination of Term Rewriting
by Peter Schneider-Kamp 25 Oct '07

25 Oct '07

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.

1 0

2007-10: Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes
by Peter Schneider-Kamp 28 Aug '07

28 Aug '07

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.

1 0

2007-15: Temporal assertions for sequential and current programs
by Peter Schneider-Kamp 15 Aug '07

15 Aug '07

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.

1 0

2007-16: Adaptive Channel Assignment to Support QoS and Load Balancing for Wireless Mesh Networks
by Peter Schneider-Kamp 07 Aug '07

07 Aug '07

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.

1 0

2007-11: 6. Fachgespräch Sensornetzwerke
by Peter Schneider-Kamp 23 Jul '07

23 Jul '07

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.

1 0

2007-14: OpenAD/F: A Modular, Open-Source Tool for Automatic Differentiation of Fortran Codes
by Peter Schneider-Kamp 02 Jul '07

02 Jul '07

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.

1 0

2007-13: Second-Order Adjoints by Source Code Manipulation of Numerical Programs
by Peter Schneider-Kamp 02 Jul '07

02 Jul '07

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.

1 0