# Axioms for behavioural congruence of single-pass instruction sequences

## TL;DR

This paper develops an axiom system for behavioural congruence in program algebra, focusing on single-pass instruction sequences, with particular attention to axioms involving forward jump instructions.

## Contribution

It introduces the first axiom system specifically for behavioural congruence, expanding the algebraic theory of instruction sequences.

## Key findings

- Axiom system for behavioural congruence is sound and complete.
- Special axioms for forward jump instructions are provided.
- Advances understanding of instruction sequence equivalence.

## 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.