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
Chapter PDF
Similar content being viewed by others
References
M. Bernardo and R. Gorrieri. A Tutorial on EMPA: A Theory of Concurrent Processes with Nondeterminism, Priorities, Probabilities and Time. Theoretical Computer Science, 202:1–54, 1998.
T. Bolognesi and E. Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems, 14:25–59, 1987.
M. Bravetti and R. Gorrieri. Interactive Generalized Semi-Markov Processes. In J. Hillston and M. Silva, editors, Proc.of PAPM’99, pages 83–98, Zaragoza, Spain, September 1999.
E. Brinksma, J.-P. Katoen, R. Langerak, and D. Latella. A Stochastic Causality-Based Process Algebra. The Computer Journal, 38(7):552–565, 1995.
P. R. D’Argenio. Algebras and Automata for Timed and Stochastic Systems. PhD thesis, University of Twente, Enschede, The Netherlands, November 1999.
P. R. D’Argenio, J.-P. Katoen, and E. Brinksma. An Algebraic Approach to the Specification of Stochastic Systems (extended abstract). In D. Gries and W.-P. de Roever, editors, Proc.of PROCOMET’98, pages 126–148, Shelter Island, New York, USA, 1998. Chapman & Hall.
P. Dauphin, F. Hartleb, M. Kienow, V. Mertsiotakis, and A. Quick. PEPP: Performance Evaluation of Parallel Programs-User’s Guide-Version 3.3. Technical Report 17/93, IMMD VII, University of Erlangen-Nürnberg, Germany, 1993.
P. Dauphin, R. Hofmann, R. Klar, B. Mohr, A. Quick, M. Siegle, and F. Sötz. ZM4/SIMPLE: a General Approach to Performance-Measurement and Evaluation of Distributed Systems. In T. L. Casavant and M. Singhal, editors, Advances in Distributed Computing: Concepts and Design. IEEE Computer Society Press, 1992.
J. Engelfriet. Branching Processes of Petri Nets. Acta Informatica, 28(6):575–591, 1991.
J. Esparza. Model Checking Using Net Unfoldings. Science of Computer Programming, 23(2):151–195, 1994.
J. Esparza, S. Römer, and W. Vogler. An Improvement of McMillan’s Unfolding Algorithm. In T. Margaria and B. Steffen, editors, Proc.of TACAS’96, LNCS 1055, pages 87–106, Passau, Germany, March 1996. Springer-Verlag.
E. R. Gansner, E. Koutsofios, and S. C. N. an Kiem-Phong Vo. A Technique for Drawing Directed Graphs. IEEE Transactions on Software Engineering, 19(3):214–230, 1993.
N. Götz, U. Herzog, and M. Rettelbach. Multiprocessor and Distributed System Design: The Integration of Functional Specification and Performance Analysis Using Stochastic Process Algebras. In L. Donatiello and R. Nelson, editors, Proc. of PERFORMANCE’93, LNCS 729, pages 121–146, Rome, Italy, September 1993. Springer-Verlag.
P. G. Harrison and B. Strulo. Stochastic Process Algebra for Discrete Event Simulation. In F. Bacelli, A. Jean-Marie, and I. Mitrani, editors, Quantitative Methods in Parallel Systems, Esprit Basic Research Series, pages 18–37. Springer-Verlag, 1995. Chapter 2.
F. Hartleb. Stochastic Graph Models for Performance Evaluation of Parallel Programs and the Evaluation Tool PEPP. In N. Götz, U. Herzog, and M. Rettelbach, editors, Proc.of the QMIPS Workshop on Formalisms, Principles and State-ofthe-art, pages 207–224, Erlangen/Pommersfelden, Germany, March 1993. Arbeitsbericht Band 26, Number 14.
H. Hermanns. Interactive Markov Chains. PhD thesis, University of Erlangen, Nürnberg, Germany, 1998.
H. Hermanns and J.-P. Katoen. Automated Compositional Markov Chain Generation for a Plain-Old Telephone System. Science of Computer Programming, 36(1):97–127, 2000.
U. Herzog. A Concept for Graph-Based Stochastic Process Algebras, Generally Distributed Activity Times, and Hierarchical Modelling. In M. Ribaudo, editor, Proc.of PAPM’96, pages 1–20. C.L.U.T. Press, 1996.
J. Hillston. A Compositional Approach to Performance Modelling. Distinguished Dissertations Series. Cambridge University Press, 1996.
IEEE Computer Society. IEEE Standard for a High Performance Serial Bus, Std 1394-1995 edition, 1996.
R. Klar, P. Dauphin, F. Hartleb, R. Hofmann, B. Mohr, A. Quick, and M. Siegle. Messung and Modellierung Paralleler und Verteilter Rechensysteme (in german). Teubner-Verlag, Stuttgart, 1995.
R. Langerak. Transformations and Semantics for LOTOS. PhD thesis, University of Twente, Enschede, The Netherlands, November 1992.
R. Langerak. Deriving a Graph Grammar from a Complete Finite Prefix of an Unfolding. In I. Castellani and B. Victor, editors, Proc.of EXPRESS’99, ENTCS 27, Eindhoven, The Netherlands, August 1999. Elsevier Science Publishers.
R. Langerak and E. Brinksma. A Complete Finite Prefix for Process Algebra. In N. Halbwachs and D. Peled, editors, Proc.of CAV’99, LNCS 1633, pages 184–195, Trento, Italy, July 1999. Springer-Verlag.
K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.
K. L. McMillan. A Technique of State Space Search Based on Unfolding. Formal Methods in System Design, 6(1):45–65, 1995.
V. Mertsiotakis. Extension of the Graph Analysis Tool SPASS and Integration into the X-Window Environment of PEPP (in german). Technical report, Department of Computer Science VII, IMMD VII, University of Erlangen-Nürnberg, Germany, 1991. Internal study.
M. Nielsen, G. D. Plotkin, and G. Winskel. Petri Nets, Event Structures and Domains, Part 1. Theoretical Computer Science, 13(1):85–108, 1981.
E.-R. Olderog. Nets, Terms and Formulas, volume 23 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1991.
A. Rensink. Models and Methods for Action Refinement. PhD thesis, University of Twente, Enschede, The Netherlands, August 1993.
T. C. Ruys. Towards Effective Model Checking. PhD thesis, University of Twente, Enschede, The Netherlands, March 2001. To be published.
G. Sander. Graph Layout through the VCG Tool. In R. Tamassia and I. G. Tollis, editors, Proc.of the Int. Workshop on Graph Drawing (GD’94), LNCS 894, pages 194–205, Princeton, New Jersey, USA, 1994. Springer-Verlag.
M. I. Stoelinga and F. W. Vaandrager. Root Contention in IEEE 1994. In J.-P. Katoen, editor, Proc.of ARTS’99, LNCS 1601, pages 53–74, Bamberg, Germany, May 1999. Springer-Verlag.
F. Wallner. Model-Checking LTL using Net Unfoldings. In A. J. Hu and M. Y. Vardi, editors, Proc.of CAV’98, LNCS 1427, pages 207–218, Vancouver, Canada, July 1998. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ruys, T.C., Langerak, R., Katoen, JP., Latella, D., Massink, M. (2001). First Passage Time Analysis of Stochastic Process Algebra Using Partial Orders. In: Margaria, T., Yi, W. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2001. Lecture Notes in Computer Science, vol 2031. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45319-9_16
Download citation
DOI: https://doi.org/10.1007/3-540-45319-9_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41865-8
Online ISBN: 978-3-540-45319-2
eBook Packages: Springer Book Archive