Abstract
In this paper we show how Rate Transition Systems (RTSs) can be used as a unifying framework for the definition of the semantics of stochastic process algebras. RTSs facilitate the compositional definition of such semantics exploiting operators on the next state functions which are the functional counterpart of classical process algebra operators. We apply this framework to representative fragments of major stochastic process calculi namely TIPP, PEPA and IML and show how they solve the issue of transition multiplicity in a simple and elegant way. We, moreover, show how RTSs help describing different languages, their differences and their similarities. For each calculus, we also show the formal correspondence between the RTSs semantics and the standard SOS one.
Research partially funded by EU IP SENSORIA (contract n. 016004), CNR-RSTL project XXL, FIRB-MUR project TOCAI.IT and by PRIN-MIUR PACO.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aldini, A., Bernardo, M., Corradini, F.: A Process Algebraic Approach to Software Architecture Design. Springer, Heidelberg (to appear)
Baier, C., Hermanns, H., Katoen, J.-P., Haverkort, B.: Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theoretical Computer Science 345, 2–26 (2005)
Bernardo, M., Gorrieri, R.: A tutorial on EMPA: A theory of concurrent processes with nondeterminism, priorities, probabilities and time. Theoretical Computer Science 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: Kaklamanis, C., Nielson, F. (eds.) TGC 2008. LNCS, vol. 5474, pp. 52–68. Springer, Heidelberg (2009)
Van Hung, D., Chaochen, Z.: Probabilistic Duration Calculus for Continuous Time. Formal Aspects of Computing. The International Journal of Formal Methods 11, 21–44 (1999)
De Nicola, R., Katoen, J.-P., Latella, D., Loreti, M., Massink, M.: \(\textsc{Klaim}\) and its Stochastic Semantics. Technical Report 6, Dipartimento di Sistemi e Informatica, Università di Firenze (2006), http://rap.dsi.unifi.it/~loreti/papers/TR062006.pdf
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), http://dx.doi.org/10.1016/j.tcs2007.05.008
De Nicola, R., Latella, D., Loreti, M., Massink, M.: MarCaSPiS: a Markovian Extension of a Calculus for Services. In: Hennessy, M., Klin, B. (eds.) Proceedings of the 5th Workshop on Structural Operational Semantics (SOS 2008), Reykjavik, Iceland, July 6, pp. 6–20 (2008); Preliminary Proceedings. Final Proceedings to appear as ENTCS by Elsevier
De Nicola, R., Latella, D., Loreti, M., Massink, M.: Rate-based Transition Systems for Stochastic Process Calculi. In: Marchetti, A., Matias, Y. (eds.) Automata, Languages and Programming - C. LNCS. Springer, Heidelberg (2009)
De Nicola, R., Latella, D., Massink, M.: Formal modeling and quantitative analysis of KLAIM-based mobile systems. In: Haddad, H., Liebrock, L., Omicini, A., Wainwright, R., Palakal, M., Wilds, M., Clausen, H. (eds.) Applied Computing 2005. Proceedings of the 20th Annual ACM Symposium on Applied Computing, pp. 428–435, Association for Computing Machinery - ACM (2005), ISBN 1-58113-964-0
De Nicola, R., Latella, D., Moreli, M., Massink, M.: On a Uniform Framework for the Definition of Stochastic Process Languages. Full Version. Technical report, Consiglio Nazionale delle Ricerche, Istituto di Scienza e Tecnologie dell’Informazione ’A. Faedo’ (to appear, 2009)
Deng, Y., van Glabbeek, R., Hennessy, M., Morgan, C., Zhang, C.: Characterising testing preorders for finite probabilistic processes. In: IEEE Symposium on Logic in Computer Science, pp. 313–325. IEEE Computer Society Press, Los Alamitos (2007)
Gotz, 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.) SIGMETRICS 1993 and Performance 1993. LNCS, vol. 729. Springer, Heidelberg (1993)
Haverkort, B.: 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. LNCS, vol. 2428, p. 129. Springer, Berlin (2002)
Hermanns, H., Herzog, U., Katoen, J.-P.: Process algebra for performance evaluation. Theoretical Computer Science 274(1-2), 43–87 (2002)
Hermanns, H., Herzog, U., Mertsiotakis, V.: Stochastic process algebras - between LOTOS and Markov chains. Computer Networks and ISDN Systems 30, 901–924 (1998)
Hermanns, H., Johr, S.: Uniformity by Construction in the Analysis of Nondeterministic Stochastic Systems. In: 2007 International Conference on Dependable Systems & Networks, pp. 718–728. IEEE Computer Society Press, Los Alamitos (2007)
Hillston, J.: A compositional approach to performance modelling. In: Distinguished Dissertation in Computer Science. Cambridge University Press, Cambridge (1996)
Klin, B., Sassone, V.: Structural Operational Semantics for Stochastic Process Calculi. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 428–442. Springer, Heidelberg (2008)
Knast, R.: Continuous-Time Probabilistic Automata. Information and Control 15, 335–352 (1969)
Zhang, L., Hermanns, H., Eisenbrand, F., Jansen, D.: Flow Faster: Efficient Decision Algorithms For Probabilistic Simulations. Logical Methods in Computer Science 4(6), 1–43 (2008)
Prandi, D., Quaglia, P.: Stochastic COWS. In: Krämer, B.J., Lin, K.-J., Narasimhan, P. (eds.) ICSOC 2007. LNCS, vol. 4749, pp. 245–256. Springer, Heidelberg (2007)
Priami, C.: Stochastic π-Calculus. The Computer Journal 38(7), 578–589 (1995)
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). On a Uniform Framework for the Definition of Stochastic Process Languages. In: Alpuente, M., Cook, B., Joubert, C. (eds) Formal Methods for Industrial Critical Systems. FMICS 2009. Lecture Notes in Computer Science, vol 5825. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04570-7_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-04570-7_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04569-1
Online ISBN: 978-3-642-04570-7
eBook Packages: Computer ScienceComputer Science (R0)