A Two-Level Decomposition Scheme for Markovian Process Algebra Models
The concurrent composition of Markov chains quickly leads to the notorious problem of state space explosion, also known as the largeness problem, as the number of involved Markov chains increases. In the context of Markovian Process Algebras (MPAs) this problem is of particular interest, since small and compact model descriptions in form of language terms provided by the MPA may possess huge underlying Markov chains. Of course, many long known counter-strategies to tackle the largeness problem of Markov chains in one way or the other, like, e.g., product-form solutions, lumpability, sparse data structures, nearly-complete decomposability, can also be applied to the Markov chains which are generated by MPA models. Recent research mostly focuses on the classification of syntactical properties on the MPA language term level which ensure the applicability of these strategies.
In this work we propose a novel approach to solve MPA models which explicitly exploits the concurrent nature of the given model. The method involves two levels of compositionality. In the first level, the model is decomposed along points of global synchronisation into several sub-models. These sub-models are solved in isolation, and afterwards the individual results are combined to yield a solution of the entire model. The second level of compositionality concerns the individual sub-models. Under certain conditions each sub-model can be described as the parallel evolution of a number of independent absorbing Markov chains. This independence can be exploited to efficiently solve the sub-models.
As a side result of the consideration of the second level of compositionality, we derive a novel result on cumulative measures of absorbing joint Markov chains. Provided that the marginal processes are independent continuous time Markov chains (CTMCs), the mean time to absorption and the expected total time in a transient set of the joint Markov chain are computed from the marginal CTMCs in a compositional way. Operations on the state space of the joint Markov chain are never carried out, hence, the problem of state space explosion is avoided. The computational effort of our method rather depends on convergence properties of the joint CTMC, i.e., the number of steps until absorption of a discrete time Markov chain embedded in the joint CTMC.
Die nebenläufige Komposition von Markovketten führt mit steigender Anzahl an involvierten Komponenten schnell zum bekannten Problem der Zustandsraumexplosion, auch bekannt als Largeness Problem. Im Kontext von Markovschen Prozess-Algebren (MPA) ist dieses Problem von besonderer Bedeutung, da kleine und kompakte Modellbeschreibungen in Form von Sprachtermen riesige Markovketten repräsentieren können. Viele altbekannte Gegenstrategien zur Zustandsraumexplosion, wie z.B. Produkt-Form-Lösungen, Lumpability, dünnbesetzte Datenstrukturen, können auf die von der jeweiligen MPA erzeugten Markovkette angewendet werden. Die jüngste Forschung konzentriert sich vornehmlich auf die Klassifikation von syntaktischen Eigenschaften auf der MPA Sprachebene, welche die Anwendbarkeit dieser Strategien garantieren.
In der vorliegenden Arbeit schlagen wir einen neuen Ansatz zur Lösung von MPA Modellen vor, der explizit die nebenläufige Struktur des gegebenen Modells ausnutzt. Diese Methode besteht aus zwei Ebenen der Kompositionalität. In der ersten Ebene wird das Modell entlang von globalen Synchronisationspunkten in mehrere Submodelle aufgespalten. Diese Submodelle werden zunächst in Isolation gelöst; anschließend erhält man durch geeignete Kombination der einzelnen Lösungen eine Lösung für das gesamte Modell. Die zweite Ebene der Kompositionalität betrifft die individuellen Submodelle. Unter bestimmten Bedingungen kann jedes Submodell als die parallele Entwicklung mehrerer unabhängiger absorbierender Markovketten beschrieben werden. Diese Unabhängigkeit kann zur Lösung der Submodelle ausgenutzt werden.
Als ein Nebenprodukt der Betrachtung der zweiten Ebene der Kompositionalität, präsentieren wir ein neues Resultat über kumulative Ma\ss{}e gemeinsamer absorbierender Markovketten. Falls die marginalen Prozesse unabhängige kontinuierliche Markovketten sind, können die mittlere Zeit bis zur Absorption, sowie die mittlere Verweilzeit in einer transienten Teilmenge des Zustandsraums aus isolierten Lösungen der marginalen Prozesse zusammengesetzt werden. Da bei dieser Methode keine Operationen auf dem gemeinsamen Zustandsraum ausgeführt werden, umgehen wir das Problem der Zustandsraumexplosion. Der Rechenbedarf unserer Methode hängt von Konvergenzeigenschaften der gemeinsamen Markovkette ab, d.h. von der Anzahl an Schritten bis zur Absorption einer in der gemeinsamen kontinuierlichen Markovkette eingebetteten diskreten Markovkette.
Vorschau
Zitieren
Zitierform:
Zitierform konnte nicht geladen werden.