A symbolic approach to the state graph based analysis of high-level Markov reward models [Elektronische Ressource] = Ein symbolischer Ansatz für die Zustandsgraph-basierte Analyse von hochsprachlichen Markov-Reward-Modellen / Kai Lampka

Sujets

• Informatik
• Mathematics

Informations

• Publié par: friedrich-alexander-universitat_erlangen-nurnberg
• Publié le: 01 janvier 2007
• Nombre de lectures: 11
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

A symbolic approach to the state graph
based analysis of high-level Markov
reward models
Ein symbolischer Ansatz fur die¨
Zustandsgraph-basierte Analyse von
hochsprachlichen Markov Reward
Modellen
Der Technischen Fakult¨at
der Universitat Erlangen-Nurnberg¨ ¨
zur Erlangung des Grades
DOKTOR-INGENIEUR
vorgelegt von
Kai Matthias Lampka
Erlangen, M¨arz 2007Als Dissertation genehmigt von
der Technischen Fakultat der¨
Universitat¨ Erlangen-Nurn¨ berg
Tag der Einreichung: 27.11.2006
Tag der Promotion: 19.3.2007
Dekan: Prof. Dr.-Ing. Alfred Leipertz
Berichterstatter: Prof. Dr.-Ing. Markus Siegle (Univ. der Bundeswehr Munchen)¨
Prof. Dr.-Ing. Reinhard German (Univ. Erlangen-Nurnberg)¨
Prof. Ph.D. William H. Sanders of Illinois, Urbana-Champaign)Abstract
Markov reward models considered in this thesis are compactly described by means of Marko-
vian extensions of well-known high-level model description formalisms. For numerically com-
puting performance and dependability (= performability) measures of high-level system
models, the latter must be transformed into low-level representations, where the concur-
rency 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. Deci-
sion 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 tech-
niques 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 representations 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 repre-
sentations 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 man-
ner, 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 in-
troduces 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 eval-
uating 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 computa-
tion 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 execu-
tion 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 mod-
els 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.Table of Contents
List of Figures............................................................. IV
List of Algorithms ......................................................... V
List of Tables .............................................................. VI
1 Introduction........................................................... 1
1.1 Motivation ......................................................... 1
1.2 Statespaceexplosionproblemandrelatedapproaches.................... 2
1.3 State-of-thesymbolictechniques....................................... 4
1.4 Contributionsofthisthesis........................................... 7
1.5 Organizationofthethesis ............................................ 7
2 Background Material .................................................. 9
2.1 Organizationofthechapter........................................... 9
2.2 MarkovTheory ..................................................... 9
2.2.1 Continuous-timeMarkovrewardmodel(MRM)................... 9
2.2.2 NumericalsolutionofMRM .................................... 11
2.2.3 Reductiontechniques.......................................... 16
2.2.4 State/Transitionsystems....................................... 19
2.3 High-levelMarkovrewardmodels...................................... 20
2.3.1 High-levelmodeldescriptiontechniques.......................... 21
2.3.2 Specification of performability measures . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.3.3 Compositionofhigh-levelmodeldescriptions...................... 23
2.3.4 Mappingofhigh-levelmodelstoMRMs.......................... 24
2.4 Non-compositionalstategraphconstruction............................. 24
2.5 Compositionalstategraphconstruction ................................ 25
2.5.1 Fundamentals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.5.2 SGcompositionforpureinterleaving............................. 26
2.5.3 SGcompositionforactivitysynchronization...................... 27
2.5.4 SGcompositionforsharingofSVs............................... 28
2.5.5 SGcompositionforreplicationofsubmodels...................... 29
2.5.6 Limitation of Kronecker operator driven composition schemes . . . . . . . 29
3 Zero-suppressed Multi-terminal BDDs:
Concepts, Algorithms and Application................................. 31
3.1 Organizationofthechapter........................................... 31
3.2 BinaryDecisionDiagramsandextensions............................... 32
3.2.1 BinaryDecisionDiagrams(BDDs)............................... 32
3.2.2 Zero-suppressed BDDs (z-BDDs)................................ 37
3.2.3 Multi-terminalBDDs(ADDs)................................... 38
I3.2.4 Zero-suppressed Multi-terminal BDDs (ZDDs) . . . . . . . . . . . . . . . . . . . . 39
3.3 Partially shared ZDDs (pZDDs)....................................... 40
3.3.1 Definitions ................................................... 41
3.3.2 Canonicity of pZDDs .......................................... 43
3.4 Operations on pZDDs................................................ 45
3.4.1 Preliminaries ................................................. 45
3.4.2 Applying binary operators to pZDDs............................. 46
3.4.3 Variants of the pZApply-algorithm............................... 52
3.4.4 Relabelingofvariables......................................... 54
3.4.5 The pZRestrict-operator...................................... 54
3.4.6 The pZAbstract-operator...................................... 54
3.5 Applications........................................................ 56
3.5.1 ZDDbasedrepresentationsofsetsandrelations................... 57
3.5.2 ZDDbasedrepresentationsofmatrices........................... 59
3.5.3 Extending ZDDs for efficiently computing matrix-vector products . . . 66
3.5.4 BeyondDDbasedmatrixrepresentations......................... 69
3.6 Relatedworkandowncontributions................................... 69
4 The Activity/Reward-local Scheme:
Symbolic SG