A symbolic approach to the state graph based analysis of high-level Markov reward models
Kai Lampka · OPUS FAU (Kooperativer Bibliotheksverbund Berlin-Brandenburg (KOBV), on behalf of the Universitätsbibliothek Erlangen-Nürnberg) · 2006
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.