First passage time analysis of stochastic process algebra using partial orders

Theo C. Ruys; Rom Langerak; Joost-Pieter Katoen; Diego Latella; Mieke Massink

doi:10.1007/3-540-45319-9_16

First passage time analysis of stochastic process algebra using partial orders

Theo C. Ruys, Rom Langerak, Joost-Pieter Katoen, Diego Latella, Mieke Massink

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

7 Citations (Scopus)

80 Downloads (Pure)

Abstract

This paper proposes a partial-order semantics for a stochastic process algebra that supports general (non-memoryless) distributions and combines this with an approach to numerically analyse the first passage time of an event. Based on an adaptation of McMillan's complete finite prefix approach tailored to event structures and process algebra, finite representations are obtained for recursive processes. The behaviour between two events is now captured by a partial order that is mapped on a stochastic task graph, a structure amenable to numerical analysis. Our approach is supported by the (new) tool FOREST for generating the complete prefix and the (existing) tool PEPP for analysing the generated task graph. As a case study, the delay of the first resolution in the root contention phase of the IEEE 1394 serial bus protocol is analysed.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication	7th International Conference, TACAS 2001, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001, Genova, Italy, April 2–6, 2001. Proceedings
Editors	Tiziana Margaria, Wang Yi
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	220-235
Number of pages	16
ISBN (Electronic)	978-3-540-45319-2
ISBN (Print)	978-3-540-41865-8
DOIs	https://doi.org/10.1007/3-540-45319-9_16
Publication status	Published - 2001
Event	7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2001 - Genova, Italy Duration: 2 Apr 2001 → 6 Apr 2001 Conference number: 7

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	2031
ISSN (Print)	0302-9743

Workshop

Workshop	7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2001
Abbreviated title	TACAS
Country/Territory	Italy
City	Genova
Period	2/04/01 → 6/04/01

Keywords

FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
FMT-NIM: NON-INTERLEAVING MODELS
FMT-PM: PROBABILISTIC METHODS

Access to Document

10.1007/3-540-45319-9_16

Ruys2001firstAccepted author version, 276 KB

Cite this

Ruys, T. C., Langerak, R., Katoen, J.-P., Latella, D., & Massink, M. (2001). First passage time analysis of stochastic process algebra using partial orders. In T. Margaria, & W. Yi (Eds.), Tools and Algorithms for the Construction and Analysis of Systems: 7th International Conference, TACAS 2001, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001, Genova, Italy, April 2–6, 2001. Proceedings (pp. 220-235). (Lecture Notes in Computer Science; Vol. 2031). Springer. https://doi.org/10.1007/3-540-45319-9_16

Ruys, Theo C. ; Langerak, Rom ; Katoen, Joost-Pieter et al. / First passage time analysis of stochastic process algebra using partial orders. Tools and Algorithms for the Construction and Analysis of Systems: 7th International Conference, TACAS 2001, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001, Genova, Italy, April 2–6, 2001. Proceedings. editor / Tiziana Margaria ; Wang Yi. Berlin, Heidelberg : Springer, 2001. pp. 220-235 (Lecture Notes in Computer Science).

@inproceedings{f83f4b48a3dd4cb4827227ba9b7bacf4,

title = "First passage time analysis of stochastic process algebra using partial orders",

abstract = "This paper proposes a partial-order semantics for a stochastic process algebra that supports general (non-memoryless) distributions and combines this with an approach to numerically analyse the first passage time of an event. Based on an adaptation of McMillan's complete finite prefix approach tailored to event structures and process algebra, finite representations are obtained for recursive processes. The behaviour between two events is now captured by a partial order that is mapped on a stochastic task graph, a structure amenable to numerical analysis. Our approach is supported by the (new) tool FOREST for generating the complete prefix and the (existing) tool PEPP for analysing the generated task graph. As a case study, the delay of the first resolution in the root contention phase of the IEEE 1394 serial bus protocol is analysed.",

keywords = "FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, FMT-NIM: NON-INTERLEAVING MODELS, FMT-PM: PROBABILISTIC METHODS",

author = "Ruys, {Theo C.} and Rom Langerak and Joost-Pieter Katoen and Diego Latella and Mieke Massink",

year = "2001",

doi = "10.1007/3-540-45319-9_16",

language = "English",

isbn = "978-3-540-41865-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "220--235",

editor = "Tiziana Margaria and Wang Yi",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

address = "Germany",

note = "7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2001, TACAS ; Conference date: 02-04-2001 Through 06-04-2001",

}

Ruys, TC, Langerak, R , Katoen, J-P, Latella, D & Massink, M 2001, First passage time analysis of stochastic process algebra using partial orders. in T Margaria & W Yi (eds), Tools and Algorithms for the Construction and Analysis of Systems: 7th International Conference, TACAS 2001, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001, Genova, Italy, April 2–6, 2001. Proceedings. Lecture Notes in Computer Science, vol. 2031, Springer, Berlin, Heidelberg, pp. 220-235, 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2001, Genova, Italy, 2/04/01. https://doi.org/10.1007/3-540-45319-9_16

First passage time analysis of stochastic process algebra using partial orders. / Ruys, Theo C.; Langerak, Rom ; Katoen, Joost-Pieter et al.
Tools and Algorithms for the Construction and Analysis of Systems: 7th International Conference, TACAS 2001, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001, Genova, Italy, April 2–6, 2001. Proceedings. ed. / Tiziana Margaria; Wang Yi. Berlin, Heidelberg: Springer, 2001. p. 220-235 (Lecture Notes in Computer Science; Vol. 2031).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - First passage time analysis of stochastic process algebra using partial orders

AU - Ruys, Theo C.

AU - Langerak, Rom

AU - Katoen, Joost-Pieter

AU - Latella, Diego

AU - Massink, Mieke

N1 - Conference code: 7

PY - 2001

Y1 - 2001

N2 - This paper proposes a partial-order semantics for a stochastic process algebra that supports general (non-memoryless) distributions and combines this with an approach to numerically analyse the first passage time of an event. Based on an adaptation of McMillan's complete finite prefix approach tailored to event structures and process algebra, finite representations are obtained for recursive processes. The behaviour between two events is now captured by a partial order that is mapped on a stochastic task graph, a structure amenable to numerical analysis. Our approach is supported by the (new) tool FOREST for generating the complete prefix and the (existing) tool PEPP for analysing the generated task graph. As a case study, the delay of the first resolution in the root contention phase of the IEEE 1394 serial bus protocol is analysed.

AB - This paper proposes a partial-order semantics for a stochastic process algebra that supports general (non-memoryless) distributions and combines this with an approach to numerically analyse the first passage time of an event. Based on an adaptation of McMillan's complete finite prefix approach tailored to event structures and process algebra, finite representations are obtained for recursive processes. The behaviour between two events is now captured by a partial order that is mapped on a stochastic task graph, a structure amenable to numerical analysis. Our approach is supported by the (new) tool FOREST for generating the complete prefix and the (existing) tool PEPP for analysing the generated task graph. As a case study, the delay of the first resolution in the root contention phase of the IEEE 1394 serial bus protocol is analysed.

KW - FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - FMT-NIM: NON-INTERLEAVING MODELS

KW - FMT-PM: PROBABILISTIC METHODS

U2 - 10.1007/3-540-45319-9_16

DO - 10.1007/3-540-45319-9_16

M3 - Conference contribution

SN - 978-3-540-41865-8

T3 - Lecture Notes in Computer Science

SP - 220

EP - 235

BT - Tools and Algorithms for the Construction and Analysis of Systems

A2 - Margaria, Tiziana

A2 - Yi, Wang

PB - Springer

CY - Berlin, Heidelberg

T2 - 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2001

Y2 - 2 April 2001 through 6 April 2001

ER -

Ruys TC, Langerak R , Katoen JP, Latella D, Massink M. First passage time analysis of stochastic process algebra using partial orders. In Margaria T, Yi W, editors, Tools and Algorithms for the Construction and Analysis of Systems: 7th International Conference, TACAS 2001, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001, Genova, Italy, April 2–6, 2001. Proceedings. Berlin, Heidelberg: Springer. 2001. p. 220-235. (Lecture Notes in Computer Science). doi: 10.1007/3-540-45319-9_16

First passage time analysis of stochastic process algebra using partial orders

Abstract

Publication series

Workshop

Keywords

Access to Document

Fingerprint

Cite this