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!
[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!
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
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
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/ |
-----------------------------------------------------------------------
-------------------------------------------------------------------------------
\_\_\_ \_ \_ \_\_\_\_\_ \_ \_ 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
-------------------------------------------------------------------------------
\_\_\_ \_ \_ \_\_\_\_\_ \_ \_ 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