\documentclass[11pt,a4paper,twosided]{llncs}
\usepackage{pdfpages}
\usepackage{longtable}
\begin{document}
\pagestyle{empty}
\includepdf[fitpaper,pages={1}]{titlepage.pdf}
%%%%%%%%%% SECOND PAGE
\clearpage
\ \vfill
\noindent The publications of the Department of Computer Science
of {\em RWTH Aachen University} are in general accessible
through the World Wide Web.
{
\begin{center}
\url{http://aib.informatik.rwth-aachen.de/}
\end{center}
}
\clearpage
%%%%%%%%%%
\title{Deciding LTL over Mazurkiewicz Traces}
\author{Benedikt Bollig and Martin Leucker\thanks{Part of this work
was done during the second author's stay at BRICS. He is grateful
for the hospitality and the overall support.}}
\institute{
Lehrstuhl f\"ur Informatik II\\
RWTH Aachen, Germany\\
Email: \email{$\{$bollig, leucker$\}$@informatik.rwth-aachen.de}
}
\date{\today}
\maketitle
\pagestyle{plain}
\begin{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 {\em
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 B\"{u}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 {\em linear} and {\em
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.
\end{abstract}
%
% ---- Your chapters ----
%
\section{Introduction}
Linear time Temporal Logic (LTL) as proposed by Pnueli~\cite{Pnueli77}
has become a well established tool for specifying the dynamic
behaviour of distributed systems. The traditional approach towards
automatic program verification is model checking specifications in
LTL. A basic feature of LTL has been that its formulas are interpreted
over sequences. Typically, such a sequence will model a computation of
a system; a sequence of states visited by the system or a sequence of
actions executed by the system during the course of the computation.
%
% ---- Bibliography ----
%
\bibliographystyle{alpha}
\bibliography{lit}
%
% ---- The other technical reports ----
%
\cleardoublepage
\input{berichte.tex}
\end{document}