The following technical report is available from http://aib.informatik.rwth-aachen.de/:
Martin Leucker Logics for Mazurkiewicz traces 2002-10
Abstract: Linear temporal logic (LTL) has become a well established tool for specifying the dynamic behavior 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 on-the-fly model checking procedures.
While this technique extends elegantly to richer domains where the underlying computations are modeled as (Mazurkiewicz) traces, it does so only for event- and location-based temporal logics. In this thesis, we exhibit a decision procedure for LTL over Mazurkiewicz traces which generalizes the classical automata-theoretic approach to a linear temporal logic interpreted no longer over sequences but restricted labeled partial orders. Specifically, we construct a (linear) alternating Buechi automaton accepting the set of linearizations of those 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 Buechi automata corresponds exactly to LTL formulas over Mazurkiewicz traces, lifting a similar result from Loeding and Thomas formulated in the framework of LTL over words.
Additionally, a linear temporal logic with a different flavor is introduced as Foata linear temporal logic (FLTL). It is designed for specifying properties of synchronized systems that comprise clocked hardware circuits or Petri nets supplied with a maximal step semantics.
Distributed synchronous transition systems (DSTSs) are introduced as formal models of these systems and are equipped with a Foata configuration graph-based semantics, which provides a link between these systems and the framework of Mazurkiewicz traces. To simplify the task of defining DSTSs, we introduce a simple calculus in the spirit of CCS.
We give optimal decision procedures for satisfiability of FLTL formulas as well as for model checking, both based on alternating Buechi automata. The model checking procedure further employs an optimization which is similar to a technique known as partial order reduction.
Regards, Volker