All Linear-Time Congruences for Finite LTSs and Familiar Operators

In process-algebraic verification, one can use many different semantic congruences. The weakest congruence that preserves the properties of interest is optimal, because it leaves most room for reducing the labelled transition system (LTS) that represents the behaviour of the system to be verified. Weakest congruences for some properties have been known. However, there has been no systematic treatment. This publication finds, for finite LTSs, all stuttering-insensitive linear-time congruences with respect to action prefix, hiding, relational renaming, and parallel composition. There are 20 of them. They are built from the alphabet, traces, two kinds of divergence traces, and five kinds of failures. Because of lack of space, the publication concentrates on the hardest and most novel part of the result, that is, proving the absence of more congruences.