Interaction in concurrent systems [Elektronische Ressource] / vorgelegt von Christoph Friedrich Minnameier

Sujets

• Informatik

Informations

• Publié par: universitat_mannheim
• Publié le: 01 janvier 2010
• Nombre de lectures: 13
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Interaction in Concurrent Systems
Inauguraldissertation
zur Erlangung des akademischen Grades
eines Doktors der Naturwissenschaften
der Universit¨at Mannheim
vorgelegt von
Christoph Friedrich Minnameier
aus Heidelberg
Mannheim, April 2010Dekan: Professor Dr. Felix Freiling, Universita¨t Mannheim
Referentin: Professor Dr. Mila Majster-Cederbaum, Universita¨t Mannheim
Korreferent: Professor Dr. Ulrich Hertrampf, Universita¨t Stuttgart
Tag der mu¨ndlichen Pru¨fung: 29. April 2010Abstract
This dissertation is concerned with the theoretical analysis of component-
basedmodelsforconcurrentsystems. Wefocusoninteractionsystems, which
were introduced by Sifakis et al. in 2003. Centered around interaction sys-
tems, we also cover Minsky machines, Petri nets and the Linda calculus and
establish relations between the models by giving translations fromone tothe
other. Thus, we gain an insight concerning the expressiveness of the mod-
els and learn, given a system described in one syntax, how to simulate it in
another. Additionally, these translations allow us to deduce complexity and
undecidability results. Namely, we show that the questions whether a LinCa
process terminates or diverges under a maximum progress semantics are un-
decidable. We also prove that the problems of reachability, progress, local
and global deadlock and availability are PSPACE-complete in interaction
systems.
This complexity-theoretic classification serves asamotivationforthesuf-
ficient condition approach that is presented in the second half of this work:
We present a generic approach to prove properties for component-based sys-
tems that allow for decomposition into subsystems. To avoid the problem of
state space explosion, we consider overlapping projections and thus compute
over-approximations of the reachable global state space. We enhance the
quality of these over-approximations by a technique we call Cross-Checking.
Based on the enhanced over-approximations, we may then prove properties
oftheglobalsystem inpolynomialtime. Wedemonstrateourideasbymeans
of interaction systems and for the property of local deadlock.Zusammenfassung
Diese Dissertation befasst sich mit der theoretischen Analyse komponenten-
basierter Modelle fu¨r nebenl¨aufige Systeme. Im Mittelpunkt steht dabei
das Modell der Interaktionssysteme, welches im Jahr 2003 von Sifakis et
al. eingefu¨hrt wurde. Im Kontext von Interaktionssystemen betrachten wir
Minsky-Maschinen, Petri-Netze und den Linda Kalku¨l und setzen die ver-
¨schiedenen Modelle durch Ubersetzungen zueinander in Beziehung. Somit
erhalten wir einen Einblick in die Ausdrucksst¨arke der Modelle und erfahren,
wiemaneinModell,welchesineinerSyntaxgegebenist,mittelseineranderen
¨simulieren kann. Zus¨atzlich erlauben die genannten Ubersetzungen die Fol-
gerung von Komplexit¨ats- und Entscheidbarkeitsaussagen. Genauer gesagt
wirdgezeigt,dassdieFragen,obeinLinCaProzessterminiertbzw. divergiert
unter einer Semantik, die maximalen Fortschritt fordert, unentscheid-
barsind. Wirzeigenaußerdem,dassdieProblemeErreichbarkeit,Fortschritt,
Lokaler und GlobalerDeadlock, sowie Verfu¨gbarkeit in Interaktionssystemen
PSPACE-vollst¨andig sind.
Diese komplexit¨atstheoretische Klassifizierung dient als Motivation fu¨r
den Ansatz einer hinreichenden Bedingung, der in der zweiten H¨alfte der
Arbeit vorgestellt wird: Wir demonstrieren eine allgemeingu¨ltige Methode,
Eigenschaften von komponenten-basierten Systemen zu beweisen, die eine
ZerlegunginTeilsystemeerlauben. UmdasProblemderZustandsraumexplo-
sionzuvermeiden, betrachten wiru¨berlappendeProjektionenundberechnen
¨damit Uberapproximationen des global erreichbaren Zustandsraums. Wir
¨verbessern die Qualit¨at dieser Uberapproximationen dann mit einer Tech-
¨nik, die wir Cross-Checking nennen. Basierend auf den verbesserten Uber-
approximationen k¨onnen wir schließlich Eigenschaften des globalen Systems
in polynomieller Zeit beweisen. Wir veranschaulichen unsere Ideen anhand
von Interaktionssystemen und fu¨r die Eigenschaft Lokaler Deadlock.-
Mensch,
der
um
anderer
willen,
ohne
dass
von
Leiden
Brief
sonst
abarbeitet,
immer
Tor.
Johann
es
jungen
seine
20.
eigene
etwas
Leidenschaft,
ist
sein
ein
eigenes
-
Bedürfnis
Wolfgang
ist,
Goethe
sich
Die
um
des
Geld
Werther,
oder
vom
Ehre
Julius
oder
EinContents
1 Introduction 1
1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Contribution . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.3 Road Map . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2 Models & Equivalences 13
2.1 Characteristic Properties of Models for Concurrent Systems . 15
2.2 Basic Definitions . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.3 Interaction Systems . . . . . . . . . . . . . . . . . . . . . . . . 24
2.4 Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
2.5 The Linda Calculus . . . . . . . . . . . . . . . . . . . . . . . . 39
2.6 Minsky Machines . . . . . . . . . . . . . . . . . . . . . . . . . 46
2.7 Equivalences . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
3 Mappings 53
3.1 Interaction Systems and 1-safe Nets . . . . . . . . . . . . . . . 54
3.2 The various Semantics of the Linda Calculus . . . . . . . . . . 66
4 Undecidability 75
4.1 Overview. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
4.2 Termination is undecidable in MTS-mp-LinCa . . . . . . . . . 77
4.3 Divergence is undecidable in MTS-mp-LinCa . . . . . . . . . . 81
5 Complexity 85
5.1 Overview. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
i