Abstracts and BibTeX-entries of the publications of Kai Lampka
Note that the copyright for papers is held
by the respective publisher, which published the conference proceedings
the resp. paper appeared in.
Can matrix-layout-independent numerical solvers be efficient?
Symbolic approaches based on decision diagrams
have shown to be well suited
for representing very large continuous-time Markov chains (CTMC),
as derived from high-level model descriptions.
Unfortunately, each type of decision diagram requires its own
implementation of the numerical solvers
for computing the state probabilities of the CTMC.
For this reason, some time ago the idea of separating numerical
solution methods from the representation of the CTMC was proposed
[Derisavi:02],
suggesting the implementation
of a so-called state-level abstract functional interface (AFI),
which defines classes of iterators for accessing the entries
of the CTMC transition rate matrix.
In this paper we (a) present an implementation of
the AFI for zero-suppressed
multi-terminal binary decision diagrams (ZDDs) [Lampka:06] and
(b) empirically investigate the viability of
matrix-layout-independent implementations of numerical solvers.
@INPROCEEDINGS{lampka_harwarth_siegle_SMCTools07,
|
author |
= "K. Lampka and S. Harwarth and M. Siegle", |
|
title |
= "{Can matrix-layout-independent numerical solvers be efficient?}"," |
|
booktitle |
= "{Proceedings of the International Workshop on Tools for solving Structured Markov Chains 2007}", |
|
series
|
= {ACM CD edition}, |
|
year |
= {2007}, |
}
A symbolic approach to the state graph based analysis of high-level Markov reward models
Markov reward models considered in this thesis
are compactly described by means of Markovian extensions of
well-known high-level model description formalisms,
such as generalized stochastic Petri nets, stochastic activity networks
and stochastic process algebras, to name only a few of them.
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 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 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.
@PHDTHESIS{lampka07,
|
author |
= "K. Lampka", |
|
title |
= "{A symbolic approach to the state graph based analysis
of high-level Markov Reward Models}"
|
|
School |
= "{University Erlangen-Nuremberg}", |
|
year |
= {2007}, |
}
An easy-to-use, efficient tool-chain to
analyze the availability of
telecommunication equipment
The
tool OpenSESAME offers an easy-to-use modeling framework, which
allows realistic availability and reliability analysis of
fault-tolerant systems. On the other hand our symbolic engine, which is
based on an extension of binary decision diagrams (BDDs), is capable of
analyzing Markov reward models,
clearly consisting of more than 100 mio. system states. In this paper
we therefore introduce a tool chain, where OpenSESAME is employed for
specifying models of fault-tolerant systems. At the backend our
symbolic engine is employed for carrying out numerical Markov reward
analysis. For illustrating the applicability of this approach, we
analyze a model of a fault-tolerant telecommunication service system
with N redundant modules, where
the system is available as long as at least K modules are available.
Based on this model, it will be shown, that the suggested tool chain
has more modeling power than traditional combinatorial methods, e.g.
simple reliability block diagrams or fault-trees, is still easy-to-use
if compared with other high-level model description techniques, and
still allows the analysis of complex system models, where other tools
such as DSPNexpress fail.
@INPROCEEDINGS{lampka_siegle_FMICS06,
|
author |
= "K. Lampka and Markus Siegle", |
|
title |
= "{An
easy-to-use, efficient tool-chain to analyze the availability
of
telecommunication equipment}", |
|
booktitle |
= "{Proceedings of Formal Methods on Industrial Critical
Systems 2006}", |
|
series
|
= {LNCS 4346}, |
|
year |
= {2006}, |
|
pages
|
= {35-50}, |
}
Analysis
of Markov Reward Models using Zero-suppressed Multi-terminal
Binary Decision Diagrams
High-level stochastic description
methods such as stochastic Petri nets, stochastic UML statecharts etc.,
together with specifications of performance variables (PVs), allow a
compact description of systems and quantitative measures of
interest.The underlying Markov reward models (MRMs) often exhibit a
significant blow-up in size,
commonly known as the state space explosion problem. In this paper we
employ our
recently developed type of symbolic data structure,
zero-suppressed multi-terminal binary decision diagram (ZDD).
But in addition to our earlier work [Lampka:06] the following
innovations are introduced:
(a) new algorithms for efficiently generating ZDD-based representation
of user-defined PVs, (b) a new ZDD-based variant of the approach of
[Parker:02] for computing state probabilities, and (c) a new
ZDD-based algorithm for computing moments of the PVs. Our contributions
give one a ZDD-based framework, which allows the computation of complex
performance and reliability measures of high-level system
specifications, whose underlying MRMs consist of more than $10^8$
states. The proposed algorithms for generating user-defined PVs and
computing their moments are in principle independent of the employed
symbolic data type. Thus they are highly suited to fit into other
symbolic frameworks as realized in popular performance evaluation
tools. The efficiency of our approach, which we incorporated into the
Moebius modeling framework [Moebius:02], is demonstrated by
analyzing several benchmark models from the literature and comparing
the obtained run-time data to other techniques.
@INPROCEEDINGS{lampka_siegle_ValueTools06,
|
author |
= "K. Lampka and Markus Siegle", |
|
title |
= "{Analysis of Markov Reward Models using
Zero-supressed Multi-terminal decision diagramms}", |
|
booktitle |
= "{Proceedings of VALUETOOLS 2006 (CD-edition)}", |
|
publisher
|
= {ACM}, |
|
year |
= {2006}, |
}
Abstract
(MMB2006):
This paper
introduces a new, efficient method for deriving compact symbolic
representations of very large (labelled) Markov chains resulting from
high-level model specifications such as stochastic Petri nets,
stochastic process algebras, etc.. This so called ``activity-local''
scheme is combined with a new data structure, called zero-suppressed
multi-terminal binary decision diagram, and a new efficient
``activity-oriented'' scheme for symbolic reachability analysis.
Several standard benchmark models from the literature are analyzed in
order to show the superiority of our approach.
@INPROCEEDINGS{lampka_siegle_MMB:06a,
|
author |
= "K. Lampka and Markus Siegle", |
|
title |
= "{Activity-Local Symbolic State Graph Generation for
High-Level Stochastic Models}", |
|
booktitle |
= "{Meassuring, Modelling, and Evaluation of Systems 2006}", |
|
month
|
= {April}, |
|
year |
= {2006}, |
|
pages
|
= {245-264},
|
}
Abstract (TechReportNr2005-02):
This report extends the activity-local symbolic state graph
representation and generation scheme developed in technical report
TechReportNr0203.
To a general class of models, since earlier publications lacked the
possibility of handling models, where the sequential execution of
independent activites may lead to new model behaviour.
We introduce a new, efficient method for constructing compact symbolic
representations of very large stochastic labelled transition systems.
Contrary to known symbolic state space generation techniques, our
technique is applicable to general high-level models which do not have
to possess any particular structure. The method is based on
zero-suppressed binary decision diagrams which we extended to the
multi-terminal case. The symbolic representation is obtained by
evaluating the semantics of the high-level model.During this step of
explicit state graph exploration one constructs a seperate symbolic
representation of all transition induced by the same activity in an
on-the-fly fashion. The obtained ``activity-local'' structures are
finally composed in order to obtain a compact symbolic representation
of the state graph of the overall system. For the then required step of
symbolic reachability analysis we propose a new, sequential and
activity-oriented scheme which leads to better run-times than
conventional symbolic reachability computation.
Comparing our new method to previously published schemes, the paper
demonstrates
the following advantages:
- The approach is applicable to a general class of high-level
stochastic models.
- In partial-order style we avoid the explicit generation of
shuffled sequences of independent activities, which results in much
higher generation speed.
- The composition scheme, as well as the new data structure,
results in extremely compact symbolic representations.
- Furthermore, the comopsition scheme does not require any
product-form of the models sub-units to be composed, as in case of the
Kronecker-based approaches.
The proposed variant of symbolic reachability analysis significantly
reduces run-time,
where other symbolic SG representation methods, e.g. like the ones
implemented in the tools CASPA and PRSIM,
may benefit from.
@TechReport{Lampka_Siegle_TR2005_02,
|
author |
= "K. Lampka and Markus Siegle", |
|
title |
= "{Activity-Local Symbolic State Graph Generation for
High-Level Stochastic Models}", |
|
institution |
= "{Institute for Computer Enginering, Design of Computing-
and Communication Systems at the Universität der Bundeswehr
München}", |
|
number |
= {2005-02}, |
|
year |
= {2005}, |
}
Activity-local
symbolic State Graph Representation within the Möbius Modeling
Framework
Abstract (TechReportNr0603):
This report extends the activity-local symbolic state graph
representation and generation scheme developed in technical report TechReportNr0203.
The here made contributions focuses on employing the activity-local
symbolic state graph representation within the Möbius performance
evaluation tool. I.e. first of all we will introduce some aspects of
the
Möbius modelling tool. This will be rounded by recapitulating some
aspects of reduced SG construction as well as the main idea of
activity-local symbolic state graph representation and
generation. Secondly we will reason about the correctnes and
completness of the latter, as well as discussing some mayor differences
between our symbolic approach and others, Kronecker-based ones. The
report will be rounded by introducing a method for handling explicitly
modeled symmetries, as induced by Möbius' Rep/Join operator, on
the level of the activity-local scheme, where we will also cover the
symbolic handling of reward variables.
BibTeX-Entry:
@TechReport{Lampka_TR0603,
|
author |
= "K. Lampka", |
|
title |
= "{Activity-local State symbolic Graph Generation within
the Moebius Modeling Framework}", |
|
institution |
= "{Institute of Computer Science, Chair for Computer
Networks and Communication Systems at the
Friedrich-Alexander-Universität Erlangen-Nuremberg}", |
|
number |
= {06/03}, |
|
year |
= {2003}, |
}
Abstract (PMCCS6_0903)
We describe a method for
constructing compact representations of labelled continuous-time Markov
chains which
are derived from high-level model descriptions, such as stochastic
Petri
nets, stochastic process algebras, etc.. Our approach extends existing
techniques in that symbolic (i.e. MTBDD-based) representations are
constructed for
non-modular, flat model descriptions. The symbolic representation of
the
overall model is obtained by merging symbolic activity-local
representations of transitions. Such a scheme will not only yield a
compact symbolic representation, we also show that the state space of
the overall model may only need to
be explored explicitly in parts. The actual reachability analysis is
then
carried out symbolically. The approach illustrated here is well suited
for
performance evaluation tools where the high-level description is mapped
onto the corresponding state graph in a monolithic manner. By applying
this
scheme one can expect both runtime and memory savings.
BibTeX-Entry:
@proceedings{LampkaSiegle_PMCCS0903,
|
author |
= "K. Lampka and M. Siegle", |
|
title |
= "{MTBDD-based Activity-local State Graph Geneartion}",
|
|
booktitle
|
= "{Proc. of The Sixth Int. Workshop on Performability
Modeling of Computer and Communication Systems, Monticello (IL) USA}",
|
|
month
|
= {September 5-7}, |
|
year |
= {2003}, |
}
Abstract (ICALP_WorkshopPetriNets03)
We describe a method for constructing compact representations of
labelled continuoustime Markov chains which are derived from high-level
model descriptions, such as stochastic Petri nets, stochastic process
algebras, etc.. Our approach extends existing techniques in that
symbolic (i.e. BDD-based) representations are constructed for
non-modular, flat model descriptions. It is well suited for performance
evaluation tools such as M"obius, where the high-level
description is mapped onto the corresponding state graph in a
monolithic
manner. The symbolic representation of the overall model is obtained by
merging symbolic activity-local representations of transitions. Such a
scheme
will not only yield a compact symbolic representation, it also has the
advantage
that the state space of the overall model may only need to be explored
partially.
BibTeX-Entry:
@proceedings{LampkaSiegle_ICALP_WorkshopPN03,
|
author |
= "K. Lampka and M. Siegle", |
|
title |
= "{Symbolic Activity-Local State Graph Generation in
the Context of Moebius}", |
|
booktitle
|
= "{Proc. of the Satelite Workshop on Stochastic Petri
Nets and related Formalisms at the 30'th International Colloquium on
Automata, Languages and Programming, Eindhoven, Netherlands}",
|
|
month
|
= {June 28-29}, |
|
year |
= {2003}, |
}
Z-BDD-based
State Space Representation for Monolithic Model Descriptions
Abstract (TechReportNr0203):
This paper describes a method for constructing compact representations
for low-level models (state graphs), where the latter are derived from
highlevel model descriptions, such as stochastic Petri nets, stochastic
process algebras etc. The here illustrated approach extends the so far
made contributions in two ways. First the reduction rules for Z-BDDs
[Minato'93] are employed on multi-terminal decision diagrams, yielding
Z-MTBDDs, in order to reduce space complexity. Secondly symbolic model
representation is applied in
the context of flat or non-modular high-level model descriptions. As a
consequence of the introduced scheme of activity-local state space
generation
and composition, the prerequisite of hierarchically structured
high-level
models, or their a posteriori partitioning in order to gain a compact
symbolic
representation of the underlying state graph, can be dropped. However
the
suggested scheme will not only benefit from the compact symbolic state
space representation, the state space of the overall model may need
only
to be explicitly explored in parts. The state space of the overall
model
will be obtained by composing the symbolic activity-local state space
representations.
Therefore the here illustrated approach is highly suited for
performance
evaluation tools, such as M"obius, where the high-level models are
mapped
onto their respective low-level representations (state graph) in a
monolithic
manner. As a result one can expect runtime and memory space savings.
BibTeX-Entry:
@TechReport{Lampka_TR0203,
|
author |
= "K. Lampka", |
|
title |
= "{Z-BDD-based State Space Representation for
Monolithic Model Descriptions}", |
|
institution |
= "{Institute of Computer Science, Chair for Computer
Networks and Communication Systems at the
Friedrich-Alexander-Universität Erlangen-Nuremberg}", |
|
number |
= {02/03}, |
|
year |
= {2003}, |
}
Abstract (Kuntz_Lampka_ProbSSpExp02):
Several methods have been developed to validate the correctness and
performance of hard- and software systems. One way to do this is to
model the system and carry out a state space exploration in order to
detect all possible states. In this paper, a survey of existing
probabilistic state space exploration methods is given. The paper
starts with a thorough review and analysis of bitstate hashing, as
introduced by Holzmann. The main idea of this initial approach is the
mapping of each state onto a specific bit within an array by employing
a hash function. Thus a state is represented by a single bit, rather
than by a full descriptor. Bitstate hashing is efficient concerning
memory and runtime, but it is hampered by the non deterministic
omission of states. The resulting positive probability of producing
wrong
results is due to the fact that the mapping of full state descriptors
onto
much smaller representatives is not injective. -- The rest of the paper
is devoted to the presentation, analysis, and comparison of
improvements
of bitstate hashing, which were introduced in order to lower the
probability
of producing a wrong result, but maintaining the memory and runtime
efficiency.
These improvements can be mainly grouped into two categories: The
approaches
of the first group, the so called multiple hashing schemes, employ
multiple
hash functions on either a single or on multiple arrays. The approaches
of the remaining category follow the idea of hash compaction. I.e. the
diverse
schemes of this category store a hash value for each detected state,
rather
than associating a single or multiple bit positions with it, leading to
persuasive reductions of the probability of error if compared to the
original
bitstate hashing scheme.
BibTeX-Entry:
@inproceedings{Kuntz_Lampka_ProbSSpExp02,
|
author |
= "M. Kuntz and K. Lampka", |
|
title |
= "{Probabilistic Methods in State Space Analysis}", |
|
booktitle |
= "{Validation of Stochastic Systems}", |
|
editor |
= {C. Baier , B. R. Haverkort, H. Hermanns, J.-P. Katoen,
M. Siegle}, |
|
pages |
= {339-383}, |
|
year |
= {2004}, |
|
series
|
= {LNCS 2925}, |
}
Abstract (MMB_Hamburg02):
This paper describes how to construct complex performability models in
the context of the software tool Moebius, by hierarchically composing
small submodels. In addition to Moebius' "Join" operator,
a second composition operator "Sync" is introduced, and it is shown how
both types of composition can be realised on the basis of symbolic,
i.e. BDD-based data structures.
BibTeX-Entry:
@inproceedings{LampkaSiegle_MMB02,
|
author |
= "K. Lampka and M. Siegle", |
|
title |
= "{Symbolic Composition within the Moebius Framework}",
|
|
booktitle |
= "{Proceedings of the 2'nd MMB Workshop}", |
|
editor |
= {B. Wolfinger and K. Heidtmann}, |
|
pages |
= {63-74}, |
|
note |
= "{Forschungsbericht Nr. 242 der Universit{\"a}t Hamburg
Fachbereich Informatik}", |
|
year |
= {2002}, |
|
month |
= {September}, |
}