All congruences below stability-preserving fair testing or CFFD

This is a self-archived version of an original article. This version may differ from the original in pagination and typographic details. Author(s): Title: Year: Version: Copyright: Rights: Rights url: Please cite the original version: CC BY 4.0 https://creativecommons.org/licenses/by/4.0/ All congruences below stability-preserving fair testing or CFFD © 2020 the Author(s) Published version Valmari, Antti Valmari, A. (2020). All congruences below stability-preserving fair testing or CFFD. Acta Informatica, 57(3-5), 353-383. https://doi.org/10.1007/s00236-019-00364-4 2020 Acta Informatica (2020) 57:353–383 https://doi.org/10.1007/s00236-019-00364-4 ORIGINAL ARTICLE All congruences below stability-preserving fair testing or CFFD Antti Valmari1 Received: 24 April 2019 / Accepted: 30 December 2019 / Published online: 6 May 2020 © The Author(s) 2020 Abstract In process algebras, a congruence is an equivalence that remains valid when any subsystem is replaced by an equivalent one. Whether or not an equivalence is a congruence depends on the set of operators used in building systems from subsystems. Numerous congruences have been found, differing from each other in fine details, major ideas, or both, and none of them is good for all situations. The world of congruences seems thus chaotic, which is unpleasant, because the notion of congruence is at the heart of process algebras. This study continues attempts to clarify the big picture by proving that in certain sub-areas, there are no other congruences than those that are already known or found in the study. First, the region below stability-preserving fair testing equivalence is surveyed using an exceptionally small set of operators. The region contains few congruences, which is in sharp contrast with an earlier result on the region below Chaos-Free Failures Divergences (CFFD) equivalence, which contains 40 well-known and not well-known congruences. Second, steps are taken towards a general theory of dealing with initial stability, which is a small but popular detail. This theory is applied to the region below CFFD. 1 Introduction This study is motivated by a striking difference: in the case of sequential computation, the notion of the result of a computation at the highest level of abstraction is simple, clear and widely agreed upon, whereas in the case of concurrent computation, many alternatives are widely used and numerous more alternatives are known to exist. Let us discuss this a bit. It is universally agreed that a deterministic sequential program computes a partial function. The function is partial, because with some inputs the program may fail to terminate. This nice picture is slightly complicated by the fact that sequential programs may contain intentional nondeterminism, such as in the Miller–Rabin probabilistic primality test [1,13]; or unwanted Congratulations to Rob van Glabbeek on his 60th birthday!. BAntti Valmari antti.v[email protected] 1Faculty of Information Technology, University of Jyväskylä, P.O. Box 35, 40014 University of Jyväskylä, Finland 123 354 A. Valmari nondeterminism, such as in i=i+++1;(a Wikipedia example of undefined behavior).1 This issue could be taken into account by declaring that a sequential program executes a relation from the set of inputs to the set of outputs union {⊥}:(i,o)is in the relation if and only if, for the input i,ois a possible output or o=⊥ denoting failure to terminate. These abstract views to sequential programs are simple, natural, and widely accepted. At their level of abstraction, they have no rivals. The situation is entirely different with concurrent programs. A concurrent program computes a behaviour. Behaviours may be—and have been—compared with branching bisimilarity [8], weak bisimilarity [10], CSP failures divergences equivalence [15], Chaos-Free Failures Divergences (CFFD) equivalence [20], and numerous other equivalences. None of them is widely considered as the “most natural” or “right” notion of “similar behaviour”. If there is any agreement, it is that the choice of the most appropriate equivalence depends on the situation. Even the same users keep on switching between different equivalences depending on the task at hand, such as in [15], where, for instance, stable failures equivalence is used when the so-called catastrophic divergence phenomenon prevents the use of failures divergences equivalence. The famous survey [5], among others, has improved our understanding a lot by presenting many equivalences in a systematic framework. However, such surveys do not provide full information, because they only discuss known equivalences. They leave it open whether there could be unknown useful equivalences with interesting properties. In many situations the equivalence must be a congruence with respect to the operators that are available for building systems from subsystems. This requirement is so strong that it makes it possible to survey certain regions of equivalences, list all congruences in them, and prove that they contain no other congruences. Chapters 11 and 12 of [15] survey two regions and prove that there are three congruences in each. In [17], all congruences that are implied by the CFFD equivalence were found. This fairly large region contains 40 congruences, including stable failures equivalence, CSP failures divergences equivalence, and trace equivalence. Five kinds of failures, four kinds of infinite traces, two kinds of divergence traces, and two kinds of traces were needed, some of them new. Perhaps none of the previously unknown congruences among the 40 is interesting, but if so, then we know that no interesting congruences are lurking in that region. A task that is somewhat similar in spirit to fully surveying a region is to choose a property such as deadlock-freedom and find the weakest congruence that preserves the property. Such results have been published in, e.g., [2,4,6,7,9,11,12,14,16]. As explained in [17], knowing the weakest congruence helps in designing compositional verification algorithms for the property. The congruence property depends on the set of operators for building systems. Perhaps the most well known example of this deals with the common choice operator “+”. Branching bisimilarity, weak bisimilarity, CSP failures divergences equivalence, CFFD equivalence, and many other equivalences are not congruences with respect to it. In CSP, the congruence property was obtained by rejecting the common choice operator and introducing two other choice operators instead. In most other theories, the common choice operator was kept and the equivalence was refined so that it became a congruence. At this point it is worth mentioning that if we are only interested in so-called safety properties of systems (that is, whatever the system does must be acceptable), then there is a single very widely agreed “right” congruence: trace equivalence. Furthermore, it was proven in 1The C and C++ specifications allow it to do just anything. In practice, the value of igrows by either 1 or 2. The assigned value i+1 is computed using the original value of i, but the assignment =may be executed before or after the post-increment i++. 123 All congruences below stability-preserving fair testing or CFFD 355 [18] that any operator that satisfies a rather natural weak assumption can be constructed from parallel composition and hiding modulo trace equivalence, implying that trace equivalence is a congruence with respect to every “reasonable” operator. This situation is comparable to sequential programs in simplicity and clarity. Things become problematic indeed, when also so-called liveness properties are of interest (the system must eventually do something useful, or at least not lose the ability to nondeterministically choose to eventually do something useful). The problems are so severe that they have led to wide adoption of an equivalence that does not imply trace equivalence, that is, CSP failures divergences equivalence. The above-mentioned results in [15] use a fairly large set of operators. In particular, they use a “throw” operator that rules out many equivalences that would otherwise be congruences. The results in [17] only use parallel composition, hiding, relational renaming, and action prefix. Therefore, where the regions considered by [15]and[17] overlap, [17] gives additional congruences. In [19], of which the present study is an extension, all congruences were found that are implied by the stability-preserving fair testing equivalence of [14]. This equivalence is a congruence. It is interesting for many reasons. It is the weakest congruence that preserves the property AG EF a, that is, “in all futures always, there is a future where eventually aoccurs”. It offers an alternative approach to the verification of liveness properties. With the traditional approach, it is often necessary to explicitly state so-called fairness assumptions, which may be a burden. With fair testing equivalence this is unnecessary, because, so to speak, it has a built-in fairness assumption that is acceptable in many cases. Unlike other congruences for a significant subset of liveness properties, it has a very well-working partial order reduction method [21]. On the theoretical side, its definition is an interesting exception, because it seems somewhat ad-hoc instead of following a familiar pattern. An important feature of [19] is that only parallel composition, hiding, and functional renaming were used for proving the absence of more congruences. This is a strictly smaller set of operators than in [15]and[17]. In [17] it was proven that if a congruence is implied by strong bisimilarity (this is a very weak assumption) and preserves anything, then it preserves at least the alphabet. It was shown with two counter-examples that the result depends on the availability of the action prefix and relational renaming operators. In [19], one of the counterexamples was encountered again, and six new (albeit uninteresting) congruences were found that do not preserve the alphabet. The most important finding of [19] was that there is only one congruence between the not stability-preserving fair testing equivalence and the congruence that only preserves the alphabet: trace equivalence. If one wants to have something like fair testing, then one must go all the way to fair testing. There are no intermediate stops. This is in sharp contrast to [17]. It is also somewhat surprising, because the definition of fair testing seems quite ad-hoc, and because fair testing preserves AG EF awhich is a well-known example of a property that is not linear-time (e.g., [3, p. 32]). The importance of this result is strengthened by the fact that it was obtained in the presence of only parallel composition, hiding, and functional renaming. Also this is different from [17]. A widely used way to make an equivalence a congruence with respect to the common choice operator is to add information on initial stability: systems that can initially execute an invisible action are deemed inequivalent to systems that cannot. The study [19]wasthefirst one that fully covers a region induced by a stability-preserving congruence. Also the weakest stability-preserving congruence was found. Some unexpected or at least unconventional congruences were found, but they may be considered uninteresting, because they rely on the absence of the action prefix operator. 123 356 A. Valmari The present study makes two contributions. First, the conference paper [19] had a strict page limit, leading to dense proofs that are hard to read. The present study attempts to make the results in [19] more readable. Second, it develops a theory that greatly simplifies the treatment of initial stability when proving the absence of unknown congruences, at the cost of assuming the congruence property with respect to more operators than [19]. Therefore, it gives less general results on fair testing equivalence than [19]. On the other hand, it applies to CFFD equivalence. Section 2presents the necessary background concepts. The congruences that are implied by stability-preserving fair testing equivalence are introduced in Sect. 3. In Sect. 4, the weakest stability-preserving congruence is found. That stability-preserving fair testing equivalence does not imply more congruences is proven in Sect. 5. The new theory on adding initial stability checking is presented in Sect. 6, and applied to CFFD equivalence in Sect. 7resulting in 79 congruences. This study is concluded by a discussion section. 2 LTSs and their operators In this section we list many widely known concepts needed in this study, pointing out little facts that are useful to remember when reading our proofs. We also pay attention to details that vary in the literature, discussing the motivation of our choice. The empty string is denoted with ε. The set of strings on Ais denoted with A∗,and A+=A∗\{ε}.Ifπand σare strings, then πσdenotes that πis a prefix of σ,thatis, there is a string ρsuch that σ=πρ.Ifπis a string and Kis a set of strings, then πK denotes that there is σ∈Ksuch that πσ.WehaveεKif and only if K=∅.We define π−1K={ρ|πρ ∈K}. It is nonempty if and only if πK. Trivially ε−1K=K. The invisible action is denoted with τ. It denotes the occurrence of something that the outside world does not see. This is different from the occurrence of nothing, thus τ= ε.An alphabet is any set Σsuch that ε/∈Σand τ/∈Σ. Its elements are called visible actions. Alabelled transition system or LTS is a tuple (S,Σ,Δ,ˆs)such that Σis an alphabet, Δ⊆S×(Σ ∪{τ})×S,andˆs∈S.ElementsofSand Δare called states and transitions, respectively, and ˆsis the initial state. The transition (s,a,s)may also be denoted with s−a→s.Bys−a→we mean that there is ssuch that s−a→s. If an LTS is shown as a drawing, then, unless otherwise stated, its alphabet is the set of the visible actions along the transitions in the drawing. The alphabet may be specified explicitly in the text or near the bottom right corner of the drawing. For instance, the alphabet of τ a is {a}and the alphabet of τ a {a,b}is {a,b}. In particular, we will frequently use and τ , their alphabets being ∅. In the constructions of this study, we will often need elements that are not in a given alphabet or in a given set of states. Such entities exist because, by the axiom of foundation in set theory, if Xis a set, then X,{X},{{X}}, and so on are not elements of X. Sometimes in the literature, instead of each LTS having an alphabet of its own, there is a single global alphabet. That convention would make things difficult in the present study, because elements that are not in the alphabet would not be available. We will return to this issue in Sect. 8. We use L,M,L,M,L1,M1, and so on to denote LTSs. Unless otherwise stated, L=(S,Σ,Δ,ˆs),L=(S,Σ,Δ ,ˆs),L1=(S1,Σ 1,Δ 1,ˆs1), and so on. Because this convention is sometimes unclear, we also use Σ(L)to denote the alphabet of L.Bys−a→is we mean that (s,a,s)∈Δi. 123 All congruences below stability-preserving fair testing or CFFD 357 Researchers widely agree that at the detailed level, it is appropriate to compare behaviours using the following notion. Two LTSs L1and L2are bisimilar, denoted with L1≡L2,if and only if Σ1=Σ2and there is a relation2“∼”⊆S1×S2with the following properties: 1. ˆs1∼ˆs2. 2. If s1−a→1s 1and s1∼s2, then there is s 2such that s2−a→2s 2and s 1∼s 2. 3. If s2−a→2s 2and s1∼s2, then there is s 1such that s1−a→1s 1and s 1∼s 2. It is easy to check that if L1and L2are isomorphic, then they are bisimilar. The reachable part of an LTS (S,Σ,Δ,ˆs)is (S,Σ,Δ ,ˆs),whereSand Δconsist of those states and transitions to which there is a path from ˆs. Any LTS is bisimilar with its reachable part. Next we define the six operators that this study will focus on. Parallel composition L1L2It is the reachable part of (S,Σ,Δ,ˆs),whereS=S1×S2, Σ=Σ1∪Σ2,ˆs=(ˆs1,ˆs2),and(s1,s2)−a→(s 1,s 2)if and only if –a/∈Σ2,s1−a→1s 1,ands 2=s2∈S2, –a/∈Σ1,s2−a→2s 2,ands 1=s1∈S1,or –a∈Σ1∩Σ2,s1−a→1s 1,ands2−a→2s 2. That is, if abelongs to the alphabets of both components, then an a-transition of the parallel composition consists of simultaneous a-transitions of both components. If abelongs to the alphabet of one but not the other component, then that component may make an a-transition while the other component stays in its current state. Also each τ-transition of the parallel composition consists of one component making a τ-transition without the other participating. The result of the parallel composition is pruned by only taking the reachable part. It is easy to check that L1L2is isomorphic to (and thus bisimilar with) L2L1,and (L1L2)L3is isomorphic to L1(L2L3).Thismeansthat“” can be considered commutative and associative. Hiding L\ALet Abe a set. The hiding of Ain Lis (S,Σ,Δ ,ˆs),whereΣ=Σ\Aand Δ={(s,a,s)∈Δ|a/∈A}∪{(s,τ,s)|∃a∈A:(s,a,s)∈Δ}. That is, labels of transitions that are in Aare replaced by τand removed from the alphabet. Other labels of transitions are not affected. Relational renaming LΦLet Φbe a set of pairs such that for every (a,b)∈Φwe have τ= a= εand τ= b= ε.Thedomain of Φis D(Φ) ={a|∃b:(a,b)∈Φ}. Let the predicate Φ(a,b)hold if and only if either (a,b)∈Φor b=a/∈D(Φ).The relational renaming of Lwith Φis (S,Σ,Δ ,ˆs),whereΣ={b|∃a∈Σ:Φ(a,b)}and Δ={(s,b,s)|∃a:(s,a,s)∈Δ∧Φ(a,b)}. That is, Φrenames visible actions to visible actions. A visible action may be renamed to more than one visible action. In that case, the transitions labelled by that action are duplicated as needed. If Φspecifies no new names for an action, the transitions labelled by it remain unchanged. In particular, τ-transitions remain unchanged. The alphabet of the result consists of the new names of the original visible actions where such have been defined, and of the remaining original visible actions as such. Pairs in Φwhose first component is not in Σ have no effect. This design makes it simple to specify the intended changes without causing accidental removal of the transitions that are not intended to change. 2When a relation symbol is used as a relation, it returns a truth value and must be between an element of the domain and an element of the codomain. When a relation symbol is used as a set of pairs, usually neither of these holds. This significantly affects the intended parsing and interpretation of the expression. To reduce the risk of mis-interpretation, the author tends to point out uses as a set of pairs with double quotes. 123 358 A. Valmari Functional renaming φ(L)Functional renaming is the subcase of relational renaming where Φspecifies at most one new action name for each action. It is denoted with φ(L),where φ(a)=bif (a,b)∈Φ,andφ(a)=a, otherwise. It is included in our list of six operators, because we will encounter some equivalences that are congruences with respect to it but not with respect to relational renaming. We will frequently use the following two special cases of functional renaming as helpful notation in proofs. They attach and remove an integer ito visible actions. They will make it easy to ensure that in a parallel composition, precisely those actions synchronize whom we want to synchronize. In the notation, Ais an alphabet, ε= a= τ,andε= aj= τfor 1≤j≤n. Without loss of generality we assume that always ε= a[i]= τ. a[i]:= (a,i) (a1a2···an)[i]:= a[i] 1a[i] 2···a[i] n A[i]:= {a[i]|a∈A} L[i]:= LΦ, where Φ={(a,a[i])|a∈Σ} L[i]:= LΦ, where Φ={(a[i],a)|a[i]∈Σ} Action prefix a.L.Leta= ε.LetΣ=Σ∪{a}if a= τ,andΣ=Σotherwise. The operator a.Lyields (S,Σ,Δ ,ˆs),whereˆsis a new state (that is, ˆs/∈S), S=S∪{ˆs}, and Δ=Δ∪{(ˆs,a,ˆs)}.Thatis,a.Lstarts by executing a, after which it is in the initial state of L. Choice L1+L2Roughly speaking, the choice between L1and L2starts by executing an initial transition of L1or an initial transition of L2. This transition represents a choice between L1and L2.ThenL1+L2continues like the chosen LTS continues after the corresponding transition. This may be formalized by taking a disjoint union of L1and L2, and adding a new state that acts as the initial state of the result. For each initial transition of L1and of L2,acopyis made that starts at the new state. Indexing of state names is used to ensure that the union is disjoint. That is, L1+L2=(S,Σ,Δ ,ˆs),whereS=S[1] 1∪S[2] 2∪{ˆs},Σ=Σ1∪Σ2, Δ=Δ 1∪Δ 1∪Δ 2∪Δ 2,andˆs/∈S[1] 1∪S[2] 2,whereΔ i={(s[i],a,s[i])|(s,a,s)∈Δi} and Δ i={(ˆs,a,s[i])|(ˆsi,a,s)∈Δi}for i∈{1,2}. Also “+” can be considered commutative and associative (up to bisimilarity). Let “∼ =”and“ ∼ =” be equivalences on LTSs. We say that “∼ =”implies “∼ =”or“ ∼ =”is at least as weak as “∼ =” if and only if “∼ =”⊆“∼ =”. This is equivalent to the following: for any LTSs L1and L2we have L1∼ =L2⇒L1∼ =L2. Let “∼ =” be an equivalence on LTSs and op be a unary operator on LTSs. We say that “∼ =” isacongruence with respect to op if and only if for every Land L,L∼ =Limplies op(L)∼ = op(L). When we say that an equivalence is a congruence with respect to parallel composition, we mean that it is a congruence with respect to the two unary operators op1(L):= L1Land op2(L):= LL2. Because “” is commutative, this is equivalent to saying that the equivalence is a congruence with respect to op1(L). The similar convention and remark apply to “+”. It is easy to show with induction that if f(L1,...,Ln)is an expression, Li∼ =L ifor 1 ≤ i≤n,and“ ∼ =” is a congruence with respect to all operators used in f,then f(L1,...,Ln)∼ = f(L 1,...,L n). 3 Stability-preserving fair testing and the region below it In this section we define 4 times 5 equivalences in a two-dimensional fashion. Stabilitypreserving fair testing equivalence is the strongest equivalence among them. We prove that 123 All congruences below stability-preserving fair testing or CFFD 359 17 of these equivalences are congruences with respect to parallel composition, hiding, and functional renaming. We investigate the congruence properties of these 17 also with respect to relational renaming, action prefix, and choice. We will see that the remaining three equivalences are not congruences with respect to parallel composition. An LTS Lis unstable if and only if ˆs−τ→,andstable otherwise. If Lis stable we define en(L):= {a∈Σ|ˆs−a→}, that is, the set of visible actions that Lcan execute in its initial state. If Lis unstable, then the value of en(L)is not important. By defining it as en(L):= {τ}we get the handy property that if Lis stable and Lis unstable, then certainly en(L)= en(L). The following lemma tells how stability and en behave in LTS expressions. Lemma 1 –L 1L2is stable if and only if both L1and L2are stable. Then en(L1L2)=(en(L1)\Σ2)∪(en(L2)\Σ1)∪(en(L1)∩en(L2)). –L\A is stable if and only if L is stable and en(L)∩A=∅. Then en(L\A)=en(L). –LΦis stable if and only if L is stable. Then en(Φ(L)) ={b|∃a∈en(L):Φ(a,b)}. –φ(L)is stable if and only if L is stable. Then en(φ(L)) ={φ(a)|a∈en(L)}. –a.L is stable if and only if a = τ. Then en(a.L)={a}. –L 1+L2is stable if and only if both L1and L2are stable. Then en(L1+L2)=en(L1)∪en(L2). If s∈S,s∈S,andσ∈Σ∗,thens=σ⇒sdenotes that Lcontains a path from sto s such that the sequence of visible actions along it is σ. In particular, s=ε⇒sholds for every s∈S. The notation s=σ⇒means that there is ssuch that s=σ⇒s.Thesetoftraces of Lis Tr(L):= {σ|ˆs=σ⇒}.IfLis stable, then en(L)=Tr(L)∩Σ. A state sof L refuses the string ρif and only if s=ρ⇒does not hold. That is, refusing a string means inability to execute it to completion. Refusing a set means refusing its every element. A tree failure of Lis a pair (σ, K)where σ∈Σ∗and K⊆Σ+such that there is ssuch that ˆs=σ⇒sand srefuses K[14]. The empty string εis ruled out from Kbecause s=ε⇒holds for every state s. In the failures of CSP [15] or CFFD [17], Kis a set of visible actions, while now it is a set of strings of visible actions. The set of the tree failures of Lis denoted with Tf(L). The following lemmas express simple properties of tree failures that will be used in the sequel. Lemma 2 1. If Σ=∅,thenTr(L)={ε}and Tf(L)={(ε, ∅)}. 2. If σ∈Tr(L),then(σ, ∅)∈Tf(L). 3. If σ/∈Tr(L), then, for every πand K , (σ π, K)/∈Tf(L). Proof The first two claims are immediate from the definitions. The third claim follows from the fact that if σ/∈Tr(L),thenσπ /∈Tr(L). Lemma 3 Assume that ˆs=σ⇒s and, for every a ∈Σ,¬(s=a⇒).Then(σ, K)∈Tf(L)if and only if K ⊆Σ+. Proof It is immediate from the definition that if (σ, K)∈Tf(L),thenK⊆Σ+.IfK⊆Σ+, the state sguarantees that (σ, K)∈Tf(L)by blocking the first action of every element in K.  123 360 A. Valmari In particular, Tf( τ )=Tf( ), implying Tf(L τ )=Tf(L). This is a major difference between tree failures and the failures in CSP or CFFD theories. In CSP failures divergences equivalence divergence is catastrophic [15], meaning, among other things, that for every L and Lwith Σ=Σ,wehaveL+ τ ∼ =CSP L+ τ and L τ ∼ =CSP L τ . Also CFFD equivalence is sensitive to divergence, but in a much less dramatic fashion [17]. We mention already now that fair testing equivalence is insensitive to divergence. Lemma 4 Assume that L is stable and K ⊆Σ+. We have (ε, K)∈Tf(L)if and only if K∩Tr(L)=∅. Proof Because Lis stable, ˆs=ε⇒simplies s=ˆs. Therefore, (ε, K)∈Tf(L)if and only if ˆsrefuses K. Furthermore, ˆsrefuses ρif and only if ρ/∈Tr(L). The notation L1L2denotes that for every (σ, K)∈Tf(L1), either (σ, K)∈Tf(L2)or there is πsuch that πKand (σπ, π−1K)∈Tf(L2). The latter condition is motivated by the following example. If L=a a a ,then(ε, {aa})/∈Tf(L).Evenso,(La.a.b. ) \{a} may fail to execute b.Here(σ π, π−1K)∈Tf(L),whereσ=ε,π=a,andπ−1K={a}. For a more detailed discussion, please see [14]. The condition (σ, K)∈Tf(L2)is only needed to deal with the case K=∅, because when K=∅it is obtained from the latter condition by choosing π=ε.TheLTSsL1and L2are fair testing equivalent, if and only if Σ1=Σ2,L1L2,andL2L1[14]. If Aand Bare sets, let A#B:= (A\B)∪(B\A). Lemma 5 The following relation is an equivalence on sets: A ≈B if and only if A #Bis finite. Proof Because A#A=∅,“≈” is reflexive. Because A#B=B#A,“≈” is symmetric. To prove transitivity, assume that A≈Band B≈C.Thatis,A#Band B#Care finite. If a∈A\C,thena∈A\Bor a∈B\C.SoA\C⊆(A\B)∪(B\C). A symmetric claim holds if a∈C\A. Thus A#C⊆(A#B)∪(B#C). Therefore, also A#Cis finite, that is, A≈C. Lemma 6 Let f1(L),..., fn(L)be functions from LTSs to some sets D1,...,Dn, and let “≈i” be equivalences on Difor 1≤i≤n. Assume that “∼ =” has been defined via L ∼ =L if and only if for 1≤i≤n, fi(L)≈ifi(L).Then“ ∼ =” is an equivalence. Proof For any Land for 1 ≤i≤n,fi(L)≈ifi(L), because “≈i” is reflexive. Therefore, L∼ =L,thatis,“ ∼ =” is reflexive. If L1∼ =L2, then, for 1 ≤i≤n,fi(L1)≈ifi(L2).The symmetry of “≈i” yields fi(L2)≈ifi(L1).SoL2∼ =L1and “∼ =” is symmetric. If L1∼ =L2 and L2∼ =L3, then, for 1 ≤i≤n,fi(L1)≈ifi(L2)≈ifi(L3), yielding fi(L1)≈ifi(L3) by the transitivity of “≈i”. This means L1∼ =L3. Therefore, “∼ =” is transitive.  We now define a number of equivalences, of which twenty will be discussed in detail. The twenty will be shown in Fig. 1. Five of them do not preserve initial stability. The remaining 15 are defined by using one of the five to compare unstable LTSs, one of three equivalences to compare stable LTSs, and declaring that a stable and an unstable LTS are never equivalent. Eight of these 20 equivalences do not preserve the alphabet. If they were not congruences, they would be uninteresting indeed. However, they are congruences, and thus serve as examples of oddities that may be found when studying all congruences. The reader can skip them by skipping everything that contains # or ⊥. 123 All congruences below stability-preserving fair testing or CFFD 367 Δ(σ,K) A:= {(sσ π,a[2],sσ πa)|a∈Σ∧πaσ}∪ {(sK π,a[2],sK πa)|a∈Σ∧πaK}∪ {(sσ π,a[1],sσ π)|a∈A∧πσ}∪ {(sK π,a[1],sK π)|a∈A∧π∈K}∪ {(ˆs(σ,K) A,τ,sσ ε), (sσ σ,τ,sK ε)}. Similarly to the previous proof, f(Li):= (Li[2]L(σ,K) A)\Σ[2][1]. We have Σ(f(L1)) =Σ(f(L2)) =Σ(MA 1)=Σ(MA 2)=A. Furthermore, all these four LTSs are unstable. Let i∈{1,2}. Trivially Tr(f(Li)) ⊆A∗. Without Limoving, f(Li)can move invisibly from its initial state (ˆsi,ˆs(σ,K) A)to (ˆsi,sσ ε). Then it can execute any member of A∗, getting back to (ˆsi,sσ ε)after each transition. Therefore, Tr(f(L1)) =Tr(f(L2)) =A∗. Because (σ, K)∈Tf(L1),L1can execute σandthenbeinastateswhere it cannot execute any element of K.So f(L1)can continue invisibly from (ˆs1,sσ ε)to the state (s,sK ε),but cannot continue from there to any state of the form (s,sK π),whereπ∈K.Thatis, f(L1)can execute any element of A∗and then invisibly move to a state from which it cannot continue to a state where it can execute an element of A. As a consequence, Tf(f(L1)) =A∗×2A+= Tf(MA 1).So f(L1)∼ =ft ft MA 1. If f(L2)is in a state of the form (s,sσ π), then it can execute any member of Aimmediately. If f(L2)is in a state of the form (s,ˆs(σ,K) A), then it can execute τand enter a state of the previous form. If f(L2)is in a state of the form (s,sK π)where ε= πKor ε=πK, then by (σπ, π−1K)/∈Tf(L2)it can execute invisibly at least one member of π−1K.That takes it to a state of the form (s,sK κ)where κ∈K. There it can execute any member of A. The case remains where f(L2)is in a state of the form (s,sK ε),whereε K.ThenL2 has executed σ, implying (σ, ∅)∈Tf(L2). On the other hand, K=∅because ε K.This contradicts (σ, K)/∈Tf(L2), showing that this case is impossible. Therefore, f(L2)cannot reach a state from which it cannot continue to a state where it can execute any member of A.WehaveTf(f(L2)) =A∗×{∅}and f(L2)∼ =ft ft MA 2. By the congruence property, f(L1)∼ =f(L2).WehaveprovenMA 1∼ =ft ft f(L1)∼ = f(L2)∼ =ft ft MA 2. It implies MA 1∼ =MA 2, because “∼ =ft ft” implies “∼ =”. From now on assume that L1and L2are stable. Let gbe defined similarly to f, except that the transition ˆs(σ,K) A−τ→sσ εis replaced by ˆs(σ,K) A−a[1]→sσ εfor every a∈A.We have g(L1)∼ =g(L2)and Σ(g(L1)) =Σ(g(L2)) =Σ(MA 3)=Σ(MA 5)=A. Furthermore, all these four LTSs are stable. For any stable L,g(L)starts by executing an arbitrary member of Aand then continues like f(L). As a consequence, g(L1)∼ =ft ft MA 3and g(L2)∼ =ft ft MA 5, yielding MA 3∼ =MA 5. In the congruences of the form “∼ =x y”inFig.1,xcan only be ft,tr,oren. When proving that they suffice, the next two lemmas and Theorem 13 will be used. Lemma 16 Assume A. If there are stable L 1and L 2such that L 1∼ =L 2,Σ 1=Σ 2, and L 1ft L 2, then for any stable L1and L2such that L1∼ =tr L2we have L1∼ =L2. Proof For any stable L,let f(L):= LMΣ 3. Clearly L≡LMΣ 5. By Lemma 15 and the congruence property, LMΣ 5∼ =LMΣ 3.SoL∼ =f(L). Clearly f(L)is stable, Σ(f(L)) = Σ,andTr(f(L)) =Tr(L). 123 368 A. Valmari By Lemma 4,(ε, K)∈Tf(f(L)) if and only if K∩Tr(f(L)) =∅.TheLTSMΣ 3may deadlock after any nonempty trace. Therefore, by Lemma 3,ifσ= ε,then(σ, K)∈Tf(f(L)) if and only if σ∈Tr(f(L)) and K⊆Σ(f(L))+. As a consequence, Tf(f(L)) is determined by Σ(f(L)) and Tr(f(L)),thatis,Σand Tr(L). Let L1and L2be stable and L1∼ =tr L2.WehaveΣ1=Σ2and Tr(L1)=Tr(L2).These imply Tf(f(L1)) =Tf(f(L2)). Furthermore, f(L1)and f(L2)are stable. As a consequence, f(L1)∼ =ft ft f(L2). Hence L1∼ =f(L1)∼ =ft ft f(L2)∼ =L2, implying L1∼ =L2. Lemma 17 Assume A. If there are stable L 1and L 2such that L 1∼ =L 2,Σ 1=Σ 2, and L 1tr L 2, then for any stable L1and L2such that L1∼ =en L2we have L1∼ =L2. Proof For any stable L,let f(L):= LMΣ 4. Because “∼ =ft” implies “∼ =tr”, the assumptions of Lemma 15 hold. By Lemmas 14 and 15,L≡LMΣ 5∼ =LMΣ 3∼ =LMΣ 4.SoL∼ = f(L). Clearly f(L)is stable and Σ(f(L)) =Σ. Because Tr(MΣ 4)=Σ∪{ε},wehave Tr(f(L)) =en(L)∪{ε}. It implies en(f(L)) =en(L). By Lemma 4,(ε, K)∈Tf(f(L)) if and only if K∩Tr(f(L)) =∅. By Lemma 3,ifσ= ε, then (σ, K)∈Tf(f(L)) if and only if σ∈Tr(f(L)) and K⊆Σ(f(L))+. As a consequence, Tf(f(L)) is determined by Σ(f(L)) and en(f(L)),thatis,Σand en(L). Let L1and L2be stable and L1∼ =en L2.WehaveΣ1=Σ2and en(L1)=en(L2).These imply Tf(f(L1)) =Tf(f(L2)). Furthermore, f(L1)and f(L2)are stable. As a consequence, f(L1)∼ =ft ft f(L2). Hence L1∼ =f(L1)∼ =ft ft f(L2)∼ =L2, implying L1∼ =L2. In the sequel, we will have to deal with cases where stability does not matter, and with cases where it matters and the LTSs in question are unstable. To exploit results on the latter when dealing with the former, we define a simple operator that, given an LTS, yields an unstable “∼ =ft”-equivalent LTS. We let us(L):= L τ . The following lemma tells some properties of us(L). Lemma 18 Assume A. For every L we have the following. 1. us(L)is unstable. 2. us(L)∼ =ft L. 3. If L is unstable, then us(L)∼ =ft ft L and us(L)∼ =L. 4. If there are L1and L2such that L1∼ =L2,Σ1=Σ2, and L1ft L2,thenus(L)∼ = LMΣ 1. 5. If there are L1and L2such that L1∼ =L2,Σ1=Σ2, and L1tr L2,thenus(L)∼ = ( τ )Σ. Proof The first three claims are obvious. For any L,us(L)∼ =ft ft LMΣ 2, because they both have Σas the alphabet, they are both unstable, and MΣ 2never blocks actions of L. With the assumptions of the fourth claim, Lemma 15 and the congruence property yield LMΣ 2∼ =LMΣ 1. As a consequence, us(L)∼ = LMΣ 1. With the assumptions of the last claim, for any L, Lemma 14 yields LMΣ 1∼ =L( τ )Σ. Clearly L( τ )Σ≡( τ )Σ, because ( τ )Σblocks all visible actions of L. Because “∼ =ft” implies “∼ =tr”, claim 4 yields us(L)∼ =LMΣ 1.Sous(L)∼ =( τ )Σ. 123 All congruences below stability-preserving fair testing or CFFD 369 The next lemma tells that if the congruence equates a stable and an unstable LTS, then stability does not matter at all. Lemma 19 Assume that “∼ =ft ft” implies “∼ =” and “∼ =” is a congruence with respect to parallel composition and hiding. If there are a stable LTS Lsand an unstable LTS Lusuch that Ls∼ =Lu,then 1. ∼ = τ , and 2. for any L, L ∼ =us(L). Proof Let Σ:= Σ(Ls)∪Σ(Lu)and f(L):= (LΣ)\Σ. Clearly f(Ls)≡.The alphabet of f(Lu)is ∅=Σ( τ ),andTf(f(Lu)) ={(ε, ∅)}=Tf( τ )by Lemma 2(1). Furthermore, f(Lu)is obviously unstable. So f(Lu)∼ =ft ft τ . These yield ≡f(Ls)∼ = f(Lu)∼ =ft ft τ . Therefore, ∼ = τ . Let Lbe any LTS. Clearly L≡L∼ =L τ =us(L),soL∼ =us(L). The next lemma says that if the congruence does not preserve the alphabet, then, in the case of unstable LTSs, it throws away all information on traces and tree failures. Lemma 20 Assume A. If “∼ =” does not imply “∼ =Σ”, then, for any L, us(L)∼ =( τ )Σ. Proof Because “∼ =” does not imply “∼ =Σ”, there are L1,L2,andasuch that L1∼ =L2, a∈Σ1,anda/∈Σ2.LetΣ:= (Σ1∪Σ2)\{a}. If L1=a⇒, then choose any b/∈{a,τ,ε}and let f(L):= φ(L{b})\Σ,where φ(b):= aand φ(x):= xif x= b.Wehave f(L1)=a⇒but ¬(f(L2)=a⇒). Although a/∈Σ2,wehaveΣ(f(L2)) ={a}thanks to {b}and φ. If ¬(L1=a⇒),thenlet f(L):= (La)\Σ.Wehave¬(f(L1)=a⇒)but f(L2)=a⇒. In both cases, f(L1)∼ =f(L2),Σ(f(L1)) =Σ(f(L2)) ={a},andTr(f(L1)) = Tr(f(L2)). By Lemma 18(5), for any L,us(L)∼ =( τ )Σ. If L1∼ =L2where ∼ =is a congruence with respect to parallel composition, then us(L1)= L1 τ ∼ =L2 τ =us(L2), yielding us(L1)∼ =us(L2).Nextweproveus(L1)∼ =us(L2) under five different assumptions, without assuming L1∼ =L2. Lemma 21 Assume A. In each of the following situations we have us(L1)∼ =us(L2). 1. If L1∼ =ft L2. 2. If L1∼ =tr L2, and “∼ =” implies “∼ =Σ” but not “∼ =ft”. 3. If L1∼ =ΣL2, and “∼ =” implies “∼ =Σ” but not “∼ =tr”. 4. If L1∼ =#L2, and “∼ =” does not imply “∼ =Σ”. 5. If the alphabets of L1and L2are countable, and “∼ =” does not imply “∼ =#”. Proof 1. By Lemma 18(2), us(L1)∼ =ft L1∼ =ft L2∼ =ft us(L2).Sous(L1)∼ =ft us(L2).This implies us(L1)∼ =ft ft us(L2), because us(L1)and us(L2)are unstable by Lemma 18(1). By assumption A, this implies us(L1)∼ =us(L2). 2. Let L∈{L1,L2}and f(L):= LMΣ 1. It is unstable because of MΣ 1,so f(L1)∼ =⊥ ⊥f(L2). We have Σ(f(L)) =Σ. Because MΣ 1may deadlock after any trace, Lemma 3yields Tf(f(L)) ={(σ, K)|σ∈Tr(L)∧K⊆Σ+}. Because L1∼ =tr L2,wehaveΣ1=Σ2 and Tr(L1)=Tr(L2). These yield f(L1)∼ =ft ft f(L2), implying f(L1)∼ =f(L2). The part 123 370 A. Valmari of the condition after “and” justifies the use of Lemma 18(4), implying us(L1)∼ =f(L1)∼ = f(L2)∼ =us(L2). 3. The condition L1∼ =ΣL2means that Σ1=Σ2. By Lemma 18(5), us(L1)∼ =( τ )Σ1= ( τ )Σ2∼ =us(L2). 4. The condition L1∼ =#L2means that Σ1#Σ2is finite. Because “∼ =” does not imply “∼ =Σ”, there are L 1,L 2,andasuch that L 1∼ =L 2,a∈Σ 1,anda/∈Σ 2.LetΣ:= (Σ 1∪Σ 2)\{a}.By Lemma 20, τ ∼ =us(L 2\Σ) ∼ =us(L 1\Σ) ∼ =( τ ){a},whereus(L 2\Σ) ∼ =us(L 1\Σ) follows from L 1∼ =L 2. Therefore, τ ∼ =( τ ){a}. Choose any bsuch that τ= b= ε.Letφ(a):= band φ(x):= xwhen x= a.Wehave τ ≡φ( τ )∼ =φ(( τ ){a})≡( τ ){b}.So τ ∼ =( τ ){b}.LetA={a1,...,an} be any finite alphabet. For 0 ≤i<n,wehave( τ ){a1,...,ai}≡( τ ){a1,...,ai} τ ∼ =( τ ){a1,...,ai}( τ ){ai+1}≡( τ ){a1,...,ai+1}. By induction, τ ∼ =( τ )A. If Σ1#Σ2is finite, then also Σ1\Σ2and Σ2\Σ1are finite. By Lemma 20,us(L1)∼ = ( τ )Σ1≡( τ )Σ1∩Σ2( τ )Σ1\Σ2∼ =( τ )Σ1∩Σ2 τ ∼ =( τ )Σ1∩Σ2( τ )Σ2\Σ1≡ ( τ )Σ2∼ =us(L2). 5. By the assumption, there are L 1and L 2such that L 1∼ =L 2and Σ 1\Σ 2is infinite. By Lemma 20, τ ∼ =us(L 2\Σ 2)∼ =us(L 1\Σ 2)∼ =( τ )Σ 1\Σ 2. Let Abe any countable alphabet. If A=∅,then τ =( τ )A. Otherwise there is a∈A. Because every infinite set contains a countably infinite subset, there is a bijection ffrom Ato a subset of Σ 1\Σ 2. A surjection φfrom Σ 1\Σ 2to Ais obtained by letting φ(x):= bif x=f(b)and φ(x):= aif there is no bsuch that x=f(b). We have τ ≡φ( τ )∼ =φ(( τ )Σ 1\Σ 2)=( τ )A. So both A=∅and A=∅yield τ ∼ =( τ )A. We conclude us(L1)∼ =( τ )Σ1∼ = τ ∼ =( τ )Σ2∼ =us(L2). We now have sufficient machinery to prove the main result. We deal first with the case where stability matters. Lemma 22 Let x be any of ft,tr, and en, and let prev(x)be the previous one (if x = ft). Let y be any of ft,tr,Σ,#, and ⊥, and let prev(y)be the previous one (if y = ft). Assume A and that “∼ =” implies “∼ =x y”. If x = ft, assume also that “∼ =” does not imply “∼ =prev(x) y”. If y = ft, assume also that “∼ =” does not imply “∼ =x prev(y)”. If y =⊥, assume also that the alphabets of the LTSs are countable. Then “∼ =”is“ ∼ =x y”. Proof That “∼ =”is“ ∼ =x y” means that “∼ =” implies “∼ =x y”and“ ∼ =x y” implies “∼ =”. The former was given in the assumption part of the lemma. Our task is to prove the latter for each xand y.SoweassumethatL1and L2are arbitrary LTSs such that L1∼ =x yL2, and we have to prove that L1∼ =L2. The definition of “∼ =x y” implies that L1and L2are both stable or both unstable. If L1and L2are stable,thenL1∼ =xL2. There are three cases. –Ifx=ft,thenL1and L2are stable and L1∼ =ft L2. By definition, L1∼ =ft ft L2. It implies L1∼ =L2by assumption A. –Ifx=tr,thenL1∼ =tr L2and there are L 1and L 2such that L 1∼ =L 2but L 1ft yL 2. Because L 1∼ =L 2implies L 1∼ =tr yL 2, this means that L 1and L 2are both stable, L 1ft L 2,andΣ 1=Σ 2. Lemma 16 yields L1∼ =L2. 123 All congruences below stability-preserving fair testing or CFFD 371 –Ifx=en,thenL1∼ =en L2and there are L 1and L 2such that L 1∼ =L 2but L 1tr yL 2. Because L 1∼ =L 2implies L 1∼ =en yL 2,thismeansthatL 1and L 2are both stable, L 1tr L 2,andΣ 1=Σ 2. Lemma 17 yields L1∼ =L2. If L1and L2are unstable, then Lemma 18(3) yields L1∼ =us(L1)and us(L2)∼ =L2.We will soon show that the assumptions of Lemma 21 hold. By it, us(L1)∼ =us(L2), yielding L1∼ =L2. Because L1and L2are unstable, L1∼ =x yL2implies L1∼ =yL2.Thisgivesthefirst condition of Lemma 21(1) to (4). The first condition of (5) is in the assumptions of the current lemma. When y=tr or y=Σ,then“ ∼ =” implies “∼ =x y” implies “∼ =Σ”, because both “∼ =x”and“ ∼ =y”imply“ ∼ =Σ”. This is needed by (2) and (3). When y= ft, then there are L 1 and L 2such that L 1∼ =L 2yielding L 1∼ =x yL 2,butL 1x prev(y)L 2. They are unstable and satisfy L 1prev(y)L 2.So“ ∼ =” does not imply “∼ =prev(y)”. This gives the last condition of (2) to (5) and completes the checking of the assumptions of Lemma 21. Before continuing, it is perhaps a good idea to discuss a bit the fact that Lemma 22 refers to three equivalences that are grey in Fig. 1. First, in some cases “∼ =x prev(y)”or“ ∼ =prev(x) y”isgrey. This is not a problem, because the lemma does not assume that it is a congruence. It only assumes that there are L 1and L 2such that L 1∼ =L 2but L 1x prev(y)L 2and L 1prev(x) yL 2. Second, the lemma may claim that “∼ =”is“ ∼ =x y”alsowhen“ ∼ =x y” is grey. This is not a problem, because the lemma does not promise but assumes that “∼ =” is a congruence. The lemma says that if there is a congruence with the assumed properties, then it is “∼ =x y”. If “∼ =x y” is not a congruence, then, with the chosen xand y, no congruences satisfy the assumptions of the lemma. The case remains where stability does not matter. Lemma 23 Let y be any of ft,tr,Σ,#, and ⊥, and let prev(y)be the previous one (if y = ft). Assume A and that “∼ =” implies “∼ =y” but not “∼ =y y” or not “∼ =en y”. If y = ft, assume also that “∼ =” does not imply “∼ =prev(y)”. If y =⊥, assume also that the alphabets of the LTSs are countable. Then “∼ =”is“ ∼ =y”. Proof We first show that there are L 1and L 2such that one of them is stable, the other is unstable, and L 1∼ =L 2. By the assumptions, there are L 1and L 2such that L 1∼ =L 2and either L 1y yL 2or L 1en yL 2. Because “∼ =” implies “∼ =y”, we have L 1∼ =yL 2. If one of L 1 and L 2is stable and the other is unstable, then they qualify as L 1and L 2. Because L 1∼ =yL 2, the only remaining possibility is that L 1and L 2are both stable and L 1en L 2. The latter implies L 1en ⊥L 2,so“ ∼ =” does not imply “∼ =en ⊥”andTheorem13 gives the claim. As a consequence, for every L, Lemma 19(2) yields L∼ =us(L).IfL1∼ =yL2,then L1∼ =us(L1)∼ =us(L2)∼ =L2by Lemma 21 and the fact that “∼ =tr” implies “∼ =Σ”. Therefore, “∼ =y” implies “∼ =”. It was assumed that “∼ =” implies “∼ =y”. Hence “∼ =”is“ ∼ =y”.  Theorem 24 Assume that “∼ =ft ft” implies “∼ =” and “∼ =” is a congruence with respect to parallel composition, hiding, and functional renaming. If “∼ =” does not imply “∼ =#”, then also assume that the alphabets of the LTSs are countable. Then “∼ =” is one of the black equivalences in Fig. 1. Proof The congruence “∼ =”impliesatleast“ ∼ =⊥”. Therefore, among the “∼ =y”wherey∈ {ft,tr,Σ,#,⊥}that it implies, there is a first one. For this y,if“ ∼ =” does not imply the next black equivalence to the left of “∼ =y”inFig.1, then Lemma 23 applies, saying that “∼ =”is “∼ =y”. 123 372 A. Valmari Otherwise, “∼ =” implies some “∼ =x y”inFig.1.If“ ∼ =” also implies the next equivalence to the left (if x= ft) or the next equivalence above (if y= ft), go there even if it is grey. Repeat this until it is possible to go neither left nor up. Now Lemma 22 applies, saying that “∼ =”is “∼ =x y”. As a consequence, the 20 equivalences in Fig. 1contain all congruences that are implied by “∼ =ft ft” (making the countability assumption where needed). In Sect. 3we proved that the black ones among them are congruences and the grey ones are not.  6 A somewhat general theory on adding stability preservation Let “∼ =o” be a congruence that does not preserve initial stability. Here “o” stands for “original”. The goal is to find all congruences that are implied by “∼ =o o” (that is, “∼ =o”∩“∼ =⊥ ⊥”), in terms of the congruences that are implied by “∼ =o”. (There is no point in studying the case where “∼ =o” preserves initial stability, for then “∼ =o o”and“ ∼ =o” coincide.) The first part of our work only needs very weak assumptions: Assumption B.“ ∼ =o”and“ ∼ =” are congruences with respect to parallel composition and hiding, “∼ =o” does not preserve initial stability, and “∼ =o o” implies “∼ =”. The following simple lemma will be used often. Lemma 25 Assume B. If L1∼ =oL2and L1∼ =⊥ ⊥L2,thenL 1∼ =L2. Proof The definitions of “∼ =o o”and“ ∼ =” yield L1∼ =o oL2and L1∼ =L2. We first deal with the case that also “∼ =” does not preserve initial stability. Lemma 26 If “∼ =” is a congruence with respect to “” and “\” and does not preserve initial stability, then there is an unstable LTS U such that ∼ =U. Proof Bytheassumption,thereareastableLTSLsand an unstable LTS Lusuch that Ls∼ =Lu. Let Σ=Σ(Ls).Wehave Σ≡LsΣ∼ =LuΣ,so =Σ\Σ∼ =(LuΣ)\Σ.The latter is unstable.  Theorem 27 Assume B. If “∼ =” does not preserve initial stability, then “∼ =o” implies “∼ =”. Proof Assume that L1∼ =oL2.WehavetoshowL1∼ =L2. Let Ube like in Lemma 26. Because “∼ =o” is a congruence, we have L1U∼ =oL2U. Both L1Uand L2Uare unstable because Uis unstable. Therefore, Lemma 25 yields L1U∼ =L2U. Because “∼ =” is a congruence, L1≡L1∼ =L1Uand similarly L2∼ =L2U. Altogether L1∼ =L1U∼ =L2U∼ =L2giving L1∼ =L2. In the rest of this section “∼ =” does preserve initial stability. Therefore, “∼ =” can be represented in the form “∼ =x y”, where “∼ =x” is a binary relation such that for stable LTSs L1∼ =xL2⇔ L1∼ =L2,and“ ∼ =y” is a binary relation such that for unstable LTSs L1∼ =yL2⇔L1∼ =L2. We now show that for every “∼ =”, “∼ =y” can be chosen so that it is a congruence that is implied by “∼ =o”. Application of Lemma 26 to “∼ =o” in place of “∼ =” tells that there is an unstable Uosuch that ∼ =oUo.WedefineL1∼ =τL2:⇔ L1Uo∼ =L2Uo, and prove that “∼ =τ” qualifies as “∼ =y”. 123 All congruences below stability-preserving fair testing or CFFD 373 Lemma 28 Assume B. Then “∼ =τ” is a congruence. Proof Because “∼ =” is an equivalence, Lemma 6implies that “∼ =τ” is an equivalence as well. Let op(L)be any operator with respect to which “∼ =” is a congruence. We assume that L1∼ =τL2and show that op(L1)∼ =τop(L2). By the definition, L1Uo∼ =L2Uo. Because “∼ =” is a congruence, we have op(L1Uo)∼ = op(L2Uo)and op(L1Uo)Uo∼ =op(L2Uo)Uo. Let L∈{L1,L2}. Because ∼ =oUoand “∼ =o” is a congruence, we have L≡L∼ =o LUoand op(L)Uo∼ =oop(LUo)Uo.Bothop(L)Uoand op(LUo)Uoare unstable, so Lemma 25 yields op(L)Uo∼ =op(LUo)Uo. We have op(L1)Uo∼ =op(L1Uo)Uo∼ =op(L2Uo)Uo∼ =op(L2)Uo. Therefore, op(L1)∼ =τop(L2). Lemma 29 Assume B. Then “∼ =o” implies “∼ =τ”. Proof Assume that L1∼ =oL2. Because “∼ =o” is a congruence, we have L1Uo∼ =oL2Uo. Since L1Uoand L2Uoare unstable, Lemma 25 yields L1Uo∼ =L2Uo,thatis,L1∼ =τL2.  Lemma 30 Assume B and that L1and L2are unstable. Then L1∼ =L2if and only if L1∼ =τL2. Proof Assume that L1∼ =L2. Because “∼ =” is a congruence, we have L1Uo∼ =L2Uo,that is, L1∼ =τL2. Assume that L1∼ =τL2.Thatis,L1Uo∼ =L2Uo.Likeabove,wehave L1≡L1∼ =oL1Uo. Because L1and L1Uoare unstable, Lemma 25 yields L1∼ =L1Uo. Similar reasoning yields L2∼ =L2Uo. Altogether L1∼ =L1Uo∼ =L2Uo∼ =L2. Theorem 31 Assume B. If “∼ =” preserves initial stability, then “∼ =” can be represented as “∼ =x y”forsome“ ∼ =x” and “∼ =y” such that “∼ =y” is a congruence that is implied by “∼ =o”. Proof “∼ =y”is“ ∼ =τ”.  The fact that “∼ =en Σ” is a congruence tells that a corresponding theorem for “∼ =x” must be more complicated. This is because the congruence “∼ =en Σ” is implied by “∼ =tr tr”, but no congruence implied by “∼ =tr” matches “∼ =en Σ” on stable LTSs. Therefore, in the place of “∼ =x” we will use a relation that checks that L1∼ =en L2and, roughly speaking, for each a∈en(L1),the behaviours of L1after aand L2after aare in a congruence that is implied by “∼ =o”. Our proof relies on much stronger assumptions than assumption B. The first part of the assumptions is shown below, and the second part will be presented after we have developed the necessary notions. Assumption C.“ ∼ =o”and“ ∼ =” are congruences with respect to parallel composition, hiding, relational renaming, and action prefix; “∼ =o” does not but “∼ =” does preserve initial stability; and “∼ =o o” implies “∼ =”. We now define the congruence that is implied by “∼ =o”. Definition 32 For any LTSs L1and L2,wedefineL1∼ =•L2if and only if there is x/∈ Σ1∪Σ2∪{τ,ε}such that x.L1∼ =x.L2. Lemma 33 Assume C. If L1∼ =•L2,thena.L1∼ =a.L2holds for all a /∈{τ,ε}. 123 374 A. Valmari Proof Let xbe like in Definition 32. Because “∼ =” is a congruence with respect to “Φ”, x.L1∼ =x.L2implies (x.L1){(x,a)}∼ =(x.L2){(x,a)}. Because x/∈Σ1∪Σ2we have a.L1=(x.L1){(x,a)}∼ =(x.L2){(x,a)}=a.L2, yielding a.L1∼ =a.L2. Lemma 34 Assume C. The relation “∼ =•” is a congruence with respect to “”, “\”, “Φ”, and “a.”. Proof Let L1,L2and L3be LTSs, aa visible action, Aa set of visible actions, and Φaset of pairs of visible actions. Let xbe a visible action that is not in A∪{a}∪Σ1∪Σ2∪Σ3 and not in any pair of Φ. By Lemma 33, whenever L∼ =•Lholds below for some Land L, we have x.L∼ =x.L. Because “∼ =” is an equivalence, we have the following. Obviously x.L1∼ =x.L1.So “∼ =•” is reflexive. If L1∼ =•L2,thenx.L1∼ =x.L2.Sox.L2∼ =x.L1and L2∼ =•L1. Thus “∼ =•” is symmetric. If L1∼ =•L2and L2∼ =•L3,thenx.L1∼ =x.L2and x.L2∼ =x.L3,so x.L1∼ =x.L3. Therefore, L1∼ =•L3and “∼ =•” is transitive. Because x/∈Σ1∪Σ2∪Σ3∪{τ,ε},wehavex.(LiL3)≡(x.Li)(x.L3)when i=1or i=2. If L1∼ =•L2,thenx.L1∼ =x.L2. Because “∼ =” is a congruence with respect to “”, we have (x.L1)(x.L3)∼ =(x.L2)(x.L3).Sox.(L1L3)∼ =x.(L2L3)and L1L3∼ =•L2L3. Similar reasoning proves L3L1∼ =•L3L2. Therefore, “∼ =•” is a congruence with respect to “”. Because x/∈A,wehavex.(Li\A)≡(x.Li)\Awhen i=1ori=2. If L1∼ =•L2, then x.L1∼ =x.L2. Because “∼ =” is a congruence with respect to “\”, we have (x.L1)\A∼ = (x.L2)\A.Sox.(L1\A)∼ =x.(L2\A)and L1\A∼ =•L2\A. Therefore, “∼ =•” is a congruence with respect to “\”. By the choice of x,wehavex.(LiΦ) ≡(x.Li)Φ when i=1ori=2. If L1∼ =•L2, then x.L1∼ =x.L2. Because “∼ =” is a congruence with respect to “Φ”, we have (x.L1)Φ ∼ = (x.L2)Φ.Sox.(L1Φ) ∼ =x.(L2Φ) and L1Φ∼ =•L2Φ. Therefore, “∼ =•” is a congruence with respect to “Φ”. If L1∼ =•L2,thena.L1∼ =a.L2by Lemma 33. Because “∼ =” is a congruence with respect to “x.”, we have x.(a.L1)∼ =x.(a.L2).Soa.L1∼ =•a.L2. Therefore, “∼ =•”isa congruence with respect to “a.”. By choosing aso that it is not in Σ1∪Σ2we also get τ.L1=(a.L1)\{a}∼ =•(a.L2)\{a}=τ.L2, because we have already shown that “∼ =•”isa congruence with respect to “\”. Thus “∼ =•” is a congruence with respect to “τ.”.  Lemma 35 Assume C. Then “∼ =o” implies “∼ =•”. Proof Assume that L1∼ =oL2.Letx/∈Σ1∪Σ2∪{τ,ε}. By the congruence property, we have x.L1∼ =ox.L2.Sincex.L1and x.L2are stable, Lemma 25 yields x.L1∼ =x.L2.That is, L1∼ =•L2. We will soon make it precise what we mean by the behaviour of a stable LTS after a visible action. As a preparatory step, let Σbe a set of visible actions and xa visible action. We define xΣas the two-state LTS whose alphabet is Σ∪{x}and transitions are {(ˆsx,x,sx)}∪ {(sx,a,sx)|a∈Σ}. Let L=(S,Σ,Δ,ˆs)beastableLTS,a∈Σ,andx/∈Σ∪{τ,ε}. We will soon use the LTS La x=L{(a,x)(a,a)} xΣ. To get intuition for it, we now show that it is isomorphic to the reachable part of L=(S,Σ,Δ ,ˆs),whereˆsis a new state (that is, ˆs/∈S), S=S∪{ˆs},Σ=Σ∪{x},andΔ=Δ∪{(ˆs,x,s)|(ˆs,a,s)∈Δ}(Fig. 5). The LTS xΣhas two states ˆsxand sx. The states of La xare of the form (s,s), where s∈Sand s∈{ˆsx,sx}. Because the alphabet of both L{(a,x)(a,a)}and xΣis 123 All congruences below stability-preserving fair testing or CFFD 375 L La x x x x a a a b b ... ... ... ... ... L a b idf (L) τ τ τ τ τ a a a b b ... ... ... ... ... a−1L b−1L Fig. 5 Illustrating La x(left), a−1L,andidf (L)(right) Σ∪{x}, and because xΣhas no τ-transitions, the transitions of La xare of three forms: (s,ˆsx)−x→(s,sx)where (thanks to the renaming) (s,a,s)∈Δ;(s,sx)−b→(s,sx) where b∈Σand (s,b,s)∈Δ;and(s,s x)−τ→(s,s x)where (s,τ,s)∈Δand s x∈{ˆsx,sx}.Onceˆsxhas been left, it cannot be re-entered. Furthermore, Lis stable. Therefore, the states of the form (s,ˆsx)where s=ˆsare unreachable. The states of the form (s,sx)and their outgoing transitions constitute a copy of the reachable part of L, in addition to which there is the transition (ˆs,ˆsx)−x→(s,sx)for every (ˆs,a,s)of the reachable part of L. The LTS La x\{x}is otherwise similar, but it lacks xin its alphabet and its initial transitions are labelled with τinstead of x. It is independent of the choice of x(as long as x/∈Σ∪{τ,ε}). In structural operational semantics, L−a→L La x\{x}−τ→L and that is all La x\{x}can do. From now on we denote it with a−1L.Thatis,ifLis a stable LTS, a∈Σ,andx/∈Σ∪{τ,ε}, then we define a−1L=(L{(a,x)(a,a)} xΣ)\{x}. It is easy to check that Σ(a−1L)=Σ. Lemma 36 Assume C. If L1∼ =L2where L1and L2are stable, then Σ1=Σ2,en(L1)= en(L2), and a−1L1∼ =•a−1L2for every a ∈en(L1). Proof Theorem 13 yields L1∼ =en L2,thatis,Σ1=Σ2and en(L1)=en(L2). The congruence properties of “∼ =” and the definition of a−1Lyield x.(a−1L1)∼ =x.(a−1L2), from which the definition of “∼ =•” yields the last claim.  To prove the converse of Lemma 36, we discuss the construction of L,whena−1Lis given for each a∈en(L). Then we present the assumptions we will use in addition to assumption C. Let Abe a set of visible actions and Labe an LTS for each a∈A.IfAis finite, then it is of the form {a1,...,an},wheretheaiare distinct from each other. We define finite deterministic choice between a1.La1,…,an.Lanas a∈Aa.La=a1.La1+···+an.Lan. Infinite deterministic choice is the natural extension to infinite A,anddeterministic choice is finite or infinite deterministic choice. “Deterministic” signifies that a∈Aa.Lahas precisely one initial transition for each a∈A, and no other initial transitions. Definition 37 If Lis stable, then by its initially deterministic form we mean idf (L)= a∈en(L) a.(a−1L). 123 376 A. Valmari Assumption D.L∼ =oidf (L)holds for every stable L,and“ ∼ =” is a congruence with respect to infinite deterministic choice. We need not assume that “∼ =” is a congruence with respect to finite deterministic choice, because Lemma 40 will tell that it is. However, we first focus on the big picture, and present the result where Assumption D is needed. Lemma 38 Assume C and D. If L1and L2are stable, en(L1)=en(L2), and a−1L1∼ =• a−1L2for every a ∈en(L1),thenL 1∼ =L2. Proof Clearly idf (L)is stable, so Assumption D and Lemma 25 imply L1∼ =idf (L1)and idf (L2)∼ =L2. Because a−1L1∼ =•a−1L2and ais visible, by Lemma 33,a.(a−1L1) ∼ =a.(a−1L2)for each a∈en(L1)=en(L2). Thus Lemma 40 (in the finite case) and Assumption D (in the infinite case) yield idf (L1)∼ =idf (L2). We can now prove a result that resembles Lemma 30 and can be used to characterize the “∼ =x” in Theorem 31. Theorem 39 Let “congruence” mean with respect to “”, “\”, “Φ”, and “a.”. Let “∼ =o” and “∼ =” be congruences such that “∼ =o o” implies “∼ =”, and “∼ =o” does not but “∼ =” does preserve initial stability. Also assume D. There is a congruence “∼ =•” implied by “∼ =o” such that for stable LTSs, L1∼ =L2if and only if Σ1=Σ2,en(L1)=en(L2), and a−1L1∼ =•a−1L2for every a ∈en(L1). Proof The assumptions in the theorem imply Assumption C. By Lemmas 34 and 35,the relation in Definition 32 is a congruence implied by “∼ =o”. Lemmas 36 and 38 give the last claim.  The use of Assumption D reduces the generality of this theorem. The rest of this section is devoted to a brief analysis on conditions where Assumption D holds. Based on it, we will see in the next section that the first half of Assumption D is not a problem with CFFD equivalence. Next we show that if we restrict ourselves to LTSs Lsuch that en(L)is finite whenever Lis stable, then the latter part of D need not be assumed. We do that by showing that the choice operator can be constructed from parallel composition and functional renaming, if the LTSs are stable. If Aand Bare sets of visible actions, we define C(A,B):= A ABB, where each thick arrow denotes a transition for each member of the label of the arrow. Lemma 40 If L1and L2are stable, then L1+L2≡L1[1]L2[2]C(Σ[1] 1,Σ[2] 2)[1,2]. Proof Let the right hand side be called R. Because of the renaming, the alphabets of L1[1] and L2[2]are disjoint and the alphabet of C(...)is their union. So all visible transitions of Rare either joint transitions by L1[1]and C(...)or joint transitions by L2[2]and C(...). Thanks to ...[1,2], they have the labels that are used in L1and L2. Because C(...)has no τ-transitions, all τ-transitions of Rarise from τ-transitions of L1or τ-transitions of L2. Let the states of C(...)be called c1,ˆc,andc2. The initial state of Ris (ˆs1,ˆs2,ˆc).Ithasno τ-transitions, because L1and L2are stable. It has the transitions (ˆs1,ˆs2,ˆc)−a→(s1,ˆs2,c1) where ˆs1−a→s1is a transition of L1,and(ˆs1,ˆs2,ˆc)−a→(ˆs1,s2,c2)where ˆs2−a→s2is a transition of L2. When in c1,C(...)stays there forever, blocks L2in ˆs2, and lets L1proceed freely. Therefore, states of the form (s1,ˆs2,c1)and their outgoing transitions constitute a copy of L1. A similar claim holds about (ˆs1,s2,c2)and L2. 123 All congruences below stability-preserving fair testing or CFFD 383 17. Valmari, A.: All linear-time congruences for familiar operators. Logic. Methods Comput. Sci. 9(4:11), 1–34 (2013) 18. Valmari, A.: On constructibility and unconstructibility of LTS operators from other LTS operators. Acta Inf. 52(2–3), 207–234 (2015) 19. Valmari, A.: The congruences below fair testing with initial stability. In: Desel, J., Yakovlev, A. (eds.) 16th International Conference on Application of Concurrency to System Design, ACSD 2016, Torun, Poland, June 19–24, 2016, pp. 25–34. IEEE Computer Society (2016) 20. Valmari, A., Tienari, M.: Compositional failure-based semantics models for basic LOTOS. Formal Asp. Comput. 7(4), 440–468 (1995) 21. Valmari, A., Vogler, W.: Fair testing and stubborn sets. STTT 20(5), 589–610 (2018) Publisher’s Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations. 123