Personal tools
You are here: Home Events Abstract Archives 2001 Deciding LTL over Mazurkiewicz Traces

Deciding LTL over Mazurkiewicz Traces

Martin Leucker RWTH Aachen 4pm Tuesday 21 August 2001 Room 2511, JCMB, King's Buildings

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 talk 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 Büchi 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üchi automata corresponds exactly to LTL formulas over Mazurkiewicz traces, lifting a similar result by Löding and Thomas formulated in the framework of LTL over words.

Document Actions