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