We introduce a probabilistic extension of KLAIM, where the behaviour of networks and individual nodes is determined by a probabilistic scheduler for processes and probabilistic allocation environments which describe the logical neighbourhood of each node. The resulting language has two variants which are modelled respectively as discrete and continuous time Markov processes. We suggest that Poisson processes are a natural probabilistic model for the coordination of discrete processes asynchronously communicating in continuous time and we use them to define the operational semantics of the continuous time variant. This framework allows for the implementation of networks with independent clocks on each site.
KeywordsContinuous Time Operational Semantic Global Transition Continuous Time Model Discrete Time Markov Chain
Unable to display preview. Download preview PDF.
- 3.Bause, F., Kritzinger, P.S.: Stochastic Petri Nets – An Introduction to the Theory, 2nd edn. Vieweg Verlag (2002)Google Scholar
- 5.Di Pierro, A., Hankin, C., Wiklicky, H.: Analysing the propagation of computer viruses. Journal of Functional Programming (2003) (submitted)Google Scholar
- 6.Giacalone, A., Jou, C.C., Smolka, S.: Algebraic reasoning for probabilistic concurrent systems. In: Proceedings of the IFIP WG 2.2/2.3 Working Conference on Programming Concepts and Methods, pp. 443–458. North-Holland, Amsterdam (1990)Google Scholar
- 7.Jonsson, B., Yi, W., Larsen, K.: 11. In: Probabilistic Extentions of Process Algebras, pp. 685–710. Elsevier Science, Amsterdam (2001); see Google Scholar
- 9.Hillston, J.: PEPA: Performance enhanced process algebra. Technical Report CSR-24-93, University of Edinburgh, Edinburgh, Scotland (1993)Google Scholar
- 12.Bernardo, M., Gorrieri, R.: A tutorial on EMPA: A theory of concurrent processes with nondeterminism, priorities, probabilities and time. Technical Report UBLCS-96-17, Department of Computer Science, University of Bologna (1997)Google Scholar
- 14.de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, Department of Computer Science (1998)Google Scholar
- 16.Aldini, A., Bravetti, M., Gorrieri, R.: A process algebraic approach for the analysis of probabilistic non-interference. Journal of Computer Security (2004)Google Scholar