Modularity and determinism in compositional Markov models

Abstract

Markov chains are a versatile and widely used means to model an extensive variety of stochastic phenomena, but describing a complex system as a monolithic Markov chain is difficult and error-prone. In this thesis we show that we can construct such complex Markov chains in a sound manner through the composition of a number of simple input/output interactive Markov chains (I/O-IMCs), which arise as an orthogonal combination of continuous-time Markov chains and input/output automata). I/O-IMCs come equipped with a modular semantics in terms of interactive jump processes, a novel variation of jump processes. We discuss the phenomenon of non-determinism, arising from the interaction inside such models, and how we can efficiently determine whether a complex I/O-IMC model is deterministic. Finally, we give an example of an application of I/O-IMCs by presenting the Arcade language, which can be used to describe complex dependable systems. In this thesis we show that, by providing a modular semantics for our compositional I/O-IMCs, we achieve the ’triple compositionality’ principal: a simple, but powerful compositional syntax (Arcade), has an interactive and Markovian semantics in terms of I/O-IMCs, which gives an intuitive description of the meaning of each syntactic element. I/O-IMCs themselves then have a stochastic semantics in terms of interactive jump processes which enables us to describe and compute their stochastic properties. This triple compositionality provides a natural, non-monolithic semantics for our high-level syntax and allows us to understand and reason about complex, incomplete, or partially-specified stochastic models.

Markov-Ketten sind ein vielseitiges und weit verbreitetes Mittel zur Modellierung einer Vielzahl von stochastischen Phänomenen, aber es ist schwierig und fehleranfällig, ein komplexes System als monolithische Markov-Kette zu beschreiben. In dieser Arbeit zeigen wir, dass solche komplexen Markov-Ketten auf korrekte Weise durch die Komposition einer Anzahl von einfachen input/output interactive Markov chains (I/O-IMCs), die als orthogonale Kombination von zeitkontinuierlichen Markov-Ketten und input/output automata zustande kommen, konstruiert werden können. I/O-IMCs sind ausgestattet mit einer modularen Semantik in der Form von interaktiven Sprungprozessen, einer neuartigen Variante von Sprungprozessen. Weiterhin diskutieren wir das Phänomen des Nicht-Determinismus, der sich aus der Interaktion innerhalb solcher Modelle ergibt, und wie wir effizient bestimmen können, ob ein komplexes I/O-IMC Modell deterministisch ist. Schließlich geben wir ein Beispiel für eine Anwendung von I/O-IMCs: die Arcade Sprache, die verwendet werden kann, um komplexe zuverlässige Systeme zu beschreiben. In dieser Arbeit zeigen wir, dass wir durch die Beschreibung einer modularen Semantik für unsere I/O-IMCs das ’Triple-Compositionality-Prinzip’ erreichen: eine einfache, aber leistungsfähige kompositionelle Syntax (Arcade), hat eine interaktive und markovsche Semantik in Form von I/O-IMCs, die eine intuitive Beschreibung der Bedeutung der einzelnen syntaktischen Elementen darstellt. I/O-IMCs haben außerdem eine stochastische Semantik in Form von interaktiven Sprungprozessen, die es ermöglicht, ihre stochastischen Eigenschaften zu beschreiben und zu berechnen. Dieses ’Triple-Compositionality-Prinzip’ bietet eine natürliche nicht-monolithische Semantik und erlaubt es, komplexe, unvollständige oder unterspezifierte stochastiche Modelle zu verstehen und zu beschreiben.