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