Abstract
We give a new true-concurrent model for probabilistic concurrent Kleene algebra. The model is based on probabilistic event structures, which combines ideas from Katoen’s work on probabilistic concurrency and Varacca’s probabilistic prime event structures. The event structures are compared with a true-concurrent version of Segala’s probabilistic simulation. Finally, the algebraic properties of the model are summarised to the extent that they can be used to derive techniques such as probabilistic rely/guarantee inference rules.
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
Rabin, M.O.: Probabilistic Algorithms. Technical Report RC 6164 (#26545), IBM Research Division, San Jose, Yorktown, Zurich (August 1976)
Hoare, T., Möller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra and its foundations. J. Log. Algebr. Program. 80(6), 266–296 (2011)
Hayes, I.J., Jones, C.B., Colvin, R.J.: Refining rely-guarantee thinking. Technical report, Newcastle University, United Kingdom (2012)
McIver, A.K., Rabehaja, T.M., Struth, G.: Probabilistic concurrent Kleene algebra. In: Bortolussi, L., Wiklicky, H. (eds.) QAPL. EPTCS, vol. 117, pp. 97–115 (2013)
Katoen, J.P.: Quantitative and qualitative extensions of event structures. PhD thesis, University of Twente (1996)
Langerak, R.: Bundle event structures: a non-interleaving semantics for LOTOS. Memoranda informatica. University of Twente (1992)
Rensink, A., Gorrieri, R.: Action refinement for vertical implementation. In: Wolisz, A., Schieferdecker, I., Rennoch, A. (eds.) FBT. GMD-Studien., vol. 315, pp. 69–78. GMD-Forschungszentrum Informationstechnik GmbH (1997)
Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1985. LNCS, vol. 222, pp. 325–392. Springer, Heidelberg (1986)
van Glabbeek, R.J., Vaandrager, F.W.: Bundle event structures and CCSP. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 57–71. Springer, Heidelberg (2003)
van Glabbeek, R.J., Plotkin, G.D.: Configuration structures, event structures and petri nets. Theor. Comput. Sci. 410(41), 4111–4159 (2009)
Varacca, D.: Probability, nondeterminism and concurrency: two denotational models for probabilistic computation. PhD thesis, University of Aarhus (2003)
Segala, R.: A compositional trace-based semantics for probabilistic automata. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 234–248. Springer, Heidelberg (1995)
Cherief, F.: Back and forth bisimulations on prime event structures. In: Etiemble, D., Syre, J.-C. (eds.) PARLE 1992. LNCS, vol. 605, pp. 843–858. Springer, Heidelberg (1992)
Majster-Cederbaum, M., Roggenbach, M.: Transition systems from event structures revisited. Info. Proc. Letters 67(3), 119–124 (1998)
McIver, A.K., Rabehaja, T.M., Struth, G.: An event structure model for probabilistic concurrent kleene algebra. CoRR abs/1310.2320 (2013)
Gischer, J.L.: The equational theory of pomsets. Theor. Comput. Sci. 61(23), 199–224 (1988)
Jones, C.B.: Development Methods for Computer Programs including a Notion of Interference. PhD thesis, Oxford University (June 1981)
Dingel, J.: A refinement calculus for shared-variable parallel and distributed programming. Formal Asp. Comput. 14(2), 123–197 (2002)
Fokkink, W., Zantema, H.: Basic process algebra with iteration: Completeness of its equational axioms. Comput. J. 37(4), 259–268 (1994)
Deng, Y., van Glabbeek, R.J., Hennessy, M., Morgan, C., Zhang, C.: Remarks on testing probabilistic processes. ENTCS 172, 359–397 (2007)
McIver, A.K., Weber, T.: Towards automated proof support for probabilistic distributed systems. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 534–548. Springer, Heidelberg (2005)
Parma, A., Segala, R.: Axiomatization of trace semantics for stochastic nondeterministic processes. In: Franceschinis, G., Haverkort, B.R., Katoen, J.P., Woodside, M. (eds.) QEST, pp. 294–303. IEEE Computer Society (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
McIver, A., Rabehaja, T., Struth, G. (2013). An Event Structure Model for Probabilistic Concurrent Kleene Algebra. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2013. Lecture Notes in Computer Science, vol 8312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-45221-5_43
Download citation
DOI: https://doi.org/10.1007/978-3-642-45221-5_43
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-45220-8
Online ISBN: 978-3-642-45221-5
eBook Packages: Computer ScienceComputer Science (R0)