Markov reward models considered in this thesis are compactly described by means of Markovian extensions of well-known high-level model description formalisms. For numerically computing performance and dependability (= performability) measures of high-level system models, the latter must be transformed into low-level representations, where the concurrency contained in the high-level model description is made explicit. This transformation, where a high-level model is mapped onto a (stochastic) state/transition-system, generically denoted as state graph (SG), may therefore yield an exponential blow-up in the number of system states. This problem is known as the notorious state space explosion problem. Decision diagrams (DD) have shown to be very helpful when it comes to the representation of extremely large SGs, easing the restriction imposed on the size and complexity of models and thus systems to be analyzed. However, to efficiently apply contemporary symbolic techniques the high level models must possess either a specific compositional structure and/or the employed modeling formalism must be of a specific kind. This work lift these limitations, where the number of system states, the state probability of wich must be computed, is still the limiting factor of the analysis.--To represent SGs, this thesis extends zero-suppressed'' binary decision diagrams to the case of zero-suppressed'' multi-terminal binary decision diagrams (ZDDs). To deduce the pseudo-boolean function represented by a ZDD's graph correctly, the set of Boolean function variables must be known. Consequently, within a shared DD-environment as it is provided by well-known DD-packages, ZDD-nodes lose their uniqueness. To solve this problem, the concept of partially shared ZDDs (pZDDs) is introduced, so that nodes are extended with sets of function variables. It is shown that pZDDs are canonical epresentations of pseudo-boolean functions. For efficiently working with pZDDs, this thesis also develops a wide range of (symbolic) algorithms. These algorithms are designed in such a way that they allow to implement pZDDs within common, shared DD-environments. --If a model description formalism does not possess a symbolic semantic, symbolic representations of annotated state/transition-systems can only be deduced from its high-level model descriptions by explicit execution. To do so in a memory and run-time efficient manner, this work exploits local information of high-level model constructs only, yielding the activity/reward-local approach. This new semi-symbolic technique comprises the four follwing steps: (a) The activity-local scheme for generating symbolic representation of a high-level model's SG. Since the suggested procedure does not generate all system states explicitly, the use of a symbolic composition scheme is required. The newly developed composition scheme delivers the potential SG and its restriction to the set of reachable transitions is efficiently achieved by making use of symbolic reachability analysis, where this thesis introduces a new quasi'' depth-first-search based algorithm. (b) The reward-local scheme for obtaining symbolic representations of reward functions as defined on the high-level model. Analogously to the above procedure, one explicitly executes the reward functions for evaluating the reward values of states and transitions. But for reducing the number of explicit state visits, the procedure once again exploits local information only. (c) For the computation of state probabilities, this work introduces a ZDD-based variant of the hybrid solution method, developed in the context of other symbolic data structures. (d) Given symbolically represented reward functions and state probabilities, as the next step, one determines the user-defined performability measures of the high-level model, where for this purpose a new graph-traversing algorithm is introduced.--Since the activity/reward-local scheme depends on explicit but in most cases partial execution it is not limited to a certain description technique. Based on a new symbolic composition scheme and contrary to other symbolic approaches, it is still applicable, if the high-level models are neither compositionally constructed nor possess a decomposable structure of a certain kind. Thus this thesis not only introduces a new type of decision diagram and algorithms for efficiently working with it, but also develops a universal symbolic approach for the SG based analysis of high-level Markov reward models with very large SGs.

Markov Reward Modelle, wie sie in dieser Arbeit behandelt werden, sind kompakt durch Markovsche Erweiterungen bekannter hochsprachlicher Modellbeschreibungsformalismen beschrieben. Die Transformation, die ein hochsprachliches Modell auf ein Zustands/Transitionssystem abbildet, allg. auch als Zustandsgraph (ZG)bezeichnet, kann zu einem exponentiellen Wachstum in der Anzahl der Systemzustände führen. Dieses Problem ist als das sog. Zustandsraumexplosionsproblem bekannt. Entscheidungsdiagramme (DD) haben sich als sehr nützlich erwiesen, wenn es um die Repräsentation extrem großer ZG geht. Mit ihrer Hilfe lassen sich nun größere und komplexere Modelle und somit auch Systeme analysieren. Um die zeitgenössischen symbolischen Techniken jedoch anwenden zu können, müssen die zu analysierenden Modelle entweder eine bestimmte kompositionelle Struktur besitzen und/oder ein bestimmter Modellbeschreibungsformalismus verwendet worden sein. Diese Einschränkungen werden in dieser Arbeit beseitigt. --Zur symbolischen Darstellung (stochastischer) ZG erweitert diese Arbeit zero-suppressed'' binäre Entscheidungsdiagramme zu zero-suppressed'' multi-terminalen binären Entscheidungsdiagrammen (ZDD). Um die korrekte Pseudo-Boolesche Funktion, die durch den Graphen eines ZDDs dargestellt werden soll, abzuleiten, muß die Menge der Funktionsvariablen des ZDDs bekannt sein. Als Konsequenz ergibt sich, dass i. Allg. die innerhalb einer gemeinsamen Umgebung, wie sie durch bekannte DD-Programmpakete bereitgestellt werden, allokierten ZDD-Knoten ihre Eindeutigkeit verlieren. Um dieses Problem zu lösen entwickelt diese Arbeit das Konzept der partiell gemeinsamen ZDDs (pZDDs), welches ZDD-Knoten um Funktionsvariablen erweitert. Es wird gezeigt, dass Entscheidungsdiagramme diesen Typs eine kanonische Form der Darstellung von Pseudo-Booleschen Funktionen sind. Um effizient mit pZDDs arbeiten zu können, wird ein breites Spektrum an (symbolischen) Algorithmen entwickelt. Diese Algorithmen sind so konzipiert, dass sie eine Implementierung von pZDDs in gewöhnlichen, gemeinsamen DD-Umgebungen erlauben. --Besitzt ein Modellbeschreibungsformalismus keine symbolische Semantik, so können symbolische Repräsentationen der annotierten Zustands/Transitionssysteme seiner hochsprachlichen Modellbeschreibungen nur dadurch gewonnen werden, dass man die hochsprachlichen Systemmodelle explizit ausführt. Um dies speicher- und zeiteffizient zu tun, verwendet diese Arbeit nur lokale Informationen bzgl. der hochsprachlichen Modellkonstrukte. Der so neu entstandene semi-symbolische Ansatz, den wir als Aktivitäts/Reward-lokalen Ansatz bezeichnen, umfasst nun die folgenden vier Schritte: (a) Das Aktivitäts-lokale Schema zur Generierung der symbolischen Repräsentation des ZG eines hochsprachlichen Modells. Da dieser Ansatz nicht alle Systemzustände explizit erzeugt, ist die Verwendung eines symbolischen Kompositionsschemas nötig. Das hier entwickelte Kompositionsschema erzeugt dabei den potentiellen ZG, seine Einschränkung auf erreichbare Elemente kann allerdings effizient mittels einer symbolischen Erreichbarkeitsanalyse herbeigeführt werden, wobei diese Arbeit einen neuen, quasi'' tiefe-suchenden Algorithmus einführt. (b) Das Reward-lokale Schema um symbolische Repräsentationen der Rewardfunktionen des jeweiligen hochsprachlichen Modells zu erzeugen. Analog zur obigen Vorgehensweise werden dabei die Rewardfunktionen explizit ausgeführt, um die Rewardwerte der Zustände und Transitionen zu bestimmen. Um die Anzahl der expliziten Zustandsbesuche gering zu halten, werden jedoch erneut nur lokale Informationen verwendet. (c) Zur Berechnung der Zustandswahrscheinlichkeiten führt diese Arbeit eine ZDD-basierte Variante des hybriden Lösungsverfahrens, wie es im Kontext anderer symbolischer Datentypen entwickelt wurde, ein. (d) Auf Basis der symbolisch dargestellten Rewardfunktionen und den Zustandswahrscheinlichkeiten, ist man nun in der Lage, die durch den Benutzer spezifizierten Leistungsmaße des hochsprachlichen Modells zu bestimmen, wobei dies mittels eines neuen symbolischen Algorithmus' realisiert wird. --Da der Aktivitäts/Reward-lokale Ansatz auf einer expliziten Ausführung des hochsprachlichen Modells beruht, die in der Praxis wahrscheinlich nur partiell durchgeführt werden muss, ist er nicht auf einen bestimmten Modellbeschreibungsformalismus beschränkt. Basierend auf einem neuen symbolischen Kompositionsschema und im Gegensatz zu anderen symbolischen Ansätzen, ist er auch dann einsetzbar, wenn die hochsprachlichen Modelle weder kompositionell konstruiert, noch eine dekomponierbare Struktur bestimmter Art besitzen. Diese Arbeit entwickelt somit nicht nur einen neuen Typ von Entscheidungsdiagramm und Algorithmen zu seiner effizienten Manipulation, sondern auch einen universellen Ansatz zur ZG-basierten Analyse von hochsprachlichen Markov Reward Modellen mit sehr großen ZG.