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

2010-08: Automated Termination Analysis of Java Bytecode by Term Rewriting
by Carsten Fuhs 09 Apr '10

09 Apr '10

The following technical report is available from http://aib.informatik.rwth-aachen.de: Automated Termination Analysis of Java Bytecode by Term Rewriting Carsten Otto, Marc Brockschmidt, Christian von Essen, Jürgen Giesl AIB 2010-08 We present an automated approach to prove termination of Java Bytecode (JBC) programs by automatically transforming them to term rewrite systems (TRSs). In this way, the numerous techniques and tools developed for TRS termination can now be used for imperative object-oriented languages like Java, which can be compiled into JBC.

1 0

2010-07: A New Intersection Model for Multitolerance Graphs, Hierarchy, and Efficient Algorithms
by Carsten Fuhs 27 Mar '10

27 Mar '10

The following technical report is available from http://aib.informatik.rwth-aachen.de: A New Intersection Model for Multitolerance Graphs, Hierarchy, and Efficient Algorithms George B. Mertzios AIB 2010-07 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 attracted many research efforts, mainly due to its interesting structure and its numerous applications, while a number of variations of this model has appeared. In particular, one of the most natural generalizations of tolerance graphs, namely \emph{multitolerance} graphs, has been introduced in 1998 \cite{Parra98}, where two tolerances are allowed for each interval. These two tolerances - one from the left and one from the right side of the interval - define an infinite number of the so called \emph{tolerance-intervals}, which make the multitolerance model inconvenient to cope with. The main subclass of multitolerance graphs, namely bounded multitolerance graphs, coincide with the widely known class of trapezoid graphs that has been extensively studied. In this article we introduce the first non-trivial intersection model for general multitolerance graphs, given by objects in the three-dimensional space called \emph{trapezoepipeds}, which unifies in a simple and intuitive way the trapezoid representation for bounded multitolerance graphs and the recently introduced parallelepiped representation for tolerance graphs \cite{MSZ-Model-SIDMA-09}. Apart from being important on its own, this new intersection model proves to be a powerful tool for designing efficient algorithms. Given a multitolerance graph with $n$ vertices and $m$ edges, we present three new algorithms that compute a minimum coloring and a maximum clique in optimal $O(n\log n)$ time, and a maximum weight independent set in $O(m + n\log n)$ time - this algorithm also improves the best known running time of $O(n^{2})$ for the same problem on tolerance graphs \cite{MSZ-Model-SIDMA-09}. Moreover, we prove several structural results on the class of multitolerance graphs, complementing thus the hierarchy of perfect graphs given in \cite{GolTol04}. The resulting hierarchy of classes of perfect graphs is \emph{complete}, i.e. all inclusions are strict.

1 0

2010-03: MontiCore: Agile Entwicklung von domänenspezifischen Sprachen im Software-Engineering
by Carsten Fuhs 27 Mar '10

27 Mar '10

The following technical report is available from http://aib.informatik.rwth-aachen.de: MontiCore: Agile Entwicklung von domänenspezifischen Sprachen im Software-Engineering Holger Krahn AIB 2010-03 Domänenspezifische Sprachen (engl. domain specific language - DSL) sind Sprachen der Informatik, mit denen kompakte Problemlösungen aus eng umrissenen fachlichen oder technischen Anwendungsgebieten formuliert werden können. Durch die Nutzung einer fachspezifischen Notation gelingt die Integration von Experten einfacher als bei einer herkömmlichen Softwareentwicklung, weil die Modelle von ihnen besser verstanden werden. Die automatische Erzeugung von Produktivcode aus domänenspezifischen Modellen ist eine effektive Form der modellgetriebenen Entwicklung. Die derzeitige DSL-Entwicklung erschwert aufgrund der fehlenden zentralen Sprachreferenz, die die abstrakte und konkrete Syntax umfasst, und der unzureichenden Modularisierung eine agile und effiziente Vorgehensweise. Es mangelt an Methoden und Referenzarchitekturen, um komplexe modellbasierte Werkzeuge strukturiert entwerfen und in der Softwareentwicklung einsetzen zu können. In dieser Arbeit wird daher die DSL-Entwicklung mit dem MontiCore-Framework beschrieben, das die modulare Entwicklung von textuellen DSLs und darauf basierten Werkzeugen erlaubt. Die wichtigsten wissenschaftlichen Beiträge lassen sich wie folgt zusammenfassen: * Die Definition von textuellen domänenspezifischen Sprachen wird durch ein kompaktes grammatikbasiertes Format ermöglicht, das sowohl die abstrakte als auch die konkrete Syntax einer Sprache definiert und so als zentrale Dokumentation für die Entwickler und Nutzer einer DSL fungiert. Die entstehende abstrakte Syntax entspricht etablierten Metamodellierungs-Technologien und erweitert übliche grammatikbasierte Ansätze. * Die Wiederverwendung von Teilsprachen innerhalb der modellgetriebenen Entwicklung wird durch zwei Modularitätsmechanismen vereinfacht, da so existierende Artefakte auf eine strukturierte Art und Weise in neuen Sprachdefinitionen eingesetzt werden können. Grammatikvererbung erlaubt die Spezialisierung und Erweiterung von Sprachen. Einbettung ermöglicht die flexible Kombination mehrerer Sprachen, die sich auch in ihrer lexikalischen Struktur grundlegend unterscheiden können. * Das MontiCore-Grammatikformat ist modular erweiterbar, so dass zusätzliche Informationen als so genannte Konzepte spezifiziert werden können und darauf aufbauend weitere Infrastruktur aus der Sprachdefinition generiert werden kann. Die Erweiterungsfähigkeit wird durch Konzepte zur deklarativen Spezifikation von Links in der abstrakten Syntax und durch ein Attributgrammatiksystem demonstriert. * Die Entwicklung von Codegeneratoren und Analysewerkzeugen für DSLs wird durch die Bereitstellung einer Referenzarchitektur entscheidend vereinfacht, so dass bewährte Lösungen ohne zusätzlichen Entwicklungsaufwand genutzt werden können. Die Qualität der entstehenden Werkzeuge wird damit im Vergleich zu existierenden Ansätzen gehoben. * Es wird demonstriert, wie compilierbare Templates ein integriertes Refactoring der Templates und einer Laufzeitumgebung ermöglichen. Darauf aufbauend wird eine Methodik definiert, die aus exemplarischem Quellcode schrittweise einen Generator entwickelt, dessen Datenmodell automatisiert abgeleitet werden kann. Die beschriebenen Sprachen und Methoden sind innerhalb des Frameworks MontiCore implementiert. Ihre Anwendbarkeit wird durch die Entwicklung des MontiCore-Frameworks im Bootstrapping-Verfahren und durch zwei weitere Fallstudien demonstriert.

1 0

2010-02: Learning Visibly One-Counter Automata in Polynomial Time
by Carsten Fuhs 18 Jan '10

18 Jan '10

The following technical report is available from http://aib.informatik.rwth-aachen.de: Learning Visibly One-Counter Automata in Polynomial Time Daniel Neider, Christof Löding AIB 2010-02 Visibly one-counter automata are a restricted kind of one-counter automata: The input symbols are typed such that the type determines the instruction that is executed on the counter when the input symbol is read. We present an Angluin-like algorithm for actively learning visibly one-counter automata that runs in polynomial time in characteristic parameters of the target language and in the size of the information provided by the teacher.

1 0

2009-18: Parametrized Regular Infinite Games and Higher-Order Pushdown Strategies
by Carsten Fuhs 23 Sep '09

23 Sep '09

The following technical report is available from http://aib.informatik.rwth-aachen.de: Parametrized Regular Infinite Games and Higher-Order Pushdown Strategies Paul Hänsch, Michaela Slaats, Wolfgang Thomas AIB 2009-18 Given a set $P$ of natural numbers, we consider infinite games where the winning condition is a regular $\omega$-language parametrized by $P$. In this context, an $\omega$-word, representing a play, has letters consisting of three components: The first is a bit indicating membership of the current position in $P$, and the other two components are the letters contributed by the two players. Extending recent work of Rabinovich we study here predicates $P$ where the structure $(\mathbb{N}, +1, P)$ belongs to the pushdown hierarchy (or ``Caucal hierarchy''). For such a predicate $P$ where $(\mathbb{N}, +1, P)$ occurs in the $k$-th level of the hierarchy, we provide an effective determinacy result and show that winning strategies can be implemented by deterministic level-$k$ pushdown automata.

1 0

2009-16: Vertex Splitting and the Recognition of Trapezoid Graphs
by Carsten Fuhs 23 Sep '09

23 Sep '09

The following technical report is available from http://aib.informatik.rwth-aachen.de: Vertex Splitting and the Recognition of Trapezoid Graphs George B. Mertzios, Derek G. Corneil AIB 2009-16 Trapezoid graphs are the intersection family of trapezoids where every trapezoid has a pair of opposite sides lying on two parallel lines. These graphs have received considerable attention and lie strictly between permutation graphs (where the trapezoids are lines) and cocomparability graphs (the complement has a transitive orientation). The operation of ``vertex splitting'', introduced in~\cite{CC}, first augments a given graph $G$ and then transforms the augmented graph by replacing each of the original graph's vertices by a pair of new vertices. This ``splitted graph'' is a permutation graph with special properties if and only if $G$ is a trapezoid graph. Recently vertex splitting has been used to show that the recognition problems for both tolerance and bounded tolerance graphs is NP-complete~\cite{MSZ2}. Unfortunately, the vertex splitting trapezoid graph recognition algorithm presented in~\cite{CC} is not correct. In this paper, we present a new way of augmenting the given graph and using vertex splitting such that the resulting algorithm is simpler and faster than the one reported in~\cite{CC}.

1 0

2009-17: Learning Communicating and Nondeterministic Automata
by Carsten Fuhs 22 Sep '09

22 Sep '09

The following technical report is available from http://aib.informatik.rwth-aachen.de: Learning Communicating and Nondeterministic Automata Carsten Kern AIB 2009-17 The results of this dissertation are two-fold. On the one hand, inductive learning techniques are extended and two new inference algorithms for inferring nondeterministic, and universal, respectively, finite-state automata are presented. On the other hand, certain learning techniques are employed and enhanced to semi-automatically infer communicating automata (also called design models in the software development cycle). For both topics, theoretical results on the feasibility of the approaches, as well as an implementation are presented which, in both cases, support our theory. Concerning the first objective to derive a so-called active online learning algorithm for nondeterministic finite-state automata (NFA), we present, in analogy to Angluin's famous learning algorithm L* for deterministic finite-state automata (DFA), a version for inferring a certain subclass of NFA. The automata from this class are called residual finite-state automata (RFSA). It was shown by Denis et al. that there is an exponential gap between the size of minimal DFA and their corresponding minimal RFSA. Even if there are also cases where the canonical (i.e., minimal) RFSA is exponentially larger than a corresponding minimal NFA, we show that the new learning algorithm---called NL*---is a great improvement compared to L* as the inferred canonical RFSA has always at most the size of the corresponding minimal DFA but is usually even considerably smaller and more easy to learn. Unlike a learning procedure developed by Denis et al.---called DeLeTe2---our algorithm is capable of deriving canonical RFSA. Like L*, the new algorithm will be applicable in many fields including pattern recognition, computational linguistics and biology, speech recognition, and verification. From our point of view, NL* might especially play a major role in the area of formal verification where the size of the models that are processed is of enormous importance and nondeterminism not regarded an unpleasant property. The second objective of this thesis is to create a method for inferring distributed design models (CFMs) from a given set of requirements specified as scenarios (message sequence charts). The main idea is to extend the L* algorithm to cope with valid and invalid sets of system runs and, after some iterations, come up with an intermediate design model (a DFA) which exhibits features that make it distributable into communicating components (or processes) interacting via FIFO channels. Theoretical results on which classes of CFMs are learnable in which time-complexity bounds are presented. We also developed a tool implementation called Smyle, realizing important theoretical results evolving from this part of the thesis. Based on this learning formalism we also derive a software-engineering lifecycle model called the Smyle Modeling Approach in which we embedded our learning approach. Additionally, we launched a project for a new learning library called libalf which includes most of the learning algorithms (and their extensions) mentioned in this thesis. We hope that, due to its continuously increasing functionality, libalf will find broad acceptance among researchers, and that it will be the starting point for an extensive project of different research groups which will employ libalf, or augment the library with new algorithms.

1 0

2009-02: Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
by Carsten Fuhs 31 Aug '09

31 Aug '09

The following technical report is available from http://aib.informatik.rwth-aachen.de: Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre AIB 2009-02 We study the following problem: given a continuous-time Markov chain (CTMC) C, and a linear real-time property provided as a deterministic timed automaton (DTA) A, what is the probability of the set of paths of C that are accepted by A (C satisfies A)? It is shown that this set of paths is measurable and computing its probability can be reduced to computing the reachability probability in a piecewise deterministic Markov process (PDP). The reachability probability is characterized as the least solution of a system of integral equations and is shown to be approximated by solving a system of partial differential equations. For the special case of single-clock DTA, the system of integral equations can be transformed into a system of linear equations where the coefficients are solutions of ordinary differential equations.

1 0

2008-19: Empirical Studies for the Application of Agile Methods to Embedded Systems
by Carsten Fuhs 06 Jul '09

06 Jul '09

The following technical report is available from http://aib.informatik.rwth-aachen.de: Empirical Studies for the Application of Agile Methods to Embedded Systems Dirk Wilking AIB 2008-19 Agile Methods are a collection of software engineering techniques with specific differences to traditional software engineering processes. The main differences consist of rapid, cycle based development phases setting the focus of attention on feedback of the source code being developed. The results taken from user feedback, software reviews, or other forms of software evaluation are used as a basis for changes which comprise for example corrections of the user interface or the adaption of the software architecture. Based on single techniques taken from Agile Methods, their application to embedded systems software engineering is empirically evaluated in this thesis. The experiments and studies which have been conducted comprise the techniques of refactoring, short releases, and test driven development. The results hint to inconclusive effects. For example it could be shown that a constant effort for functional work is achieved by using the short releases technique, but its impact on the resulting software remains difficult to assess. For refactoring a reduced consumption of memory was found, but this effect was created by an overhead for applying the refactoring technique itself. The effect of agile techniques appears to be inferior to individual software development ability of participants in terms of factor strength. Consequently, the second part of the thesis aims at creating variables for the purpose of experiment control. Variables comprise C language knowledge and viscosity measuring a participant's level of reluctance to change a fragment of source code. An additional experiment consists of the replication of the N-version programming experiment by Knight and Leveson. The original experiment of independence between two program failures has been extended by an additional factor of hardware diversity. By using different hardware platforms, it has been expected to create mutual independent failures which is not approved by experimental observations.

1 0

2009-15: Compositional Abstraction for Stochastic Systems
by Carsten Fuhs 26 Jun '09

26 Jun '09

The following technical report is available from http://aib.informatik.rwth-aachen.de: Compositional Abstraction for Stochastic Systems Joost-Pieter Katoen, Daniel Klink, Martin Neuhäußer AIB 2009-15 We propose to exploit three-valued abstraction to stochastic systems in a compositional way. This combines the strengths of an aggressive state-based abstraction technique with compositional modeling. Applying this principle to interactive Markov chains yields abstract models that combine interval Markov chains and modal transition systems in a natural and orthogonal way. We prove the correctness of our technique for parallel and symmetric composition and show that it yields lower bounds for minimal and upper bounds for maximal timed reachability probabilities.

1 0