A precongruence format for should testing preorder

Should testing preorder was proposed as a liveness-preserving precongruence for a process algebra except nondeterministic choice operator [22]. However, this precongruence result cannot be generalized to other languages before carefully proved. In the paper, we handle this by showing that τdes format is a precongruence format for should testing preorder. A precongruence format guarantees the precongruence of given preorder by imposing syntactic restrictions on languages. The τdes format [23] was suggested to be a precongruence format for testing preorder, which is incomparable with should testing preorder on discriminative power. Moreover, we give its applications by looking into the ACP language.