Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
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 ...