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).
In addition to earlier work
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
  (transient and steady) state probabilities.  
  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
  yet been answered satisfactorily.
  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 ---
  carry additional information.
  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
  process algebra term is addressed.
  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>


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

<ADDRESS>
Markus Siegle     (markus.siegle _at_ unibw.de)
</ADDRESS>
<HR>

</BODY>
</HTML>