------------------------------------------------------------------------------- \_\_\_ \_ \_ \_\_\_\_\_ \_ \_ 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@informatik.rwth-aachen.de TR-Admin tr-admin@informatik.rwth-aachen.de