Logics for Mazurkiewicz traces
Martin Leucker
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.