All congruences below stability-preserving fair testing or CFFD (Q2182664)

The paper is devoted to the congruence relations that are found in the algebra of processes. Various types of equivalences were used to describe the behaviour of a parallel program. Behaviours may be compared with branching bisimilarity studied by \textit{R. J. van Glabbeek} and \textit{W. P. Weijland} [J. ACM 43, No. 3, 555--600 (1996; Zbl 0882.68085)], weak bisimilarity introduced in [\textit{R. Milner}, Communication and concurrency. New York: Prentice Hall (1989; Zbl 0683.68008)], CSP failures divergences equivalence [\textit{A. W. Roscoe}, Understanding concurrent systems. London: Springer (2010; Zbl 1211.68205)], chaos-free failures divergences (CFFD) equivalence [\textit{A. Valmari} and \textit{M. Tienari}, Formal Asp. Comput. 7, No. 4, 440--468 (1995; Zbl 0838.68076)], and numerous other equivalences. None of them is widely considered as the most natural or right notion of ``similar behaviour''. This paper proposes methods for solving this problem and continues the research of its author, begun in [\textit{A. Valmari}, ``The congruences below fair testing with initial stability'', in: Proceedings of the 16th international conference on application of concurrency to system design, ACSD 2016. Los Alamitos, CA: IEEE Computer Society. 25--34 (2016)]. In Section 2, the definition of a labeled transition system (LTS) used for modeling processes is recalled. An LTS is a tuple \((S, \Sigma, \Delta, \hat{s})\) where \(S\) is the set of states, \(\Sigma\) is an alphabet such that \(\varepsilon\notin \Sigma\) and \(\tau\notin \Sigma\), \(\Delta \subseteq S\times (\Sigma \cup \{\tau\})\times S\) is a set of transitions, and \(\hat{s}\) is the initial state. The transition \((s, a, s')\) may also be denoted \(s \overset{a}\rightarrow s'\). The designation \(s\overset{a}\rightarrow \) will mean that there is \(s'\in S\) such that \(s\overset{a}\rightarrow{s'}\). Definitions of parallel composition ``\(||\)'' and choice operator ``+'' are recalled. For an arbitrary unary operator op on a set (or class) of labeled transition systems, the equivalence relation ``\(\cong\)'' is called a congruence with respect to op if and only if for any \(L\) and \(L'\), \(L\cong L'\) implies \(\operatorname{op}(L) \cong \operatorname{op}(L')\). A congruence with respect to parallel composition is defined as a congruence with respect to two unary operators \(\operatorname{op}_1(L)= L_1|| L\) and \(\operatorname{op}_2(L)= L||L_2\). Since the parallel composition is commutative, this is equivalent to saying that this congruence is a congruence with respect to \(\operatorname{op}_1(L)\). The congruence with respect to ``+'' is defined similarly. If \(f(L_1, \ldots, L_n)\) is an expression, \(L_i\cong L'_i\) for \(1\leq i\leq n\), and ``\(\cong\)'' is a congruence with respect to all operators used in \(f\), then \(f(L_1, \ldots, L_n)\cong f(L'_1, \ldots, L'_n)\). An LTS \(L\) is called unstable if \(\hat{s}\overset{\tau}\rightarrow\), and stable otherwise. If \(L\) is stable, then we define \(\operatorname{en}(L):= \{a\in \Sigma \mid \hat{s}\overset{a}\rightarrow\}\). If \(L\) is unstable, we define \(\operatorname{en}(L):=\{\tau\}\). The set of traces of \(L\) is defined by \(\operatorname{Tr}(L):=\{\sigma\in \Sigma^* \mid \hat{s}\overset{\sigma}\rightarrow\}\). If \(L\) is stable, then \(\operatorname{en}(L)=\operatorname{Tr}(L)\cap \Sigma\). A state \(s\) of \(L\) refuses the string \(\rho\) if and only if \(s\overset{\rho}\rightarrow\) does not hold. A tree failure of \(L\) is a pair \((\sigma, K)\) where \(\sigma\in \Sigma^*\) and \(K\subseteq \Sigma^+= \Sigma^*\setminus\{\varepsilon\}\) such that there is \(s\) satisfying \(\hat{s}\overset{\sigma}\rightarrow{s}\) and \(s\) refuses \(K\). In the failures CSP [\textit{A. W. Roscoe}, Understanding concurrent systems. London: Springer (2010; Zbl 1211.68205)] of CFFD [\textit{A. Valmari}, Log. Methods Comput. Sci. 9, No. 4, Paper No. 11, 34 p. (2013; Zbl 1314.68201)], \(K\) is a set of visible actions, while now it is a set of strings of visible actions. The set of tree failures of \(L\) is denoted by \(\operatorname{Tf}(L)\). Lemmas 2, 3 and 4 are devoted to the description of \(\operatorname{Tf}(L)\). The notation \(L_1\preceq L_2\) means that for every \((\sigma, K)\in \operatorname{Tf}(L_1)\), either \((\sigma, K)\in \operatorname{Tf}(L_2)\) or there is \(\pi\) such that \(\pi\sqsubseteq K\) and \((\sigma\pi, \pi^{-1}K)\in \operatorname{Tf}(L_2)\). Here \(\pi\sqsubseteq K\) denotes that there is \(\sigma\in K\) such that \(\pi\) is a prefix of \(\sigma\). In Section 3, the following binary relations between LTSs are considered. Definition 7. Let \(L_1\) and \(L_2\) be LTSs, and let \(\{x,y\}\subseteq \{\bot, \#, \Sigma, \operatorname{en}, \operatorname{tr}, \operatorname{ft} \}\). The author defines -- \(L_1\cong_{\bot} L_2\) holds for every \(L_1\) and \(L_2\), -- \(L_1\cong_{\#} L_2\) if and only if \(\Sigma_1\# \Sigma_2\) is finite, here \(\Sigma_1\# \Sigma_2:= (\Sigma_1\setminus \Sigma_2) \cup(\Sigma_2\setminus \Sigma_1)\), -- \(L_1\cong_{\Sigma} L_2\) if and only if \(\Sigma_1=\Sigma_2\), -- \(L_1\cong_{\operatorname{en}} L_2\) if and only if \(\Sigma_1= \Sigma_2\) and \(\operatorname{en}(L_1)= \operatorname{en}(L_2)\) (this one will not be used on unstable LTSs), -- \(L_1\cong_{\operatorname{tr}} L_2\) if and only if \(\Sigma_1= \Sigma_2\) and \(\operatorname{Tr}(L_1)= \operatorname{Tr}(L_2)\) (trace equivalence), -- \(L_1\cong_{\operatorname{ft}} L_2\) if and only if \(\Sigma_1= \Sigma_2\), \(L_1\preceq L_2\), and \(L_2 \preceq L_1)\) (testing equivalence), and -- \(L_1\cong^x_y L_2\) if and only if -- \(L_1\cong_x L_2\) and \(L_1\) and \(L_2\) are both stable, or -- \(L_1\cong_y L_2\) and \(L_1\) and \(L_2\) are both unstable (stability-preserving equivalences). The relations in Definition 7 are equivalences (Lemma 9). This allows the author to consider 4 times 5 equivalences in a two-dimensional fashion. Stability-preserving fair testing equivalence is the strongest equivalence among them. It is proved that 17 of these equivalences are congruences with respect to parallel composition, hiding, and functional renaming. A table is constructed in which, for each of the 17 congruences, operators are indicated with respect to which it is a congruence (Theorem 12). The congruence properties of these 17 are also investigated with respect to relational renaming, action prefix, and choice. The remaining three equivalences are not congruences with respect to parallel composition. In Section 4, the author finds the weakest congruence that preserves stability both in the presence and in the absence of the operator of the prefix of the action. This result is central in the study of stability-preserving congruences. It does not assume the congruence property with respect to renaming, so it makes weaker assumptions than the rest of this study. In Section 5, the following statement is obtained. It is formulated in Theorem 24: Assume that ``\(\cong^{\operatorname{ft}}_{\operatorname{ft}}\)'' implies ``\(\cong\)'' and ``\(\cong\)'' is a congruence with respect to papallel composition, hiding, and functional renaming. If ``\(\cong\)'' does not imply ``\(\cong_{\#}\)'', then ``\(\cong\)'' is one of the 17 equivalences mentioned above. In Section 6, the new theory on adding initial stability-checking is presented. An arbitrary congruence is considered that does not preserve initial stability. It is denoted by ``\(\cong_o\)'', where ``\(o\)'' stands for ``original''. The following result is obtained in Theorem 27: Assume that ``\(\cong_o\)'' and ``\(\cong\)'' are congruences with respect to parallel composition and hiding, ``\(\cong_o\)'' does not preserve initial stability, and \(\cong^o_o\) implies ``\(\cong\)''. Then, if ``\(\cong\)'' does not preserve initial stability, then ``\(\cong_o\)'' implies ``\(\cong\)''. Theorem 31 shows under the same assumption that if ``\(\cong\)'' preserves initial stability, then ``\(\cong\)'' can be represented as ``\(\cong^x_y\)'' for some ``\(\cong_x\)'' and ``\(\cong_y\)'' such that ``\(\cong_y\)'' is a congruence that is implied by ``\(\cong_o\)''. Let ``congruence'' mean congruence with respect to ``\(||\)'', ``\(\backslash\)'', ``\(\Phi\)'', and ``\(a\)''. Conditions are obtained under which for a congruence, there is a congruence ``\(\cong^{\bullet}\)'' implied by ``\(\cong_o\)'' such that for stable LTSs, \(L_1\cong L_2\) if and only if \(\Sigma_1=\Sigma_2\), \(\operatorname{en}(L_1)=\operatorname{en}(L_2)\), and \(a^{-1}L_1 \cong^{\bullet} a^{-1}L_2\) for every \(a\in \operatorname{en}(L_1)\). (Theorem 39). Section 7 is devoted to the application the theory in the previous section to prove that the stability-preserving CFFD equivalence implies precisely 79 congruences with respect to parallel composition, hiding, relational renaming, action prefix, and infinite deterministic choice. 40 of them are shown in a figure, 38 of them have the form ``\(\cong^x_x\)'' for some \(x\), and the 79th is ``\(\cong^{\operatorname{en}}_{\Sigma}\)'' (Theorem 46). Section 8 contains additional remarks for each section of the article and comments on its text.