Abstract
We introduce the Stochastic Quality Calculus in order to model and reason about distributed processes that rely on each other in order to achieve their overall behaviour. The calculus supports broadcast communication in a truly concurrent setting. Generally distributed delays are associated with the outputs and at the same time the inputs impose constraints on the waiting times. Consequently, the expected inputs may not be available when needed and therefore the calculus allows to express the absence of data.
The communication delays are expressed by general distributions and the resulting semantics is given in terms of Generalised Semi-Markov Decision Processes. By restricting the distributions to be continuous and by allowing truly concurrent communication we eliminate the non-determinism and arrive at Generalised Semi-Markov Processes (GSMPs); further restriction to exponential distributions gives rise to numerically analysable GSMPs, in particular using techniques from stochastic model checking.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
CONNECT, U.A.D.: Report from the European Union workshop on Directions in Systems of Systems Engineering as part of Horizon 2012 (July 2012)
Nielson, H.R., Nielson, F., Vigo, R.: A calculus for quality. In: Păsăreanu, C.S., Salaün, G. (eds.) FACS 2012. LNCS, vol. 7684, pp. 188–204. Springer, Heidelberg (2013)
Milner, R.: Communicating and Mobile Systems: the Pi-Calculus. Cambridge University Press (1999)
Nielson, H.R., Nielson, F.: Probabilistic analysis of the quality calculus. In: Beyer, D., Boreale, M. (eds.) FORTE 2013 and FMOODS 2013. LNCS, vol. 7892, pp. 258–272. Springer, Heidelberg (2013)
Vigo, R., Nielson, F., Nielson, H.R.: Broadcast, denial-of-service, and secure communication. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 412–427. Springer, Heidelberg (2013)
Hillston, J.: A compositional approach to performance modelling. Cambridge University Press, New York (1996)
Brinksma, E., Hermanns, H.: Process Algebra and Markov Chains. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) FMPA 2000. LNCS, vol. 2090, pp. 183–231. Springer, Heidelberg (2001)
Priami, C.: Stochastic π-calculus. The Computer Journal 38(7), 578–589 (1995)
De Nicola, R., Katoen, J.P., Latella, D., Massink, M.: Stoklaim: A stochastic extension of klaim. CNR-ISTI Technical Report number ISTI-2006-TR-01 (2006)
Yi, W.: CCS + time= an interleaving model for real time systems. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, pp. 217–228. Springer, Heidelberg (1991)
Ciobanu, G., Koutny, M.: PerTiMo: A Model of Spatial Migration with Safe Access Permissions. Newcastle University, Computing Science (2011)
Bravetti, M., Bernardo, M., Gorrieri, R.: Towards performance evaluation with general distributions in process algebras. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 405–422. Springer, Heidelberg (1998)
Nielsen, B.F., Nielson, F., Riis Nielson, H.: Model checking multivariate state rewards. In: QEST 2010, Seventh International Conference on the Quantitative Evaluation of Systems, pp. 7–16. IEEE Computer Society (2010)
Markovski, J.: Real and stochastic time in process algebras for performance evaluation. PhD thesis, Ph. D. Thesis, Eindhoven University of Technology (2008)
Doshi, B.T.: Generalized semi-markov decision processes. Journal of Applied Probability, 618–630 (1979)
Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming, 1st edn. John Wiley & Sons, Inc., New York (1994)
Younes, H.L., Simmons, R.G.: Solving generalized semi-markov decision processes using continuous phase-type distributions. In: Proceedings of the National Conference on Artificial Intelligence, pp. 742–748 (2004)
Matthes, K.: Zur theorie der bedienungsprozesse. In: Trans. of the 3rd Prague Conf. on Information Theory, Stat. Dec. Fns. and Random Processes, pp. 513–528 (1962)
Glynn, P.W.: A GSMP formalism for discrete event systems. Proceedings of the IEEE 77(1), 14–23 (1989)
Younes, H.L.: Ymer: A statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 429–433. Springer, Heidelberg (2005)
Younes, H., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. International Journal on Software Tools for Technology Transfer (STTT) 8(3), 216–228 (2006)
Lindemann, C., Thümmler, A.: Numerical Analysis of Generalized Semi-Markov Processes. Dekanat Informatik, Univ. (1999)
Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996)
Milner, R.: A proposal for standard ML. In: Proceedings of the 1984 ACM Symposium on LISP and functional Programming, pp. 184–197. ACM (1984)
Nielson, F., Nielson, H.R., Zeng, K.: Stochastic Model Checking for the Stochastic Quality Calculus (2014) (submitted for Publication)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 IFIP International Federation for Information Processing
About this paper
Cite this paper
Zeng, K., Nielson, F., Nielson, H.R. (2014). The Stochastic Quality Calculus. In: Kühn, E., Pugliese, R. (eds) Coordination Models and Languages. COORDINATION 2014. Lecture Notes in Computer Science(), vol 8459. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-43376-8_12
Download citation
DOI: https://doi.org/10.1007/978-3-662-43376-8_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-43375-1
Online ISBN: 978-3-662-43376-8
eBook Packages: Computer ScienceComputer Science (R0)