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

[tr-announce] AIB: Innermost Termination of Context-Sensitive Rewriting
by Volker Stolz 19 Feb '02

19 Feb '02

The following technical report is available from http://aib.informatik.rwth-aachen.de/: Jürgen Giesl, Aart Middeldorp Innermost Termination of Context-Sensitive Rewriting 2002-04 Abstract: Context-sensitive rewriting is a term rewriting strategy used to model evaluation strategies in functional programming and in programming languages like OBJ. For example, under certain conditions termination of an OBJ program is equivalent to innermost termination of the corresponding context-sensitive rewrite system [Lucas, 2001]. To prove termination of context-sensitive rewriting, several methods have been proposed in the literature which transform context-sensitive rewrite systems into ordinary rewrite systems such that termination of the transformed ordinary system implies termination of the original context-sensitive system. None of these transformation methods is very satisfactory when it comes to proving innermost termination. We present a simple transformation which is both sound and complete for innermost termination. -- 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: Generalised Regular MSC Languages
by Volker Stolz 19 Feb '02

19 Feb '02

[The web pages finally moved to a new layout and automated generation of HTML code. Please report any problems to tr-admin(a)informatik.rwth-aachen.de!] The following technical report is available from http://aib.informatik.rwth-aachen.de/: Benedikt Bollig, Martin Leucker, Thomas Noll Generalised Regular MSC Languages 2002-03 Abstract: We establish the concept of regularity for languages consisting of Message Sequence Charts (MSCs). To this aim, we formalise their behaviour by string languages and give a natural definition of regularity in terms of an appropriate Nerode right congruence. Moreover, we present a class of accepting automata and establish several decidability and closure properties of MSC languages. We also provide a logical characterisation by a monadic second-order logic interpreted over MSCs. In contrast to existing work on regular MSC languages, our approach is neither restricted to a certain class of MSCs nor tailored to a fixed communication medium (such as a FIFO channel). It explicitly allows MSCs with message overtaking and is thus applicable to a broad range of channel types like mixtures of stacks and FIFOs. 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: Kolloquium Programmiersprachen und Grundlagen der Programmierung
by Volker Stolz 28 Jan '02

28 Jan '02

The following technical report is available from http://aib.informatik.rwth-aachen.de: Klaus Indermark and Thomas Noll (eds.) Kolloquium Programmiersprachen und Grundlagen der Programmierung 2001-11 Abstract: This report contains the proceedings of the Colloquium on "Programmiersprachen und Grundlagen der Programmierung", which was held between October 7 and 11, 2001, at Rurberg, Germany. -- Volker Stolz * stolz(a)i2.informatik.rwth-aachen.de

1 0

[tr-announce] AIB: Transformation Techniques for Context-Sensitive Rewrite Systems
by Volker Stolz 17 Jan '02

17 Jan '02

The following technical report is available from http://aib.informatik.rwth-aachen.de: Jürgen Giesl, Aart Middledorp Transformation Techniques for Context-Sensitive Rewrite Systems 2002-02 Abstract: Context-sensitive rewriting is a term rewriting strategy used to model non-strict (lazy) evaluation in functional programming. The goal of this paper is the study and development of techniques to analyse the termination behavior of context-sensitive rewrite systems. For that purpose, several methods have been proposed in the literature which transform context-sensitive rewrite systems into ordinary rewrite systems such that termination of the transformed ordinary system implies termination of the original context-sensitive system. In this way, the huge variety of existing techniques for termination analysis of ordinary rewriting can be used for context-sensitive rewriting, too. We analyse the existing transformation techniques for proving termination of context-sensitive rewriting and we suggest two new transformations. Our first method is simple, sound, and more powerful than the previously proposed transformations. However, it is not complete, i.e., there are terminating context-sensi\-tive rewrite systems that are transformed into non-terminating term rewrite systems. The second method that we present in this paper is both sound and complete. All these observations also hold for rewriting modulo associativity and commutativity. Our completeness result can be interpreted as stating that one no longer needs any special techniques for the termination analysis of context-sensitive rewriting. Regards, Volker Stolz -- Volker Stolz * stolz(a)i2.informatik.rwth-aachen.de

1 0

[tr-announce] AIB: Axiomatising Tree-interpretable Structures
by Martin Leucker 06 Dec '01

06 Dec '01

Hi, please note that the following technical report is available on http://aib.informatik.rwth-aachen.de: Achim Blumensath: Axiomatising Tree-interpretable Structures 2001-10 Abstract: We introduce the class of tree-interpretable structures which generalises the notion of a prefix-recognisable graph to arbitrary relational structures. We prove that every tree-interpretable structure is finitely axiomatisable in guarded second-order logic with cardinality quantifiers. Note: This is an extended version of the corresponding STACS'02 paper. Best regards, Martin Leucker -- ----------------------------------------------------------------------- | Martin Leucker | Address: | | Department of Computer Science | Lehrstuhl fuer Informatik II | | University of Technology Aachen | Ahornstr. 55 | | Germany | D-52056 Aachen | ----------------------------------------------------------------------- | Tel.: (office) +49/(0)241/80-21210 (private) +49/(0)241/877073 | | Email: leucker(a)informatik.rwth-aachen.de Fax: +49/(0)241/80-22217 | | Web: http://www-i2.informatik.rwth-aachen.de/leucker/ | -----------------------------------------------------------------------

1 0

[tr-announce] Aachen University of Technology, TR Announcement 02/01
by Bollig 13 Feb '01

13 Feb '01

------------------------------------------------------------------------------- \_\_\_ \_ \_ \_\_\_\_\_ \_ \_ Rheinisch- Aachen \_ \_ \_ \_ \_ \_ \_ Westfaelische University \_\_\_ \_ \_ \_ \_ \_\_\_\_ Technische of Technology \_ \_ \_\_ \_\_ \_ \_ \_ Hochschule \_ \_ \_ \_ \_ \_ \_ Aachen _______________________________________________________________________________ Dept. of Computer Science Announcements of new Technical Reports 2/01 ------------------------------------------------------------------------------- WWW at URL: ftp://ftp.informatik.rwth-aachen.de/pub/reports/index.html ~~~~~~~~~~~ Anonymous ftp: ftp.informatik.rwth-aachen.de(137.226.225.3):/pub/reports ~~~~~~~~~~~~~~ Format: gzipped PostScript Files (<number>.ps.gz) ______________________________________________________________________________ TITEL = Deciding LTL over Mazurkiewicz Traces NUMBER = 2001-02 AUTHORS = Benedikt Bollig and Martin Leucker PAGES = 26 ABSTRACT = Linear time temporal logic (LTL) has become a well established tool for specifying the dynamic behaviour 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 further on-the-fly model checking procedures. In this paper we exhibit a decision procedure for LTL over Mazurkiewicz traces which generalises the classical automata-theoretic approach to a linear time temporal logic interpreted no longer over sequences but certain partial orders. Specifically, we construct a (linear) alternating Buechi automaton accepting the set of linearisations of 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 B\"uchi automata corresponds exactly to LTL formulas over Mazurkiewicz traces, lifting a similar result from L\"oding and Thomas formulated in the framework of LTL over words. KEYWORDS = Model Checking, LTL, Mazurkiewicz Traces, Alternating Automata This report is located at ftp://ftp.informatik.rwth-aachen.de/pub/reports/2001/2001-02.ps.gz _______________________________________________________________________________ If you are interested in receiving periodic announcements, subscribe to our mailing-list. Write an e-mail with subject subscribe (your e-mail address) to tr-announce-request(a)informatik.rwth-aachen.de TR-Admin tr-admin(a)informatik.rwth-aachen.de

1 0

[tr-announce] Aachen University of Technology, TR Announcement 08/00
by Bollig 13 Feb '01

13 Feb '01

------------------------------------------------------------------------------- \_\_\_ \_ \_ \_\_\_\_\_ \_ \_ Rheinisch- Aachen \_ \_ \_ \_ \_ \_ \_ Westfaelische University \_\_\_ \_ \_ \_ \_ \_\_\_\_ Technische of Technology \_ \_ \_\_ \_\_ \_ \_ \_ Hochschule \_ \_ \_ \_ \_ \_ \_ Aachen _______________________________________________________________________________ Dept. of Computer Science Announcements of new Technical Reports 8/00 ------------------------------------------------------------------------------- WWW at URL: ftp://ftp.informatik.rwth-aachen.de/pub/reports/index.html ~~~~~~~~~~~ Anonymous ftp: ftp.informatik.rwth-aachen.de(137.226.225.3):/pub/reports ~~~~~~~~~~~~~~ Format: gzipped PostScript Files (<number>.ps.gz) ______________________________________________________________________________ TITLE = Verifying Generic Erlang Client-Server Implementations NUMBER = 00-08 AUTHORS = Thomas Arts and Thomas Noll PAGES = 26 ABSTRACT = The Erlang Verification Tool is an interactive theorem prover tailored to verify properties of distributed systems implemented in Erlang. It is being developed by the Swedish Institute of Computer Science in collaboration with Ericsson. In this paper we present an extension of this tool which allows to reason about the Erlang code on an architectural level. We demonstrate our approach by developing a verification method for client-server systems designed using the generic server implementation of the Open Telecom Platform. Our idea is to specify a set of transition rules which characterize the abstract behaviour of the generic server functions. In this way we can reason in a compositional way about any client-server application without having to consider the concrete implementation details of the generic part, which simplifies proofs dramatically. We argue that, due to the generality of our approach, it is easily possible to put it into practice using other verification tools or to integrate further generic architectural elements such as finite-state machines or event handlers. KEYWORDS = software verification, theorem proving, formal semantics This report is located at ftp://ftp.informatik.rwth-aachen.de/pub/reports/2000/00-08.ps.gz _______________________________________________________________________________ If you are interested in receiving periodic announcements, subscribe to our mailing-list. Write an e-mail with subject subscribe (your e-mail address) to tr-announce-request(a)informatik.rwth-aachen.de TR-Admin tr-admin(a)informatik.rwth-aachen.de

1 0