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

2003-05: Solving the Sabotage Game is PSPACE-hard
by Volker Stolz 19 Mar '03

19 Mar '03

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/

1 0

2003-03: Deciding Inductive Validity of Equations
by Volker Stolz 14 Feb '03

14 Feb '03

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

1 0

2003-02: Size-Change Termination for Term Rewriting
by Volker Stolz 24 Jan '03

24 Jan '03

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/

1 0

2002-11: Liveness in Rewriting
by Volker Stolz 31 Oct '02

31 Oct '02

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/

1 0

2002-07 Invariant Image Object Recognition using Gaussian Mixture Densities
by Volker Stolz 09 Aug '02

09 Aug '02

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

1 0

2002-10 Logics for Mazurkiewicz traces
by Volker Stolz 16 Jul '02

16 Jul '02

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

1 0

[tr-announce] AIB: Interfaces with Default Implementations in Java
by Volker Stolz 01 May '02

01 May '02

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 --

1 0

[tr-announce] AIB: An Open Framework for Data-Flow Analysis in Java
by Volker Stolz 01 May '02

01 May '02

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 --

1 0

[tr-announce] AIB: 3-Party Message Complexity is Better than 2-Party Ones for Proving Lower Bounds on the Size of Minimal Nondeterministic Finite Automata
by Volker Stolz 14 Mar '02

14 Mar '02

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!

1 0

[tr-announce] AIB: Modelling Requirements and Architectures for Software Product Lines
by Volker Stolz 26 Feb '02

26 Feb '02

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!

1 0