Compositional solution of stochastic process algebra models

Bohnenkamp, Henrik; Haverkort, Boudewijn

doi:urn:nbn:de:hbz:82-opus-4101

Compositional solution of stochastic process algebra models

Bohnenkamp, Henrik (Author)

2002

Verantwortlichkeitsangabevorgelegt von Henrik Bohnenkamp

ImpressumAachen : Publikationsserver der RWTH Aachen University 2002

UmfangX, 220 S.

Aachen, Techn. Hochsch., Diss., 2002

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Haverkort, Boudewijn (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2002-02-13

Online
URN: urn:nbn:de:hbz:82-opus-4101
URL: https://publications.rwth-aachen.de/record/61479/files/Bohnenkamp_Henrik.pdf

Einrichtungen

Fakultät für Mathematik, Informatik und Naturwissenschaften (100000)

Inhaltliche Beschreibung (Schlagwörter)
Informatik (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Diese Dissertation behandelt Lösungsverfahren für Markovsche stochachstische Prozeßalgebren mit dem Ziel, das Problem der Zustandsraumexplosion zu vermeiden. Wir untersuchen die Frage, ob die Kompositionalität von SPA-Modellen zur Vermeidung der Zustandsraumexplosion ausgenutzt werden kann. Zuerst konzentrieren wir unsere Untersuchungen auf die Komponenten eines SPA-Modells und leiten einige allgemeine Ergebnisse her, die Aufschluss über die stochastischen Abhängigkeiten zwischen diesen Komponenten geben. Wir identifizieren Wartezeiten, Durchsätze und Verzweigungswahrscheinlichkeiten als die drei wichtigsten Quantitäten, die die Abh"angigkeiten zwischen Komponenten beschreiben und die es erlauben, Leistungsmaße auszudrücken. Wir untersuchen dann eine spezielle Klasse von SPA-Prozessen, die Semi-Markov-Prozesse beschreiben. SPA-Modelle in dieser Klasse können sehr effizient gelöst werden. Ein wichtiger Teilschritt dieser Technik ist dabei die effiziente Berechnung des Mittelwertes des Maximums von phasenverteilten Zufallsvariablen. Ein naiver Ansatz würde sofort zu einem exponentiellem Anwachsen in der Anzahl der Zufallsvariablen zumindest der Lösungszeit führen. Wir stellen jdeoch ein Verfahren vor, dessen Speicherbedarf und Lösungszeit nur polynomial wachsen. Schließlich betrachten wir eine true-concurrency-Semantik für SPA, die auf Ereignis-Strukturen basiert. Letztere ermöglichen eine explizite Darstellung von Parallelität und Lokalität. Wir untersuchen, ob diese Semantik Vorteile bietet für die effiziente Lösung von SPA-Modellen. Wir identifizieren drei grundlegende Quantitäten, mit denen sich Leistungsmaße in Ereignis-Strukturen darstellen lassen. Bedauerlicherweise zeigt ein anderes Ergebnis, daß nur unter starken Einschränkungen Leistungsmaße auch tatsächlich berechnet werden können.

This dissertation is about the solution of Markovian stochastic process algebra (SPA) models and the avoidance of the state-space explosion problem. We try to answer the question whether the compositionality of SPA models can be exploited to overcome the largeness problems appearing when evaluating such models. First, instead of a global view, we take up a local view, i.e. we focus on components of SPA models, and derive some general results about the relation between components. We identify waiting times, throughputs, and branching probabilities as the three quantities that should be known for a compositional performance evaluation strategy. Then, we consider a special class of SPA processes that describe semi-Markov processes. SPA processes in this class are suitable to be solved by a very efficient new technique. An important step in applying this technique is the computation of the mean value of the maximum of phase-type distributed random variables. A naive approach for a computation would require exponential space, but we present an efficient algorithm of polynomial complexity in time and space in the number of considered random variables. Finally, we consider a true-concurrency semantics for SPA models and investigate its use for an efficient solution of SPA models. We identify three important quantities to express performance measures in this semantics. Unfortunately, as we will show, only for very restricted cases the true-concurrency-view on SPA models allows the actual computation of measures.

OpenAccess:
PDF
(additional files)