# 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>