Axioms for Behavioural Congruence of Single-Pass Instruction Sequences

Published in Volume XXVII, Issue 2, 2017, pages 111-135, doi: 10.7561/SACS.2017.2.111

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

Abstract

In program algebra, an algebraic theory of single-pass instruction sequences, three congruences on instruction sequences are paid attention to: instruction sequence congruence, structural congruence, and behavioural congruence. Sound and complete axiom systems for the first two congruences were already given in early papers on program algebra. The current paper is the first one that is concerned with an axiom system for the third congruence. The presented axiom system is especially notable for its axioms that have to do with forward jump instructions.

Full Text (PDF)

References

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

[2] J. A. Bergstra and J. W. Klop. Process algebra for synchronous communication. Information and Control, 60(1–3):109–137, 1984. doi:10.1016/S0019-9958(84)80025-X.

[3] 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.

[4] 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.

[5] 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.

[6] J. A. Bergstra and C. A. Middelburg. On the behaviours produced by instruction sequences under execution. Fundamenta Informaticae, 120(2):111–144, 2012. doi:10.3233/FI-2012-753.

[7] J. A. Bergstra and C. A. Middelburg. Instruction sequence based non- uniform complexity classes. Scientific Annals of Computer Science, 24(1):47–89, 2014. doi:10.7561/SACS.2014.1.47.

[8] J. A. Bergstra and C. A. Middelburg. Instruction sequence size complexity of parity. Fundamenta Informaticae, 149(3):297–309, 2016. doi:10.3233/FI-2016-1450.

[9] J. A. Bergstra and C. A. Middelburg. On instruction sets for Boolean registers in program algebra. Scientific Annals of Computer Science, 26(1):1–26, 2016. doi:10.7561/SACS.2016.1.1

[10] S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. Journal of the ACM, 31(3):560–599, 1984. doi:10.1145/828.833.

[11] M. Hennessy and R. Milner. Algebraic laws for non-determinism and concurrency. Journal of the ACM, 32(1):137–161, 1985. doi:10.1145/ 2455.2460.

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

[13] C. A. Middelburg. Instruction sequences as a theme in computer science. https://instructionsequence.wordpress.com/, 2015.

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

Bibtex

@article{sacscuza:bergstra2017afbcosis,
  title={Axioms for Behavioural Congruence of Single-Pass Instruction Sequences},
  author={J.A. Bergstra and C.A. Middelburg},
  journal={Scientific Annals of Computer Science},
  volume={27},
  number={2},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  year={2017},
  pages={111--135},
  doi={10.7561/SACS.2017.2.111},
  publisher={``A.I. Cuza'' University Press}
}