General Distributions in Process Algebra
| Title | General Distributions in Process Algebra |
| Publication Type | Book Chapter |
| Year of Publication | 2001 |
| Authors | Katoen, J-P, D'Argenio, PR |
| Editor | Brinksma, E, Hermanns, H, Katoen, J-P |
| Book Title | Lectures on Formal Methods and Performance Analysis, First EEF/Euro Summer School on Trends in Computer Science, Berg en Dal, The Netherlands, July 3-7, 2000, Revised Lectures |
| Series Title | Lecture Notes in Computer Science |
| Volume | 2090 |
| Pagination | 375-430 |
| Publisher | Springer |
| ISBN | 3-540-42479-2 |
| Abstract | This paper is an informal tutorial on stochastic process algebras, i.e., process calculi where action occurrences may be subject to a delay that is governed by a (mostly continuous) random variable. Whereas most stochastic process algebras consider delays determined by negative exponential distributions, this tutorial is concerned with the integration of general, non-exponential distributions into a process algebraic setting. We discuss the issue of incorporating such distributions in an interleaving semantics, and present some existing solutions to this problem. In particular, we present a process algebra for the specification of stochastic discrete-event systems modeled as generalized semi-Markov chains (GSMCs). Using this language stochastic discrete-event systems can be described in an abstract and modular way. The operational semantics of this process algebra is given in terms of stochastic automata, a novel mixture of timed automata and GSMCs. We show that GSMCs are a proper subset of stochastic automata, discuss various notions of equivalence, present congruence results, treat equational reasoning, and argue how an expansion law in the process algebra can be obtained. As a case study, we specify the root contention phase within the standardized IEEE 1394 serial bus protocol and study the delay until root contention resolution. An overview of related work on general distributions in process algebra and a discussion of trends and future work complete this tutorial. |
| DOI | 10.1007/3-540-44667-2_11 |
PDF (Full text):
