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
