Abstract
A variant of Rate Transition Systems (RTS), proposed by Klin and Sassone, is introduced and used as the basic model for defining stochastic behaviour of processes. The transition relation used in our variant associates to each process, for each action, the set of possible futures paired with a measure indicating their rates. We show how RTS can be used for providing the operational semantics of stochastic extensions of classical formalisms, namely CSP and CCS. We also show that our semantics for stochastic CCS guarantees associativity of parallel composition. Similarly, in contrast with the original definition by Priami, we argue that a semantics for stochastic π-calculus can be provided that guarantees associativity of parallel composition.
Research partially funded by EU IP SENSORIA (contract n. 016004), EU project RESIST/FAERUS (IST-2006-026764), the CNR-RSTL project XXL, the Italian national projects FIRB-MUR TOCAI.IT and PRIN PACO.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-Checking Algorithms for Continuous-Time Markov Chains. IEEE Transactions on Software Engineering 29(6), 524–541 (2003)
Bernardo, M., Gorrieri, R.: A tutorial on EMPA: A theory of concurrent processes with nondeterminism, priorities, probabilities and time. Theoret. Comput. Sci. 202(1-2), 1–54 (1998)
Bravetti, M., Latella, D., Loreti, M., Massink, M., Zavattaro, G.: Combining timed coordination primitives and probabilistic tuple spaces. In: TGC 2008. LNCS, vol. 5474, pp. 52–68. Springer, Heidelberg (2009)
Brinksma, E., Hermanns, H.: Process Algebra and Markov Chains. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) EEF School 2000 and FMPA 2000. LNCS, vol. 2090, pp. 183–231. Springer, Heidelberg (2001)
De Nicola, R., Katoen, J.-P., Latella, D., Loreti, M., Massink, M.: Model checking mobile stochastic logic. Theoretical Computer Science 382(1), 42–70 (2007)
De Nicola, R., Latella, D., Loreti, M., Massink, M.: Rate-based Transition Systems for Stochastic Process Calculi, http://www.dsi.unifi.it/~loreti/
Deng, Y., van Glabbeek, R., Hennessy, M., Morgan, C., Zhang, C.: Characterising testing preorders for finite probabilistic processes. In: Proceedings of LICS 2007, pp. 313–325. IEEE Computer Society, Los Alamitos (2007)
Glotz, N., Herzog, U., Rettelbach, M.: Multiprocessor and distributed systems design: The integration of functional specification and performance analysis using stochastic process algebras. In: Donatiello, L., Nelson, R. (eds.) PECCS 1993. LNCS, vol. 729. Springer, Heidelberg (1993)
Haverkort, B.R.: Markovian Models for Performance and Dependability Evaluation. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) EEF School 2000 and FMPA 2000. LNCS, vol. 2090, pp. 38–83. Springer, Heidelberg (2001)
Hermanns, H.: Interactive Markov Chains. In: Hermanns, H. (ed.) Interactive Markov Chains. LNCS, vol. 2428, pp. 57–88. Springer, Heidelberg (2002)
Hermanns, H., Herzog, U., Katoen, J.-P.: Process algebra for performance evaluation. Theoret. Comput. Sci. 274(1-2), 43–87 (2002)
Hermanns, H., Johr, S.: Uniformity by Construction in the Analysis of Nondeterministic Stochastic Systems. In: DSN 2007, pp. 718–728. IEEE Computer Society Press, Los Alamitos (2007)
Hermanns, H., Siegle, M.: Bisimulation algorithms for stochastic process algebras and their BDD-based implementation. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 244–264. Springer, Heidelberg (1999)
Hillston, J.: A compositional approach to performance modelling. Distinguished Dissertation in Computer Science, Cambridge University Press, Cambridge (1996)
Hillston, J.: Process algebras for quantitative analysis. In: IEEE Symposium on Logic in Computer Science, pp. 239–248. IEEE Computer Society Press, Los Alamitos (2005)
Hoare, C.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Kemeny, J., Snell, J.: Finite Markov Chains. Springer, Heidelberg (1976)
Klin, B., Sassone, V.: Structural operational semantics for stochastic process calculi. In: Lipp, P., Sadeghi, A.-R., Koch, K.-M. (eds.) Trust 2008. LNCS, vol. 4968. Springer, Heidelberg (2008)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Milner, R., Parrow, J., Walker, J.: A Calculus of Mobile Processes, I and II. Information and Computation 100(1), 1–77 (1992)
Nicola, R.D., Latella, D., Loreti, M., Massink, M.: MarCaSPiS: a markovian extension of a calculus for services. In: Proc. of SOS 2008. ENTCS, Elsevier, Amsterdam (2008)
Priami, C.: Stochastic π-Calculus. The Computer Journal 38(7), 578–589 (1995)
Puterman, M.: Markov Decision Processes (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
De Nicola, R., Latella, D., Loreti, M., Massink, M. (2009). Rate-Based Transition Systems for Stochastic Process Calculi. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds) Automata, Languages and Programming. ICALP 2009. Lecture Notes in Computer Science, vol 5556. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02930-1_36
Download citation
DOI: https://doi.org/10.1007/978-3-642-02930-1_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02929-5
Online ISBN: 978-3-642-02930-1
eBook Packages: Computer ScienceComputer Science (R0)