Temporal logics are a widespread formalism for the specification of the behaviour exhibited by a system in the course of time. Kamp proved that, if this behaviour is modeled as a sequence of actions, the approach known as linear temporal logic can express the same properties as first-order logic.
When a model represents a distributed system it is desirable to formalize the temporal dependence between its actions as a partial rather than a linear order. Mazurkiewicz traces are an extension of words by the partial commutation $ab = ba$ for certain letters of the alphabet. There are two different approaches which generalize linear temporal logic to Mazurkiewicz traces while preserving its completeness with respect to first-order logic: local temporal logic, which expresses properties from the perspective of single elements of a partial order, and a global approach that can be used to describe states of the system as a whole.
This text presents both approaches, with an emphasis on fragments of the local temporal logic, which are also compared to fragments of first-order logic. All results are obtained with the use of Ehrenfeucht-Fraisse games. These are simple and deterministic non-cooperative games with two players who can place pebbles on the vertices of two traces. The rules are chosen such that a winning strategy for one of the players corresponds to the existence of a logical formula which assumes different truth values for these traces.
--
Temporallogiken sind ein weit verbreiteter Formalismus für die Spezifikation des zeitlichen Verhaltens eines Systems. Falls dieses Verhalten als eine Sequenz von Aktionen dargestellt wird, kann man nach einem Satz von Kamp mit der Linearzeitlogik LTL die gleichen Eigenschaften ausdrücken wie in der Logik erster Stufe.
Für die Modellierung eines verteilten Systems ist es sinnvoll, die zeitliche Abfolge seiner Aktionen als Partialordnung statt als lineare Ordnung darzustellen. Mazurkiewicz-Spuren sind eine Erweiterung von Wörtern um die partielle Kommutativität ab = ba für bestimmte Buchstaben aus dem Alphabet. Zwei verschiedene Ansätze verallgemeinern LTL auf Mazurkiewicz-Spuren und erhalten dabei die Vollständigkeit in Bezug auf die Logik erster Stufe: zum einen die lokale Temporallogik, die Eigenschaften aus der Perspektive einzelner Elemente der Partialordnung formuliert, und zum anderen die globale Linearzeitlogik, die Zustände des Gesamtsystems beschreibt.
Dieser Text stellt die beiden Ansätze vor. Der Schwerpunkt liegt auf der Untersuchung von Fragmenten der lokalen Temporallogik, die auch mit Fragmenten der Logik erster Stufe verglichen werden. Alle Ergebnisse werden mit Ehrenfeucht-Fraisse-Spielen bewiesen. Dabei handelt es sich um einfache und deterministische nichtkooperative Spiele, in denen Marken von zwei Spielern auf die Knoten zweier Spuren gesetzt werden. Die Regeln werden so gewählt, dass eine Gewinnstrategie für einen dieser Spieler der Existenz einer Formel entspricht, die für die beiden Spuren unterschiedliche Wahrheitswerte annimmt.
|