# abstracts.html

abstracts.html — HTML, 48 kB (49.172 bytes)

## Dateiinhalt

<HTML>

<BODY bgcolor="white">

<H1>Abstracts of the publications of
<A HREF="http://www.unibw.de/inf4/personen/prof/ms">
Markus Siegle</A></H1>

<A NAME="siegle_habil">
<BLOCKQUOTE>
<HR>
<B>Abstract (siegle_habil):</B><BR>
In this habilitation thesis ("Habilitationsschrift"),
we describe novel techniques for analysing the
behaviour of complex communication systems by means of advanced
stochastic modelling.
We are interested in performance and dependability properties
(which aspects are subsumed by the term "performability")
and focus on Markovian models derived from high-level specifications.
It is well known that the notorious problem of state space explosion
can make the storing and analysis of large models difficult or even
infeasible in practice.
We approach this problem by
exploiting the structure of the system to be modelled.
For compositional model specification we advocate the use of
stochastic process algebras (SPA), which offer
composition operators for building large models from small components
and enable a compositional reduction of the state space on the
basis of bisimulation equivalences.
For compact model representation
we use binary decision diagrams (BDD) and extensions thereof.
It is shown that such symbolic representations can be extremely
space-efficient, provided that they are built according to the
compositional structure as given by the high-level model specification.
We describe a comprehensive set of model construction and analysis
techniques which rely completely on the symbolic data structures.
These include the BDD construction
from explicit representations, symbolic parallel composition,
reachability analysis, elimination of instable states
(which are caused by immediate transitions),
computation of bisimilar states and numerical analysis, which latter
is needed for determining the performability measures of the system.
It turns out that the runtime of numerical computations, in particular
of linear algebraic operations, is currently the bottleneck of the
symbolic approach.
We provide a systematic analysis of this problem and propose
possible solutions for speeding up BDD-based numerical analysis.
Then we focus our attention on the type of measure
that can be specified and analysed.
Traditionally, the purpose of modelling has been to
derive state, throughput or more general reward measures.
It is shown that such classical measures are often not sufficient when
studying complex behavioural properties of interest.
Therefore we develop a temporal logic for specifying a more general class
of performability properties.
This logic is based on actions rather than
on elementary state properties and therefore ideally suited to
be used in conjunction with SPA models.
We describe model checking for this logic, i.e. algorithms
for checking whether a certain property actually holds for a given model,
and point out that this type of analysis fits in well
with our symbolic approach to model representation.
Throughout this thesis we refer to software tools that support the
described techniques, discussing special features of the tools that
were developed during the course of this work.
These tools are also employed to carry out the application case studies
which are described towards the end of the thesis.
</BLOCKQUOTE>
</A>

<A NAME="siegle_diss">
<BLOCKQUOTE>
<HR>
<B>Kurzfassung (siegle_diss):</B><BR>
In dieser Arbeit geht es um die Leistungsbewertung von parallelen und
verteilten Rechensystemen mit Hilfe von Markovmodellen. Es werden
Methoden zur Beschreibung und Analyse von Markovmodellen mit grossem
Zustandsraum untersucht. Stochastische Automaten, stochastische
Prozessalgebren, stochastische Petrinetze und Warteschlangenmodelle werden
als gebraeuchliche Methoden fuer die Modellbeschreibung anhand eines
gemeinsamen Beispielproblems vorgestellt und anschliessend bezueglich
einschlaegiger Kriterien verglichen. Fur ein effizientes Vorgehen bei der
Modellierung grosser Systeme gibt es unterschiedliche Ansaetze, die in der
Arbeit diskutiert und zum Teil erweitert werden. Ein zentraler Inhalt
der Arbeit ist die Entwicklung einer neuen Modellwelt, die sich durch
eine strukturierte Beschreibung des Gesamtmodells, aufgebaut aus
interagierenden Submodellen, auszeichnet. Diese Modellwelt ist besonders
geeignet zur Beschreibung von Systemen mit replizierten Komponenten. Sie
beinhaltet einen effizienten Reduktionsalgorithmus, mit dessen Hilfe der
Zustandsraum eines Modells unter Umstaenden dramatisch reduziert werden
kann. Diese Zustandsraumreduktion hat den zusaetzlichen Vorteil, dass sie
in Verbindung mit einer strukturierten numerischen Analyse eingesetzt
werden kann. Dem Zustandsraumproblem wird also in der neuen Modellwelt
durch zwei sich gegenseitig ergaenzende Methoden Rechnung getragen.
</BLOCKQUOTE>
</A>

<BLOCKQUOTE>
<B>Summary (siegle_diss):</B><BR>
This thesis addresses problems which arise during performance evaluation
of parallel and distributed computer systems using Markov models.
Methods for the description and analysis of Markov models with large
state space are studied. Stochastic automata, stochastic process
algebras, stochastic Petri nets and queueing models are commonly used
model description methods. They are explained by means of a common
example. A comparison of these methods is then given, using a set of
relevant criteria. Different approaches to the efficient modelling of
large systems are discussed and partially extended. One major part of
this work is the development of a new modelling environment which is
characterized by a structured description of the overall model,
consisting of communicating submodels. This environment is especially
suited for describing systems with replicated components. It contains a
reduction algorithm which, under certain circumstances, allows to reduce
a model's state space dramatically. This kind of state space reduction
can also be used in combination with structured numerical analysis.
Therefore, our modelling environment provides two methods for dealing
with the state space explosion problem.</BLOCKQUOTE>
</A>

<A NAME="mmbbook">
<BLOCKQUOTE>
<HR>
<B>Zusammenfassung (mmbbook): </B><BR>
Die Entwicklung von Rechensystemen in Hard- und Software ist  seit  den
sechziger Jahren stets von Leistungsmessungen und Leistungsmodellierung
begleitet gewesen. Dennoch muss man bis heute feststellen,  dass nur ein
Bruchteil der Forschung auf dem Gebiet der  Leistungsbewertung
fruchtbare Anwendung findet. Ferrari  spricht 1986 selbstkritisch von
der  Selbstisolation der Leistungsbewertung innerhalb der Informatik:
"The study of performance evaluation as an independent subject has
sometimes caused researchers in the area to lose contact with reality".
Dieses Buch will einen Beitrag dazu leisten, die von Ferrari
angesprochene Selbstisolation der Leistungsbewertung innerhalb der
Informatik zu durchbrechen und die Leistungsbewertung zu einem
integralen Bestandteil der Systementwicklung zu machen. Die Wirklichkeit
ist aber noch weit von der Idealvorstellung  entfernt, dass Systeme
ausgehend von einer funktionalen und leistungsbezogenen Spezifikation
entworfen und implementiert werden. So meint Goos im Informatik Spektrum
17(1): "... der Programmiertechniker (muss sich) in der Praxis
hauptsaechlich mit der Weiterentwicklung und Aufarbeitung bestehender
Software bescheaftigen, deren Entwicklungsmethodik er nicht kennt und die
nur mangelhaft dokumentiert ist.". Dieser Situation wird im Buch
insoweit Rechnung getragen, als  Methoden vorgestellt werden, die  man
auch dann erfolgreich einsetzen kann, wenn es erst a posteriori zu einer
Leistungsanalyse kommt. Die  Mess- und Modellierungsmethoden werden
jeweils zusammen mit unterstuetzenden Werkzeugen behandelt.
</BLOCKQUOTE>
</A>

<A NAME="Valuetools_2006">
<BLOCKQUOTE>
<HR>
<B>Abstract (Valuetools_2006): </B><BR>
High-level stochastic description methods such as stochastic Petri nets, stochastic UML statecharts etc.,
together with specifications of performance variables (PVs),
enable 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).
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 for computing state probabilities, and
(c) a new ZDD-based algorithm for computing moments of the PVs.
These contributions yield 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 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 the presented approach,
which we incorporated into the Moebius modeling framework,
is demonstrated by analyzing several benchmark
models from the literature and comparing the obtained run-time data to other techniques.
</BLOCKQUOTE>
</A>

<A NAME="FMICS_2006">
<BLOCKQUOTE>
<HR>
<B>Abstract (FMICS_2006): </B><BR>
The tool OpenSESAME offers an easy-to-use modeling framework which enables
realistic availability and reliability analysis of fault-tolerant systems.
Our symbolic engine, which is based on an extension of binary decision
diagrams (BDDs), is capable of analyzing Markov reward models
consisting of more than $10^8$ system states.
In this paper, we introduce a tool chain where OpenSESAME is employed for
specifying models of fault-tolerant systems, and at the back end 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 is 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 to other high-level model description techniques,
and allows the analysis of complex system models
where other tools fail.
</BLOCKQUOTE>
</A>

<A NAME="SPIN_2006">
<BLOCKQUOTE>
<HR>
<B>Abstract (SPIN_2006): </B><BR>
This paper presents IM-SPDL, a stochastic extension of the modal logic PDL,
which supports the specification of complex performance and dependability requirements.
The logic is interpreted over extended stochastic labelled transition systems (ESLTS),
i.e. transition systems containing both immediate and Markovian transitions.
We define the syntax and semantics of the new logic and show that
IM-SPDL provides powerful means to specify path-based properties with timing restrictions.
In general, paths can be characterised by regular expressions, also called programs,
where the executability of a program may depend on the validity of test formulae.
For the model checking of IM-SPDL time-bounded path formulae,
a deterministic program automaton is constructed from the requirement.
Afterwards the product transition system between
this automaton and the ESLTS is built and subsequently
transformed into a continuous time Markov Chain (CTMC)
on which numerical analysis is performed.
Empirical results given in the paper show that model checking IM-SPDL can be
realised efficiently in practice.
</BLOCKQUOTE>
</A>

<A NAME="mbmv_2006">
<BLOCKQUOTE>
<HR>
<B>Abstract (mbmv_2006): </B><BR>
Finite state machines are considered in a probabilistic environment
that is generated by a Markov chain. An expressive temporal logic is
introduced for specifying complex requirements that the FSM should satisfy
in the given environment. The corresponding model checking algorithm
is described and its symbolic implementation is sketched.
Throughout the paper, the method is illustrated by a simple running example.
</BLOCKQUOTE>
</A>

<A NAME="MMB_2006_Activity">
<BLOCKQUOTE>
<HR>
<B>Abstract (MMB_2006_Activity): </B><BR>
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.
</BLOCKQUOTE>
</A>

<A NAME="MMB_2006_CASPA">
<BLOCKQUOTE>
<HR>
<B>Abstract (MMB_2006_CASPA): </B><BR>
This note describes the new features of the performance evaluation tool CASPA,
which has been extended by algorithms for the model checking of stochastic systems.
CASPA uses stochastic process algebras as its input language.
Multi-terminal binary decision diagrams (MTBDD) are
employed to represent the
transition system underlying a given process algebraic specification.
The specification of performability requirements can be done using a newly developed
stochastic temporal logic.
All phases of modelling, from model construction to model checking and
numerical analysis, are based entirely on MTBDDs.
</BLOCKQUOTE>
</A>

<A NAME="dsn_pds_2004">
<BLOCKQUOTE>
<HR>
<B>Abstract (dsn_pds_2004): </B><BR>
In this paper we introduce the logic asCSL, an extension of continuous stochastic logic (CSL),
which provides powerful means to characterise execution paths of action- and state-labelled Markov
chains. In asCSL, path properties are characterised by regular expressions over actions and state-formulas
(which play the role of tests). Thus, the executability of a path not only depends on the available
actions but also on the validity of certain state formulas in intermediate states. Our main result is
that the model checking problem for asCSL can be reduced to CSL model checking on a modified Markov
chain, which is obtained through a product automaton construction. We provide a case study of a
scalable cellular phone system which shows how the logic asCSL and the model checking procedure can
be applied in practice.
</BLOCKQUOTE>
</A>

<A NAME="epew_2004">
<BLOCKQUOTE>
<HR>
<B>Abstract (epew_2004): </B><BR>
This paper describes the tool CASPA, a new performance evaluation tool
which is based on a Markovian stochastic process algebra. CASPA uses
multi-terminal binary decision diagrams (MTBDD) to represent the
labelled continuous time Markov chain (CTMC) underlying a given process algebraic specification.
All phases of modelling, from model construction to numerical analysis and measure computation,
are based entirely on this symbolic data structure. We present several case studies
which demonstrate the superiority of CASPA over sparse-matrix-based process algebra tools.
Furthermore, CASPA is compared to other symbolic modelling tools.
</BLOCKQUOTE>
</A>

<A NAME="jlap_2003">
<BLOCKQUOTE>
<HR>
<B>Abstract (jlap_2003): </B><BR>
This paper describes how to employ Multi Terminal Binary
Decision Diagrams (MTBDD)
for the construction and analysis of a general class of models
that exhibit stochastic, probabilistic and non-deterministic behaviour.
It is shown how the notorious problem of state space explosion
can be circumvented by compositionally constructing symbolic
(i.e. MTBDD-based)
representations of complex systems from small-scale components.
We emphasise, however, that compactness of the representation
can only be achieved if heuristics are applied with
insight into the structure of the system under investigation.
We report on our
experiences concerning compact representation,
performance analysis and
verification of performability properties.
</BLOCKQUOTE>
</A>

<A NAME="sttt_2003">
<BLOCKQUOTE>
<HR>
<B>Abstract (sttt_2003): </B><BR>
Markov chains are widely used in the context of performance
and reliability modeling of systems of various nature. Model checking of such
chains with respect to a given (branching) temporal logic formula has been
proposed for both the discrete and the continuous time
setting.  In this paper, we describe a prototype model
checker for discrete and continuous-time Markov chains, the
Erlangen-Twente Markov Chain Checker (ETMCC), where properties are
expressed in appropriate extensions of CTL.
We illustrate the general benefits
of this approach and discuss the structure of the tool.
Furthermore we report
on successful applications of the tool to some examples, highlighting
lessons learned during the development and application of ETMCC.
</BLOCKQUOTE>
</A>

<A NAME="eindhoven03_lampkasiegle.ps.gz">
<BLOCKQUOTE>
<HR>
<B>Abstract (eindhoven03_lampkasiegle): </B><BR>
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. BDD-based) representations are
constructed for non-modular, flat model descriptions. It is well
suited for performance evaluation tools such as Mobius, 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.
</BLOCKQUOTE>
</A>

<A NAME="pmccs03_lampkasiegle.ps.gz">
<BLOCKQUOTE>
<HR>
<B>Abstract (pmccs03_lampkasiegle): </B><BR>
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.
</BLOCKQUOTE>
</A>

<A NAME="pmccs03_kuntzsiegle_2003">
<BLOCKQUOTE>
<HR>
<B>Abstract (pmccs03_kuntzsiegle): </B><BR>
We present stochastic PDL (SPDL),
a stochastic extension of the modal logic PDL (propositional dynamic logic),
which is interpreted over labelled continuous time Markov chains (CTMC).
This logic allows one to specify complex path-based performability
measures and check their validity automatically.
We define the syntax and semantics of SPDL.
In this logic, computation paths can be characterised by regular
expressions, also called programs, where the
executability of a regular expression may depend on the
validity of test formulae.
For model checking SPDL path formulae, we transform programs
into a variant of deterministic finite automata,
and then build the product automaton between this automaton
and the labelled CTMC.
The paper contains a small example that illustrates the model
checking procedure.
</BLOCKQUOTE>
</A>

<A NAME="caspa_illinois_2003">
<BLOCKQUOTE>
<HR>
<B>Abstract (caspa_illinois_2003): </B><BR>
This note describes the tool CASPA, a new performance evaluation tool
which is based on a Markovian stochastic process algebra. CASPA uses
multi-terminal binary decision diagrams (MTBDD) to represent the
transition systems underlying a given process algebraic specification.
All phases of modelling, from model construction via numerical analysis
to the computation of performance measures,
are based entirely on this symbolic data structure.
</BLOCKQUOTE>
</A>

<A NAME="MMB_Hamburg02">
<BLOCKQUOTE>
<HR>
<B>Abstract (MMB_Hamburg02): </B><BR>
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.
</BLOCKQUOTE>
</A>

<A NAME="papm_2002">
<BLOCKQUOTE>
<HR>
<B>Abstract (papm_2002): </B><BR>
A new denotational semantics for a variant of the
stochastic process algebra TIPP is presented,
which maps process terms to Multi-terminal binary
decision diagrams. It is shown that the new semantics
is Markovian bisimulation equivalent to the standard SOS semantics.
The paper also addresses the difficult question of
keeping the underlying state space minimal at every
construction step.
</BLOCKQUOTE>
</A>

<A NAME="aachen_inv_2001">
<BLOCKQUOTE>
<HR>
<B>Abstract (aachen_inv_2001): </B><BR>
We review high-level specification formalisms
for Markovian performability models,
thereby emphasising the role of structuring concepts as
realised par excellence by stochastic process algebras.
Symbolic representations based on decision diagrams are presented,
and it is shown that they quite ideally support
compositional model construction and analysis.
</BLOCKQUOTE>
</A>

<A NAME="aachen_etmcc_2001">
<BLOCKQUOTE>
<HR>
<B>Abstract (aachen_etmcc_2001): </B><BR>
Markov chains are widely used in the context of performance and reliability
evaluation of systems of various nature. Model checking of such chains with
respect to a given (branching) temporal logic formula has been proposed for
both the discrete and the continuous time setting. In this note, we describe
the prototype model checker ETMCC for discrete and continuous-time Markov
chains, where properties are expressed in appropriate extensions of CTL. We
illustrate the general benefits of this approach and discuss the structure
of the tool.
</BLOCKQUOTE>
</A>

<A NAME="pmccs_aCSL_2001">
<BLOCKQUOTE>
<HR>
<B>Abstract (pmccs_aCSL_2001): </B><BR>
We describe a novel model checking algorithm for analysing the
behaviour of stochastic systems with respect to their performability.
Systems are modelled as action-labelled CTMCs, and the properties to be
verified are specified with the help of the action-based temporal logic
aCSL.  The technique is currently being implemented in our freely available
prototype tool ETMCC.
</BLOCKQUOTE>
</A>

<A NAME="ifm2000">
<BLOCKQUOTE>
<HR>
<B>Abstract (ifm2000): </B><BR>
Stochastic process algebra have been proven useful because they allow
behaviour-oriented performance and reliability modelling.
As opposed to traditional performance modelling techniques,
the behaviour-oriented style supports composition and abstraction in a
natural way.
However, analysis of stochastic process algebra models is state-oriented,
because standard numerical analysis is typically based on the calculation of
This shift of paradigms hampers the acceptance of the process
algebraic approach by performance modellers.
In this paper, we develop an entirely behaviour-oriented analysis technique
for stochastic process algebra.
The key contribution is an action-based temporal logic to describe
behaviours-of-interest, together with a model checking algorithm
to derive the probability with which a stochastic process algebra
model exhibits a given behaviour-of-interest.
</BLOCKQUOTE>
</A>

<A NAME="tacas2000">
<BLOCKQUOTE>
<HR>
<B>Abstract (tacas2000): </B><BR>
Markov chains are widely used in the context of performance and
reliability evaluation of systems of various nature. Model checking
of such chains with respect to a given (branching) temporal logic
formula has been proposed for both the discrete and the continuous
time setting.  In this paper, we describe a prototype model checker
for discrete and continuous-time Markov chains, the Erlangen-Twente
Markov Chain Checker(ETMCC), where properties are expressed in
appropriate extensions of CTL.  We illustrate the general benefits
of this approach and discuss the structure of the tool. Furthermore
we report on first successful applications of the tool to non-trivial
examples, highlighting lessons learned during development and
application of ETMCC.
</BLOCKQUOTE>
</A>

<A NAME="tipptool">
<BLOCKQUOTE>
<HR>
<B>Abstract (tipptool): </B><BR>
Stochastic Process Algebras have been proposed as compositional
specification formalisms for performance models. In this paper,
we describe a tool which aims at realising all beneficial aspects
of compositional performance modelling, the TIPPtool. It incorporates
methods for compositional specification as well as solution, based
on state-of-the-art-techniques, and wrapped in a user-friendly
graphical front end. Apart from highlighting the general benefits
of the tool, we also discuss some lessons learned during development
and application of the TIPPtool. A non-trivial model of a real
life communication system serves as a case study to illustrate
benefits and limitations.
</BLOCKQUOTE>
</A>

<A NAME="cav99">
<BLOCKQUOTE>
<HR>
<B>Abstract (cav99): </B><BR>
In this short paper we briefly describe a tool which is based on
a Markovian stochastic process algebra. The tool offers both model
specification and quantitative model analysis in a compositional
fashion, wrapped in a user-friendly graphical front-end.
</BLOCKQUOTE>
</A>

<A NAME="nsmc99">
<BLOCKQUOTE>
<HR>
<B>Abstract (nsmc99): </B><BR>
Binary Decision Diagrams (BDDs) have gained high attention in the
context of design and verification of digital circuits. They have
successfully been employed to encode very large state spaces in an
efficient, \emph{symbolic} way. Multi terminal BDDs (MTBDDs) are
generalisations of BDDs from Boolean values to values of any finite
domain.  In this paper, we investigate the applicability of MTBDDs
to the symbolic representation of continuous time Markov chains,
derived from high-level formalisms, such as queueing networks or
process algebras. Based on this data structure, we discuss iterative
solution algorithms to compute the steady-state probability vector
that work in a completely symbolic way. We highlight a number
</BLOCKQUOTE>
</A>

<A NAME="mmb99_siegle">
<BLOCKQUOTE>
<HR>
<B>Abstract (mmb99_siegle): </B><BR>
Compact symbolic representations of large labelled transition
systems, based on binary decision diagrams (BDD), are discussed.
Extensions of BDDs are considered, in order to represent
{\em stochastic} transition systems for performability analysis.
We introduce Decision Node BDDs, a novel stochastic extension of BDDs
which preserves the structure and properties of purely functional BDDs.
It is shown how parallel composition of components can be performed
in this context, without leading to state space explosion.
Furthermore, we discuss state space reduction by Markovian
bisimulation, also entirely based on symbolic techniques.
Together, parallel composition and state space reduction enable a
compositional approach to the stochastic modelling of concurrent
systems.
</BLOCKQUOTE>
</A>

<A NAME="esm99">
<BLOCKQUOTE>
<HR>
<B>Abstract (esm99): </B><BR>
Stochastic Process Algebras (SPA) have been proposed as compositional
specification formalisms for quantitative models. Here we apply these
compositional features to SPAs extended by rewards. State space
reduction of performability models can be achieved based on the
behaviour-preserving notion of Markov Reward Bisimulation. For a
framework extended by immediate actions we develop a new equivalence
relation which allows further model reduction. We show that both
bisimulations are congruences concerning the composition operators
of the SPA, which enables a compositional reduction technique.
</BLOCKQUOTE>
</A>

<A NAME="arts99">
<BLOCKQUOTE>
<HR>
<B>Abstract (arts99): </B><BR>
Stochastic process algebras have been introduced
in order to enable compositional performance analysis.
The size of the state space is a limiting factor,
especially if the system consists of many cooperating components.
To fight state space explosion, various proposals for
compositional aggregation have been made. They rely on
minimisation with respect to a congruence relation. This paper
addresses the computational complexity of minimisation
algorithms and explains how efficient, BDD-based data
structures can be employed for this purpose.
</BLOCKQUOTE>
</A>

<A NAME="fbt99">
<BLOCKQUOTE>
<HR>
<B>Abstract (fbt99): </B><BR>
Stochastic process algebras have been introduced
in order to enable compositional performance analysis.
The size of the state space is a limiting factor,
especially if the system consists of many cooperating components.
To fight state space explosion, compositional aggregation
based on congruence relations can be applied.
This paper addresses the computational complexity of minimisation
algorithms and explains how efficient, BDD-based data
structures can be employed for this purpose.
</BLOCKQUOTE>
</A>

<A NAME="gmds99">
<BLOCKQUOTE>
<HR>
<B>Abstract (gmds99): </B><BR>
The management and further development of modern hospital
communication systems is a challenging task, due to the size,
complexity and heterogeneity of such systems. We use stochastic
models in order to predict the behaviour and the performance of
future configurations of hospital communication systems. To this
aim, we employ a stochastic process algebra (SPA) and our tool
TIPPtool as a methodology which supports structured model
specification and analysis.
</BLOCKQUOTE>
</A>

<A NAME="williamsburg">
<BLOCKQUOTE>
<HR>
<B>Abstract (williamsburg): </B><BR>
We discuss compact symbolic representations of large state spaces,
based on binary decision diagrams (BDD).
Extensions of BDDs are considered, in order to represent
{\em stochastic} transition systems for performability analysis.
Parallel composition of components can be performed in
this context, without leading to state space explosion.
Furthermore, we discuss state space reduction by Markovian
bisimulation, also based on symbolic techniques.
</BLOCKQUOTE>
</A>

<A NAME="durham">
<BLOCKQUOTE>
<HR>
<B>Abstract (durham): </B><BR>
We present a new approach to the compact symbolic
representation of stochastic transition systems,
based on Decision Node BDDs, a novel stochastic extension of BDDs.
Parallel composition of components can be
performed on the basis of this new data structure.
We also discuss symbolic state space reduction by Markovian
bisimulation.
</BLOCKQUOTE>
</A>

<A NAME="palma">
<BLOCKQUOTE>
<HR>
<B>Abstract (palma): </B><BR>
Stochastic Process Algebras have been proposed as compositional
specification formalisms for performance models. In this paper,
we describe a tool which aims at realising all beneficial aspects
of compositional performance modelling, the TIPPtool. It incorporates
methods for compositional specification as well as solution, based
on state-of-the-art-techniques, and wrapped in a user-friendly
graphical front end.
</BLOCKQUOTE>
</A>

<A NAME="papm98">
<BLOCKQUOTE>
<HR>
<B>Abstract (papm98): </B><BR>
Stochastic process algebras have been introduced
in order to enable compositional performance analysis.
The size of the state space is a limiting factor,
especially if the system consists of many cooperating components.
To fight state space explosion, various proposals for compositional
aggregation have been made. They rely on minimisation with respect
to a congruence relation. This paper addresses the computational
complexity of minimisation algorithms and explains how efficient,
BDD-based data structures can be employed for this purpose.
</BLOCKQUOTE>
</A>

<A NAME="dnbdd">
<BLOCKQUOTE>
<HR>
<B>Abstract (dnbdd): </B><BR>
This report presents a new approach to the compact symbolic
representation of stochastic transition systems.
We introduce Decision Node BDDs, a novel stochastic extension of
BDDs which preserves the strucure and properties of purely functional
BDDs. It is shown how parallel composition of stochastic transition
systems can be performed on the basis of this new data structure.
Furthermore, we discuss state space reduction by Markovian
bisimulation, also based on symbolic techniques.
</BLOCKQUOTE>
</A>

<A NAME="ukpew97">
<BLOCKQUOTE>
<HR>
<B>Abstract (ukpew97): </B><BR>
A BDD (Binary Decision Diagram)  is a compact canonical
representation of a Boolean function. While BDDs are well-established in
the area of functional system verification, their use for the
purpose of performance analysis is a new idea.
We use BDDs to represent labelled transition systems which
arise from higher-level model specifications such as stochastic
process algebras or structured stochastic Petri nets. BDDs offer
a compact representation of transition systems with very large state
space. They are therefore promising candidates for alleviating
the problem of state space explosion. However, as a
survey of the relevant literature shows, the question of how to
code stochastic information in a BDD context had not
We offer a new solution to this problem, concentrating on the
Markovian case. A new data structure, Decision-node BDD (DNBDD), is
introduced and used to represent stochastic transition systems. It is
shown that DNBDD have important advantages compared to earlier
approaches. A DNBDD is structurally identical with the corresponding
ordinary BDD, but some of its nodes --- which we call decision nodes ---
Generation and manipulation algorithms for DNBDDs are then discussed.
In particular, we show how a DNBDD can be constructed in a
stepwise fashion from a stochastic LTS, and how the parallel composition
of two stochastic transition systems can be performed in the DNBDD context.
DNBDD-based bisimulation minimisation (which corresponds to Markov
lumpability) is also discussed.
</BLOCKQUOTE>
</A>

<A NAME="gmds97">
<BLOCKQUOTE>
<HR>
<B>Abstract (gmds97): </B><BR>
Short description of a new approach to the performance
analysis of a hospital communication system. We use stochastic
modelling with stochastic process algebras.
</BLOCKQUOTE>
</A>

<A NAME="fmethods">
<BLOCKQUOTE>
<HR>
<B>Abstract (fmethods): </B><BR>
Parallel and distributed systems have to fulfill functional
requirements (they should function as expected) and temporal
requirements (they should meet performance requirements, e.g.
offer a certain throughput or assure real-time limits). To
meet these goals, designers need techniques and tools for
both functional and temporal description and analysis at an
early stage of the system lifecycle.  Description of complex
systems, as well as their analysis, can be extremely difficult
and costly.  In this note, after a brief survey of classical
methods, we discuss stochastic process algebras, a new
constructive approach which promises to overcome some of the
tractability problems.</BLOCKQUOTE>
</A>

<A NAME="mmb-fachgespraech">
<BLOCKQUOTE>
<HR>
<B>Kurzfassung (mmb-fachgespraech): </B><BR>
Markovmodelle spielen fuer die Leistungsbewertung paralleler
und verteilter Systeme eine grosse Rolle, da ihnen eine verhaeltnismaessig
einfache mathematische Theorie zugrunde liegt und effiziente
Analyseverfahren bekannt sind. Bei der Modellierung komplexer
nebenlaeufiger Systeme kann es aber zum Problem des unkontrollierten
Anwachsens des Zustandsraums kommen (Zustandsraumexplosion), das die
praktische Handhabung eines Modells unmoeglich macht.
In bestimmten Situationen laesst sich eine erhebliche Reduktion des
Zustandsraums  eines Markovmodells erreichen, indem man Zustaende nach
dem Prinzip der sogenannten Lumpability zusammenfasst. Wir zeigen am
Beispiel einer stochastischen Prozessalgebra, wie die Zusammenfassbarkeit
aequivalenter Zustande bereits wahrend der Erzeugung der Markovkette aus
einer prozessalgebraischen Modellbeschreibung ausgenutzt werden kann.
Diese Methode hat den Vorteil, dass als Endergebnis eine im Sinne der
Lumpability reduzierte Markovkette vorliegt, ohne dass jemals
unbeherrschbar grosse Zwischenergebnisse verarbeitet oder gespeichert
werden muessen.</BLOCKQUOTE>
</A>

<A NAME="it-plus-ti">
<BLOCKQUOTE>
<HR>
<B>Kurzfassung (it-plus-ti): </B><BR>
PEPP erlaubt die ablauforientierte Modellierung paralleler
Programme mit stochastischen Graphmodellen. Exakte und approximative
Auswerteverfahren ermoglichen Laufzeitvorhersagen fur Graphmodelle von
unterschiedlichem Typus und Komplexitat. Daruberhinaus bietet PEPP
Funktionen zur Unterstutzung der modellgesteuerten Messung und die
Moglichkeit, Modelle mit beliebigen gemessenen Verteilungsfunktionen zu
parametrieren.</BLOCKQUOTE>
<BLOCKQUOTE><B>
English Abstract (it-plus-ti): </B><BR>
Modelling and Monitoring Support with the Tool PEPP: PEPP is a tool for
modelling parallel programs using stochastic graph models. It provides
exact and approximate analysis methods for runtime prediction of
different graph model types. PEPP also supports model-driven monitoring
and allows to use arbitrary measured distributions for model
parametrization.</BLOCKQUOTE>
</A>

<A NAME="wien">
<BLOCKQUOTE>
<HR>
<B>Abstract (wien): </B><BR>
A method for analyzing parallel and distributed
systems with the help of structured Markovian models is presented. The
overall model is built from interdependent submodels, its generator matrix
being described by a tensor expression involving only small submodel
matrices. Similar submodels are grouped in submodel classes which allows the
automatic recognition and exploitation of symmetries. This is an instance of
exact Markov chain lumpability. It is shown that lumping can be carried out
advantageously at the submodel class level before the building of the tensor
descriptor. During model analysis, this leads to a significant state space
reduction. An efficient algorithm for computing the reduced generator matrix
directly from the symmetric submodels' matrices is presented. Its complexity
is analyzed and compared to that of the usual approach to computing the
lumped Markov chain, showing the superiority of the new
algorithm</BLOCKQUOTE>
</A>

<A NAME="matrixsemantik">
<BLOCKQUOTE>
<HR>
<B>Abstract (matrixsemantik): </B><BR>
The problem of deriving the Markov chain underlying a stochastic
Transition rate matrices are used as a convenient method for uniquely
describing Markov chains.
For a modified version of the stochastic process algebra TIPP, we propose
a set of new semantic rules which specify the way in which process terms
are translated into their corresponding matrices.
For each operator of the language, a semantic rule describes how the
(one ore more) operand matrices have to be combined in order to form the
matrix corresponding to the overall term.
These semantic rules guarantee certain highly advantageous
properties of the resulting matrices, the two most important of which are
(i) the absence of non-reachable states
and (ii) minimality with respect to Markov chain lumpability.
Thus avoiding redundancy, our new approach is a
contribution to the struggle against state space explosion.</BLOCKQUOTE>
</A>

<A NAME="euromicro_markov">
<BLOCKQUOTE>
<HR>
<B>Abstract (euromicro_markov): </B><BR>
The behaviour of parallel programs with
replicated processes is modelled by continuous time Markov chains. For
high-level model description, we use stochastic automata networks. We are
particularly interested in models of parallel programs which exhibit
symmetries. Exact lumpability is exploited for reducing the model's state
space, thus making complex models of large real systems computationally
tractable. Complexity analysis of a new reduction algorithm shows that the
method can be applied efficiently in practice.</BLOCKQUOTE>
</A>

<A NAME="ieee">
<BLOCKQUOTE>
<HR>
<B>Abstract (ieee): </B><BR>
The performance of parallel and distributed
systems is highly dependent on the degree of parallelism and the efficiency
of their communication systems. Both, efficiently parallelizing big jobs and
successfully designing high-speed communication systems, need insight into
the dynamic behavior of at least two computers at a time. Getting insight is
usually needed in debugging, here it is a means for improving performance.
First, we present a comprehensive methodology for monitoring and modeling
programs in parallel and distributed systems. In using event-driven
monitoring and event-oriented models there is a common abstraction, the
event, which enables us to integrate both approaches. A second part describes
implementation concepts in hardware and software which render the methodology
generally applicable and fruitful for practical performance evaluation
problems. The hardware monitor ZM4 uses many distributed monitor agents and a
global clock mechanism for achieving generality, and the evaluation
environment SIMPLE uses new trace description and access principles which
allow for accessing arbitrarily formatted traces, thus making standardized
formats in the measured event traces superfluous.</BLOCKQUOTE>
</A>

<BLOCKQUOTE>
<HR>
A method for analyzing the functional behavior
and the performance of programs in distributed systems is presented. We use
hybrid monitoring, a technique which combines advantages of both software
monitoring and hardware monitoring. The paper contains a description of a
hardware monitor and a software package (ZM4/SIMPLE) which make our concepts
available to programmers, assisting them in debugging and tuning of their
code. A short survey of related monitor systems highlights the distinguishing
features of our implementation. As an application of our monitoring and
evaluation system, the analysis of a parallel ray tracing program running on
the SUPRENUM multiprocessor is described. It is shown that monitoring and
modeling both rely on a common abstraction of a system's dynamic behavior and
therefore can be integrated to one comprehensive methodology. This
methodology is supported by a set of tools.</BLOCKQUOTE>
</A>

<A NAME="parco93_struct_mod">
<BLOCKQUOTE>
<HR>
<B>Abstract (parco_struct_mod): </B><BR>
A method for analyzing parallel systems with the
help of structured Markovian models is presented. The overall model is built
from interdependent submodels, and symmetries are exploited automatically by
grouping similar submodels in classes. During model analysis, this leads to a
state space reduction, based on the concept of exact
lumpability.</BLOCKQUOTE>
</A>

<A NAME="pars">
<BLOCKQUOTE>
<HR>
<B>Abstract (pars): </B><BR>
A new method of carrying out hybrid monitoring
for the observation of parallel programs is presented. A comprehensive set of
interacting tools, the PEPP-ZM4-SIMPLE environment, is briefly discussed.
These tools support modelling, measurement preparation, monitoring, event
trace analysis and assist in result interpretation. The emphasis of the paper
is on the flexibility of the method with respect to the level of abstraction.
It is shown that the level of granularity of observation is user-determined
and can be changed with minimal effort using our tools. An application
example, in which the dynamic behaviour of a parallel program on SUPRENUM is
analyzed, illustrates the benefits of the method.</BLOCKQUOTE>
</A>

<A NAME="pasa">
<BLOCKQUOTE>
<HR>
<B>Abstract (pasa): </B><BR>
Techniques for the efficient modelling of modern
parallel systems are discussed. Structured modelling and the use of tensor
algebra make it possible to analyze models which are otherwise not tractable.
A key point is the exploitation of model symmetries and its relation to the
SRG technique developed in the field of coloured stochastic Petri
nets.</BLOCKQUOTE>
</A>

<A NAME="isca92">
<BLOCKQUOTE>
<HR>
<B>Abstract (isca92): </B><BR>
It is often very difficult for programmers of
parallel com- puters to understand how their parallel programs behave at
execution time, because there is not enough insight into the interactions
between concurrent activities in the parallel machine. Programmers do not
only wish to obtain statistical information that can be supplied by
profiling, for example. They need to have detailed knowledge about the
functional behaviour of their programs. Considering performance aspects, they
need timing information as well. Monitoring is a technique well suited to
obtain information about both functional behaviour and timing. Global time
information is essential for determining the chronological order of events on
different nodes of a multiprocessor or of a distributed system, and for
determining the duration of time intervals between events from different
nodes. A major problem on multiprocessors is the absence of a global clock
with high resolution. This problem can be overcome if a monitor system
capable of supplying globally valid time stamps is used. In this paper, the
behaviour and performance of a parallel program on the SUPRENUM
multiprocessor is studied. The method used for gaining insight into the
runtime behaviour of a parallel program is hybrid monitoring, a technique
that combines advantages of both software monitoring and hardware monitoring.
A novel interface makes it possible to measure program activities on
SUPRENUM. The SUPRENUM system and the ZM4 hardware monitor are briefly
described. The example program under study is a parallel ray tracer. We show
that hybrid monitoring is an excellent method to provide programmers with
valuable information for debugging and tuning of parallel
programs.</BLOCKQUOTE>
</A>

<A NAME="qmips_markov">
<BLOCKQUOTE>
<HR>
<B>Abstract (qmips_markov): </B><BR>
Approaches to the state space explosion problem
in Markovian modelling of concurrent systems are discussed. The emphasis is
on structured model description techniques and model simplification. In
particular, it is shown that the exploitation of model symmetries has a
potential to drastically reduce the size of the state space. The common
features of different techniques described in the literature are pointed out.
Examples from the domain of stochastic Petri Nets are given.</BLOCKQUOTE>
</A>

<A NAME="interlock">
<BLOCKQUOTE>
<HR>
<B>Abstract (interlock): </B><BR>
A method of fault-tolerance in mesh-connected
processor arrays is presented.  This method is based
on a new type of interconnection network
called the Interlocking Bus Network.
The array can be reconfigured in the presence of
faulty processors,
using an algorithm for bipartite graph matching.
The survivability of this method and its hardware/delay
overhead are presented and compared to other schemes.
The new technique is very
general, leading to a number of important extensions.
Application of the method to the BLITZEN parallel
computer is also discussed.
</BLOCKQUOTE>
</A>

<HR>