Composing Systems While Preserving Probabilities
Restricting the power of the schedulers that resolve the nondeterminism in probabilistic concurrent systems has recently drawn the attention of the research community. The goal is to preserve the probabilistic behaviour of systems when composed, and at the same time, to guarantee compositionality for trace-like equivalences. In our previous work, we have defined a model of probabilistic systems with labels on the internal transitions, that restrict the power of the schedulers. A trace-style equivalence for the same model, compatible with a synchronous parallel composition, was proposed. In the present paper we generalize the parallel composition to allow for action interleaving and synchronization on a given set of actions, combined with hiding afterwards. We propose a method for automatic labeling of the internal transitions that arise due to the parallel composition. These labels reflect the information that the components use in order to resolve the nondeterminism in the composition, and thus restrict the power of the schedulers. We show that our equivalence is compositional w.r.t. the parallel composition. We also define operational semantics that, besides the parallel composition, includes deadlock, and four types of choices – action, external, internal, and probabilistic.
KeywordsOperational Semantic Internal Transition Probabilistic Choice Parallel Composition Process Algebra
Unable to display preview. Download preview PDF.
- 8.Georgievska, S., Andova, S.: Process theory for probabilistic ready-trace equivalence. Technical Report (2010), http://www.win.tue.nl/~sgeorgie/axioms2010.pdf
- 9.Giro, S., D’Argenio, P.: On the expressive power of schedulers in distributed probabilistic systems. In: Proc. QAPL 2009. ENTCS, vol. 253(3), pp. 45–71 (2009)Google Scholar
- 11.Hansson, H.A.: Time and Probability in Formal Design of Distributed Systems. Elsevier, Amsterdam (1994)Google Scholar
- 13.Kwiatkowska, M.Z., Norman, G.J.: A fully abstract metric-space denotational semantics for reactive probabilistic processes. In: Proc. COMPROX 1998. ENTCS, vol. 13 (1998)Google Scholar
- 15.Lowe, G.: Representing nondeterministic and probabilistic behaviour in reactive processes. Technical Report PRG-TR-11-93. Oxford Univ. Comp. Labs (1993)Google Scholar
- 19.Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)Google Scholar
- 20.Segala, R.: Modeling and verification of randomized distributed real-time systems. PhD thesis, MIT (1995)Google Scholar