|
Interaction in Concurrent Systems
Minnameier, Christoph
|
URL:
|
http://ub-madoc.bib.uni-mannheim.de/2913
|
|
URN:
|
urn:nbn:de:bsz:180-madoc-29133
|
|
Document Type:
|
Doctoral dissertation
|
|
Year of publication:
|
2010
|
|
The title of a journal, publication series:
|
None
|
|
Publishing house:
|
Universität Mannheim
|
|
Evaluator:
|
Majster-Cederbaum, Mila
|
|
Date of oral examination:
|
29 April 2010
|
|
Publication language:
|
English
|
|
Institution:
|
School of Business Informatics and Mathematics > Praktische Informatik II (Majster-Cederbaum -2005, Em)
|
|
Subject:
|
004 Computer science, internet
|
|
Classification:
|
CCS:
Parallelis Relations Reducibili ,
|
|
Subject headings (SWD):
|
Nebenläufigkeit , Komplexität
|
|
Individual keywords (German):
|
Interaktionssysteme , Komponenten-basierte Systeme
|
|
Keywords (English):
|
Interaction Systems , Component-based systems
|
|
Abstract:
|
This dissertation is concerned with the theoretical analysis of component-based models for concurrent systems. We focus on interaction systems, which were introduced by Sifakis et al. in 2003. Centered around interaction systems, we also cover Minsky machines, Petri nets and the Linda calculus and establish relations between the models by giving translations from one to the other. Thus, we gain an insight concerning the expressiveness of the models 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 undecidable. 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 as a motivation for the sufficient condition approach that is presented in the second half of this work: We present a generic approach to prove properties for component-based systems 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 of the global system in polynomial time. We demonstrate our ideas by means of interaction systems and for the property of local deadlock.
|
|
Translation of the title:
|
Interaktionen in nebenläufigen Systemen
(German)
|
|
Translation of the abstract:
|
Diese Dissertation befasst sich mit der theoretischen Analyse komponentenbasierter Modelle für nebenläufige Systeme. Im Mittelpunkt steht dabei das Modell der Interaktionssysteme, welches im Jahr 2003 von Sifakis et al. eingeführt wurde. Im Kontext von Interaktionssystemen betrachten wir Minsky-Maschinen, Petri-Netze und den Linda Kalkül und setzen die verschiedenen Modelle durch Übersetzungen zueinander in Beziehung. Somit erhalten wir einen Einblick in die Ausdrucksstärke der Modelle und erfahren, wie man ein Modell, welches in einer Syntax gegeben ist, mittels einer anderen simulieren kann. Zusätzlich erlauben die genannten Übersetzungen die Folgerung von Komplexitäts- und Entscheidbarkeitsaussagen. Genauer gesagt wird gezeigt, dass die Fragen, ob ein LinCa Prozess terminiert bzw. divergiert unter einer Semantik, die maximalen Fortschritt fordert, unentscheidbar sind. Wir zeigen außerdem, dass die Probleme Erreichbarkeit, Fortschritt, Lokaler und Globaler Deadlock, sowie Verfügbarkeit in Interaktionssystemen PSPACE-vollständig sind. Diese komplexitätstheoretische Klassifizierung dient als Motivation für den Ansatz einer hinreichenden Bedingung, der in der zweiten Hälfte der Arbeit vorgestellt wird: Wir demonstrieren eine allgemeingültige Methode, Eigenschaften von komponenten-basierten Systemen zu beweisen, die eine Zerlegung in Teilsysteme erlauben. Um das Problem der Zustandsraumexplosion zu vermeiden, betrachten wir überlappende Projektionen und berechnen damit Überapproximationen des global erreichbaren Zustandsraums. Wir verbessern die Qualität dieser Überapproximationen dann mit einer Technik, die wir Cross-Checking nennen. Basierend auf den verbesserten Überapproximationen können wir schließlich Eigenschaften des globalen Systems in polynomieller Zeit beweisen. Wir veranschaulichen unsere Ideen anhand von Interaktionssystemen und für die Eigenschaft Lokaler Deadlock.
(German)
|
|
Additional information:
|
|
 | Das Dokument wird vom Publikationsserver der Universitätsbibliothek Mannheim bereitgestellt. |
 Search Authors in
You have found an error? Please let us know about your desired correction here: E-Mail
Actions (login required)
 |
Show item |
|
![[img]](https://madoc.bib.uni-mannheim.de/style/images/fileicons/application_pdf.png)