Probabilistic Thread Algebra – Facultatea de Informatică

Published in Volume XXV, Issue 2, 2015, pages 211-243, doi: 10.7561/SACS.2015.2.211

Authors: J.A. Bergstra, C.A. Middelburg

Abstract

We add probabilistic features to basic thread algebra and its extensions with thread-service interaction and strategic interleaving. Here, threads represent the behaviours produced by instruction sequences under execution and services represent the behaviours exhibited by the components of execution environments of instruction sequences. In a paper concerned with probabilistic instruction sequences, we proposed several kinds of probabilistic instructions and gave an informal explanation for each of them. The probabilistic features added to the extension of basic thread algebra with thread-service interaction make it possible to give a formal explanation in terms of non-probabilistic instructions and probabilistic services. The probabilistic features added to the extensions of basic thread algebra with strategic interleaving make it possible to cover strategies corresponding to probabilistic scheduling algorithms.

Full Text (PDF)

References

[1] S. Andova and S. Georgievska. On compositionality, efficiency, and applicability of abstraction in probabilistic systems. In M. Nielsen et al., editors, SOFSEM 2009, volume 5404 of Lecture Notes in Computer Science, pages 67–78. Springer-Verlag, 2009. doi:10.1007/ 978-3-540-95891-8_10.

[2] J. C. M. Baeten, J. A. Bergstra, and S. A. Smolka. Axiomatizing probabilistic processes: ACP with generative probabilities. Information and Computation, 121(2):234–255, 1995. doi:10.1006/inco.1995.1135.

[3] J. C. M. Baeten and W. P. Weijland. Process Algebra, volume 18 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 1990.

[4] J. A. Bergstra, I. Bethke, and A. Ponse. Cancellation meadows: A generic basis theorem and some applications. Computer Journal, 56(1):3– 14, 2013. doi:10.1093/comjnl/bxs028.

[5] J. A. Bergstra, Y. Hirshfeld, and J. V. Tucker. Meadows and the equational specification of division. Theoretical Computer Science, 410(12–13):1261–1271, 2009. doi:10.1016/j.tcs.2008.12.015.

[6] J. A. Bergstra and M. E. Loots. Program algebra for sequential code. Journal of Logic and Algebraic Programming, 51(2):125–156, 2002. doi: 10.1016/S1567-8326(02)00018-8.

[7] J. A. Bergstra and C. A. Middelburg. Thread algebra with multi-level strategies. Fundamenta Informaticae, 71(2–3):153–182, 2006.

[8] J. A. Bergstra and C. A. Middelburg. Thread algebra for strategic interleaving. Formal Aspects of Computing, 19(4):445–474, 2007. doi: 10.1007/s00165-007-0024-9.

[9] J. A. Bergstra and C. A. Middelburg. A thread algebra with multi-level strategic interleaving. Theory of Computing Systems, 41(1):3–32, 2007. doi:10.1007/s00224-006-1337-4.

[10] J. A. Bergstra and C. A. Middelburg. Distributed strategic interleaving with load balancing. Future Generation Computer Systems, 24(6):530– 548, 2008. doi:10.1016/j.future.2007.08.001.

[11] J. A. Bergstra and C. A. Middelburg. Program algebra with a jump- shift instruction. Journal of Applied Logic, 6(4):553–563, 2008. doi: 10.1016/j.jal.2008.07.001.

[12] J. A. Bergstra and C. A. Middelburg. Instruction sequence notations with probabilistic instructions. arXiv:0906.3083v1 [cs.PL], June 2009.

[13] J. A. Bergstra and C. A. Middelburg. A thread calculus with molecular dynamics. Information and Computation, 208(7):817–844, 2010. doi: 10.1016/j.ic.2010.01.004.

[14] J. A. Bergstra and C. A. Middelburg. Instruction sequence processing operators. Acta Informatica, 49(3):139–172, 2012. doi:10.1007/ s00236-012-0154-2.

[15] J. A. Bergstra and C. A. Middelburg. Instruction Sequences for Computer Science, volume 2 of Atlantis Studies in Computing. Atlantis Press, Amsterdam, 2012. doi:10.2991/978-94-91216-65-7.

[16] J. A. Bergstra and A. Ponse. Combining programs and state machines. Journal of Logic and Algebraic Programming, 51(2):175–192, 2002. doi: 10.1016/S1567-8326(02)00020-6.

[17] J. A. Bergstra and A. Ponse. Signed meadow valued probability mass functions. arXiv:1307.5173v1
[math.LO], July 2013.

[18] J. A. Bergstra and J. V. Tucker. The rational numbers as an abstract data type. Journal of the ACM, 54(2):Article 7, 2007. doi:10.1145/ 1219092.1219095.

[19] S. J. Gay. Quantum programming languages: Survey and bibliography. Mathematical Structures in Computer Science, 16(4):581–600, 2006. doi:10.1017/S0960129506005378.

[20] J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java Language Specification. Addison-Wesley, Reading, MA, second edition, 2000.

[21] He Jifeng, K. Seidel, and A. K. McIver. Probabilistic models for the guarded command language. Science of Computer Programming, 28(2– 3):171–192, 1997. doi:10.1016/S0167-6423(96)00019-6.

[22] A. Hejlsberg, S. Wiltamuth, and P. Golde. C# Language Specification. Addison-Wesley, Reading, MA, 2003.

[23] C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs, 1985.

[24] W. A. Hodges. Model Theory, volume 42 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, Cambridge, 1993.

[25] A. Itai and M. Rodeh. Symmetry breaking in distributed networks. Information and Computation, 88(1):60–87, 1990. doi:10.1016/0890-5401(90)90004-2.

[26] R. Milner. Communication and Concurrency. Prentice-Hall, Englewood Cliffs, 1989.

[27] M. O. Rabin. Probabilistic algorithms. In J. F. Traub, editor, Algorithms and Complexity: New Directions and Recent Results, pages 21–39. Academic Press, New York, 1976.

[28] M. O. Rabin. Probabilistic algorithm for testing primality. Journal of Number Theory, 12(1):128–138, 1980. doi:10.1016/0022-314X(80) 90084-0.

[29] A. Sabelfeld and D. Sands. Probabilistic noninterference for multithreaded programs. In Computer Security Foundations Workshop 2000, pages 200–214. IEEE Computer Society Press, 2000. doi:10.1109/ CSFW.2000.856937.

[30] D. Sannella and A. Tarlecki. Algebraic preliminaries. In E. Astesiano, H.-J. Kreowski, and B. Krieg-Brückner, editors, Algebraic Foundations of Systems Specification, pages 13–30. Springer-Verlag, Berlin, 1999. doi:10.1007/978-3-642-59851-7_2.

[31] P. W. Shor. Algorithms for quantum computation: Discrete logarithms and factoring. In FOCS ’94, pages 124–134. IEEE Computer Society Press, 1994. doi:10.1109/SFCS.1994.365700.

[32] R. J. van Glabbeek, S. A. Smolka, and B. Steffen. Reactive, generative and stratified models of probabilistic processes. Information and Computation, 121(1):59–80, 1995. doi:10.1006/inco.1995.1123.

[33] C. A. Waldspurger and W. E. Weihl. Lottery scheduling: Flexible proportional-share resource management. In OSDI ’94, pages 1–12. USENIX Association, 1994.

[34] M. Wirsing. Algebraic specification. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 675–788. Elsevier, Amsterdam, 1990.

Bibtex

@article{sacscuza:bergstra2015pta,
  title={Probabilistic Thread Algebra},
  author={J.A. Bergstra and C.A. Middelburg},
  journal={Scientific Annals of Computer Science},
  volume={25},
  number={2},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  year={2015},
  pages={211--243},
  doi={10.7561/SACS.2015.2.211},
  publisher={``A.I. Cuza'' University Press}
}