Bisimulation Algorithms for StochasticProcess Algebras and their BDD-based Implementation

Joost P. Katoen; H. Hermanns; M. Siegle

Bisimulation Algorithms for StochasticProcess Algebras and their BDD-based Implementation

Joost P. Katoen (Editor), H. Hermanns, M. Siegle

Research output: Contribution to conference › Paper › peer-review

11 Downloads (Pure)

Abstract

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.

Original language	Undefined
Pages	144-264
Number of pages	121
Publication status	Published - 1999
Event	Formal Methods for Real-Time and Probabilistic Systems: 5th International AMAST Workshop, ARTS'99 - Bamberg, Germany Duration: 1 May 1999 → 1 May 1999

Workshop

Workshop	Formal Methods for Real-Time and Probabilistic Systems: 5th International AMAST Workshop, ARTS'99
Period	1/05/99 → 1/05/99
Other	May 1999

Keywords

FMT-PA: PROCESS ALGEBRAS
FMT-PM: PROBABILISTIC METHODS
IR-63312
FMT-BDD: BINARY DECISION DIAGRAMS
FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
EWI-6504

Access to Document

Cite this

@conference{a236886ec3af466e9e1f403a7858df22,

title = "Bisimulation Algorithms for StochasticProcess Algebras and their BDD-based Implementation",

abstract = "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.",

keywords = "FMT-PA: PROCESS ALGEBRAS, FMT-PM: PROBABILISTIC METHODS, IR-63312, FMT-BDD: BINARY DECISION DIAGRAMS, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, EWI-6504",

author = "Katoen, {Joost P.} and H. Hermanns and M. Siegle",

year = "1999",

language = "Undefined",

pages = "144--264",

note = "Formal Methods for Real-Time and Probabilistic Systems: 5th International AMAST Workshop, ARTS'99 ; Conference date: 01-05-1999 Through 01-05-1999",

}

TY - CONF

T1 - Bisimulation Algorithms for StochasticProcess Algebras and their BDD-based Implementation

AU - Hermanns, H.

AU - Siegle, M.

A2 - Katoen, Joost P.

PY - 1999

Y1 - 1999

N2 - 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.

AB - 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.

KW - FMT-PA: PROCESS ALGEBRAS

KW - FMT-PM: PROBABILISTIC METHODS

KW - IR-63312

KW - FMT-BDD: BINARY DECISION DIAGRAMS

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - EWI-6504

M3 - Paper

SP - 144

EP - 264

T2 - Formal Methods for Real-Time and Probabilistic Systems: 5th International AMAST Workshop, ARTS'99

Y2 - 1 May 1999 through 1 May 1999

ER -