Principles of Markov automata

A substantial amount of today's engineering problems revolve around systems that are concurrent and stochastic by their nature. Solution approaches attacking these problems often rely on the availability of formal mathematical models that reflect such systems as comprehensively as possible. In this thesis, we develop a compositional model, Markov automata, that integrates concurrency, and probabilistic and timed stochastic behaviour. This is achieved by blending two well-studied constituent models, probabilistic automata and interactive Markov chains. A range of strong and weak bisimilarity notions are introduced and evaluated as candidate relations for a natural behavioural equivalence between systems. Among them, weak distribution bisimilarity stands out as a natural notion being more oblivious to the probabilistic branching structure than prior notions. We discuss compositionality, axiomatizations, decision and minimization algorithms, state-based characterizations and normal forms for weak distribution bisimilarity. In addition, we detail how Markov automata and weak distribution bisimilarity can be employed as a semantic basis for generalized stochastic Petri nets, in such a way that known shortcomings of their classical semantics are ironed out in their entirety.Ein beträchtlicher Teil gegenwärtiger ingenieurwissenschafter Probleme erstreckt sich auf Sys- teme, die ihrer Natur nach sowohl stochastisch als auch nebenläufig sind. Lösungsansätze fußen hierbei häufig auf der Verfügbarkeit formaler mathematischer Modelle, die es erlauben, die Spez- ifika jener Systeme möglichst erschöpfend zu erfassen. In dieser Dissertation entwickeln wir ein kompositionelles Modell namens Markov-Automaten, das Nebenläufigkeit mit probabilistis- chen und stochastischen Prozessen integriert. Dies wird durch die Verschmelzung der zweier bekannter Modellklassen erreicht, und zwar die der probabilistischen Automaten und die der interaktiven Markovketten. Wir entwickeln dabei ein Spektrum verschiedener, starker und schwacher Bisimulationsrelationen und beurteilen sie im Hinblick auf ihre Eignung als natür- liche Verhaltensäquivalenz zwischen Systemen. Die schwache Wahrscheinlichkeitsverteilungs- bisimulation sticht dabei als natürliche Wahl hervor, da sie die probabilistische Verzwei- gungsstruktur treffender abstrahiert als bisher bekannte Bisimulationsrelationen. Wir betra- chten des Weiteren Kompositionalitätseigenschaften, Axiomatisierungen, Entscheidungs- und Minimierungsalgorithmen, sowie zustandsbasierte Charakterisierungen und Normalformen für die schwache Wahrscheinlichkeitsverteilungsbisimulation. Abschließend legen wir dar, dass Markov-Automaten und die schwacheWahrscheinlichkeitsverteilungsbisimulation als Grundlage für eine verbesserte Semantik von verallgemeinerten stochastischen Petrinetzen dienen kann, welche bekannte Mängel der klassischen Semantik vollständig behebt