Computing Bisimulation-Based Comparisons Linh Anh Nguyen Institute of Informatics, University of Warsaw Banacha 2, 02-097 Warsaw, Poland nguyen@mimuw.edu.pl Abstract. By using the idea of Henzinger et al. for computing the similarity relation, we give an efficient algorithm, with complex- ity O((m + n)n), for computing the largest bisimulation-based auto- comparison and the directed similarity relation of a labeled graph for the setting without counting successors, where m is the number of edges and n is the number of vertices. Moreover, we provide the first algorithm with a polynomial time complexity, O((m + n)2 n2 ), for computing such relations but for the setting with counting successors (like the case with graded modalities in modal logics and qualified number restrictions in description logics). 1 Introduction In a transition system, bisimilarity between states is an equivalence relation defined inductively as follows: x and x0 are bisimilar if they have the same label, each transition from x to a state y can be simulated by a transition from x0 to a state y 0 that is bisimilar to y, and vice versa (i.e., each transition from x0 to a state y 0 can be simulated by a transition from x to a state y that is bisimilar to y 0 ) [5]. In modal logic, a Kripke model can be treated as a transition system, and the characterization of bisimilarity is as follows: two states are bisimilar iff they cannot be distinguished by any formula. The “only if” implication is called the invariance and does not require additional conditions, while the whole assertion is called the Hennessy-Milner property and holds for modally saturated models (including finitely-branching models) [10, 5, 1]. Simulation between states in a transition system is a pre-order defined in- ductively as follows: x0 simulates x if they have the same label and, for each transition from x to a state y, there exists a transition from x0 to a state y 0 that simulates y. Notice the lack of the backward direction. Similarity is an equiva- lence relation defined as follows: x and x0 are similar if x simulates x0 and vice versa. In modal logic, the characterization of simulation is as follows: x0 simu- lates x iff x0 satisfies all existential formulas (in negation normal form) satisfied by x (see, e.g., [1]). The “only if” implication is a kind of preservation and does not require additional conditions, while the whole assertion can also be called the Hennessy-Milner property and holds for modally saturated models. Now, consider the pre-order . between states in a transition system defined inductively as follows, x . x0 if: the label of x is a subset of the label of x0 ; for each transition from x to a state y, there exists a transition from x0 to a state y 0 such that y . y 0 ; and conversely, for each transition from x0 to a state y 0 , there exists a transition from x to a state y such that y . y 0 . In the context of description logic, such a relation is called the largest bisimulation- based auto-comparison of the considered interpretation [4, 3]. The relation ', defined by x ' x0 iff x . x0 and x0 . x, is an equivalence relation that can be called the directed similarity relation.1 The characterization of . is as follows: x . x0 iff x0 satisfies all semi-positive formulas satisfied by x. This was proved for modally saturated interpretations in some description logics [4, 3]. The “only if” implication was proved earlier for some modal logics [8]. The above mentioned notions and their characterizations can be formulated appropriately for different kinds of transition systems and different variants or extensions of modal logic. For example, when transitions are labeled, the transi- tions used in each of the mentioned conditions should have the same label. This corresponds to the case of multimodal logics and description logics. Extensions of the basic description logic ALC may allow additional concept constructors, which may require more conditions for bisimulation or bisimulation-based com- parison [3]. Some of such constructors are qualified number restrictions, which correspond to graded modalities in graded modal logics. In this work, the case with these constructors is called the setting with counting successors, and in this case, we use the symbol .c instead of . (the latter is used for the setting without counting successors). In this work, we consider bisimulation-based comparison and directed similar- ity, formulated for (finite) labeled graphs, and the objective is to provide efficient algorithms for computing the largest bisimulation-based auto-comparison (and hence also the directed similarity relation) of a labeled graph for two settings, with or without counting successors. The related work is as follows. The Paige-Tarjan algorithms for com- puting bisimilarity [9] are currently the most efficient ones, with complexity O((m + n)n), where m is the number of transitions and n the number of states. They were originally formulated for graphs w.r.t. both the settings with or with- out counting successors, but can be reformulated or extended for other contexts (like transition systems, Kripke models, or interpretations in description logics). It exploits the idea of Hopcroft’s automaton minimization algorithm [7], but makes a generalization to deal with nondeterministic finite automata instead of deterministic ones. The currently most efficient algorithms, with complex- ity O((m + n)n), for computing the similarity relation were first provided by Bloom and Paige [2] and by Henzinger et al. [6]. The former was formulated for transition systems and the latter was formulated for graphs. They are both de- voted to the setting without counting successors. Divroodi [3] provided a simple algorithm for computing the largest bisimulation-based auto-comparison of an interpretation in a number of description logics.2 It is not efficient, having a high 1 The term “bisimulation-based comparison” of [4, 3] is a synonym of the term “di- rected simulation” of [8], and the term “directed similarity” is named in this spirit. 2 It is like Algorithm 1 given on page 5 for the setting without counting successors. polynomial time complexity for the case without counting successors, and an ex- ponential time complexity for the case with counting successors (i.e., qualified number restrictions). In this work, by using the idea of Henzinger et al. [6] for computing the similarity relation, we give an efficient algorithm, with complexity O((m + n)n), for computing the largest bisimulation-based auto-comparison and the directed similarity relation of a labeled graph for the setting without counting successors. Moreover, we provide the first algorithm with a polynomial time complexity, O((m + n)2 n2 ), for computing such relations but for the setting with counting successors. The rest of this paper is structured as follows. Section 2 formally introduces some notions. In Sections 3 and 4, we present our algorithms for the settings with or without counting successors, respectively, justify their correctness and analyze their complexity. Section 5 concludes this work. 2 Bisimulation-Based Comparisons A (finite) labeled graph is a tuple G = hV, E, A, Li, where V is a finite set of vertices, E ⊆ V 2 is a set of edges, A is a finite set of labels, and L is a function that maps each vertex to a subset of A. From now on, let G = hV, E, A, Li be a given labeled graph. For a binary relation R, we write R(x, y) to denote hx, yi ∈ R. For x ∈ V , we denote post(x) = {y ∈ V | E(x, y)} and pre(x) = {y ∈ V | E(y, x)}. A relation Z ⊆ V 2 is called a bisimulation-based auto-comparison of G without counting successors if it satisfies the following conditions for every x, y, x0 , y 0 ∈ V : Z(x, x0 ) ⇒ L(x) ⊆ L(x0 ) (1) 0 0 0 0 Z(x, x ) ∧ y ∈ post(x) ⇒ ∃y ∈ post(x ) Z(y, y ) (2) 0 0 0 0 Z(x, x ) ∧ y ∈ post(x ) ⇒ ∃y ∈ post(x) Z(y, y ). (3) 2 A relation Z ⊆ V is called a bisimulation-based auto-comparison of G with counting successors if it satisfies (1) and, for every x, x0 ∈ V , if Z(x, x0 ) holds, then there exists a bijection (4) h : post(x) → post(x0 ) such that h ⊆ Z. We write x . x0 (resp. x .c x0 ) to denote that there exists a bisimulation- based auto-comparison Z of G without (resp. with) counting successors such that Z(x, x0 ) holds. Observe that both . and .c are pre-orders, and .c is stronger than . (i.e., the former is a subset of the latter). It can be shown that the relation . (resp. .c ) is the largest (w.r.t. ⊆) bisimulation-based auto-comparison of G without (resp. with) counting successors. We write x ' x0 to denote that x . x0 and x0 . x. Similarly, we write x 'c x0 to denote that x .c x0 and x0 .c x. We call ' (resp. 'c ) the directed similarity relation of G without (resp. with) counting successors. Both ' and 'c are equivalence relations. 3 The Case without Counting Successors In this section, we present three algorithms for computing the largest bisimulation-based auto-comparison of a given labeled graph G = hV, E, A, Li in the setting without counting successors. The first two algorithms, Schematic- Comparison and RefinedComparison, are used to help to understand the last one, EfficientComparison. The idea of the EfficientComparison algorithm and the explanation via two simpler algorithms follow from the ones by Henzinger et al. for computing simulations [6]. All the three mentioned algorithms compute the sets leq(v) and geq(v) for v ∈ V , where leq(v) = {u ∈ V | u . v} and geq(v) = {u ∈ V | v . u} with . being the relation defined in Section 2. For the explanations given in the current section, however, by . we denote the following relation, which depends on and changes together with leq: {hu, vi ∈ V 2 | u ∈ leq(v)}. (5) The SchematicComparison algorithm (on page 5) initializes the sets leq(v) and geq(v), for v ∈ V , to satisfy the condition (1) with Z replaced by .. Then, while the condition (2) (resp. (3)) with Z replaced by . and x, y, x0 (resp. x0 , y 0 , x) replaced by u, v, w is not satisfied, it updates the mappings leq and geq appropriately in order to delete the pair hu, wi (resp. hw, ui) from .. It is easy to see that at the end the relation . specified by (5) is the largest bisimulation-based auto-comparison of G without counting successors. That is, the SchematicComparison algorithm is correct. The RefinedComparison algorithm (on page 5) refines the SchematicCompa- rison algorithm by using two additional mappings prevGeq and prevLeq, which approximate the mappings geq and leq, respectively. The mappings geq and leq are refined by reducing the sets geq(v) and leq(v), for v ∈ V , in each iteration of the “repeat” loop. The set prevGeq(v) (resp. prevLeq(v)) stores the value of geq(v) (resp. leq(v)) at some earlier iteration and is a superset of geq(v) (resp. leq(v)). The refinement is done by making updates only for w ∈ pre(prevGeq(v)) \ pre(geq(v)) (resp. w ∈ pre(prevLeq(v)) \ pre(leq(v))) in- stead of for w ∈ pre(geq(v)) (resp. pre(leq(v))) as in the SchematicComparison algorithm. It is straightforward to check that the conditions I1, I2, I3 listed in the RefinedComparison algorithm are invariants of the “repeat” loop. When the al- gorithm terminates, we have geq(v) = prevGeq(v) and leq(v) = prevLeq(v) for all v ∈ V , and hence the relation . specified by (5) satisfies the conditions (1)–(3) and is a bisimulation-based auto-comparison of G without counting successors. It is the largest one because the deletions of elements from the sets geq(v) and leq(v), for v ∈ V , are appropriate and done only when needed. Therefore, the RefinedComparison algorithm is correct. The EfficientComparison algorithm (on page 6) modifies the Refined- Comparison algorithm in that instead of maintaining the sets prevGeq(v) and prevLeq(v), for v ∈ V , it maintains the sets removeGeq(v) = pre(prevGeq(v)) \ pre(geq(v)), (6) Algorithm 1: SchematicComparison input : a labeled graph G = hV, E, A, Li. output : for each v ∈ V , the sets geq(v) and leq(v). 1 foreach v ∈ V do 2 geq(v) := {u ∈ V | L(v) ⊆ L(u)}; 3 leq(v) := {u ∈ V | L(u) ⊆ L(v)}; 4 repeat // assert: I0: ∀u, w ∈ V w ∈ geq(u) ↔ u ∈ leq(w) 5 if there are u, v, w ∈ V such that v ∈ post(u), w ∈ geq(u) and post(w) ∩ geq(v) = ∅ then 6 geq(u) := geq(u) \ {w}, leq(w) := leq(w) \ {u}; 7 if there are u, v, w ∈ V such that v ∈ post(u), w ∈ leq(u) and post(w) ∩ leq(v) = ∅ then 8 leq(u) := leq(u) \ {w}, geq(w) := geq(w) \ {u}; 9 until no change occurred during the last iteration; Algorithm 2: RefinedComparison 1 foreach v ∈ V do 2 prevGeq(v) := V , prevLeq(v) := V ; 3 if post(v) = ∅ then 4 geq(v) := {u ∈ V | L(v) ⊆ L(u) and post(u) = ∅}; 5 leq(v) := {u ∈ V | L(u) ⊆ L(v) and post(u) = ∅}; 6 else 7 geq(v) := {u ∈ V | L(v) ⊆ L(u) and post(u) 6= ∅}; 8 leq(v) := {u ∈ V | L(u) ⊆ L(v) and post(u) 6= ∅}; 9 repeat // assert: // I1: ∀v ∈ V geq(v) ⊆ prevGeq(v) ∧ leq(v) ⊆ prevLeq(v) // I2: ∀u, v, w ∈ V v ∈ post(u) ∧ w ∈ geq(u) → post(w) ∩ prevGeq(v) 6= ∅ // I3: ∀u, v, w ∈ V v ∈ post(u) ∧ w ∈ leq(u) → post(w) ∩ prevLeq(v) 6= ∅ 10 if there exists v ∈ V such that geq(v) 6= prevGeq(v) then 11 foreach u ∈ pre(v) and w ∈ pre(prevGeq(v)) \ pre(geq(v)) do 12 if w ∈ geq(u) then 13 geq(u) := geq(u) \ {w}, leq(w) := leq(w) \ {u}; 14 prevGeq(v) := geq(v); 15 if there exists v ∈ V such that leq(v) 6= prevLeq(v) then 16 foreach u ∈ pre(v) and w ∈ pre(prevLeq(v)) \ pre(leq(v)) do 17 if w ∈ leq(u) then 18 leq(u) := leq(u) \ {w}, geq(w) := geq(w) \ {u}; 19 prevLeq(v) := leq(v); 20 until no change occurred during the last iteration; Algorithm 3: EfficientComparison 1 foreach v ∈ V do // prevGeq(v) := V , prevLeq(v) := V 2 if post(v) = ∅ then 3 geq(v) := {u ∈ V | L(v) ⊆ L(u) and post(u) = ∅}; 4 leq(v) := {u ∈ V | L(u) ⊆ L(v) and post(u) = ∅}; 5 else 6 geq(v) := {u ∈ V | L(v) ⊆ L(u) and post(u) 6= ∅}; 7 leq(v) := {u ∈ V | L(u) ⊆ L(v) and post(u) 6= ∅}; 8 removeGeq(v) := pre(V ) \ pre(geq(v)); 9 removeLeq(v) := pre(V ) \ pre(leq(v)); 10 repeat // assert: // I4: ∀v ∈ V removeGeq(v) = pre(prevGeq(v)) \ pre(geq(v)) // I5: ∀v ∈ V removeLeq(v) = pre(prevLeq(v)) \ pre(leq(v)) 11 if there exists v ∈ V such that removeGeq(v) 6= ∅ then 12 foreach u ∈ pre(v) and w ∈ removeGeq(v) do 13 if w ∈ geq(u) then 14 geq(u) := geq(u) \ {w}, leq(w) := leq(w) \ {u}; 15 foreach w0 ∈ pre(w) do 16 if post(w0 ) ∩ geq(u) = ∅ then 17 removeGeq(u) := removeGeq(u) ∪ {w0 }; 18 foreach u0 ∈ pre(u) do 19 if post(u0 ) ∩ leq(w) = ∅ then 20 removeLeq(w) := removeLeq(w) ∪ {u0 }; // prevGeq(v) := geq(v) 21 removeGeq(v) := ∅; 22 if there exists v ∈ V such that removeLeq(v) 6= ∅ then 23 foreach u ∈ pre(v) and w ∈ removeLeq(v) do 24 if w ∈ leq(u) then 25 leq(u) := leq(u) \ {w}, geq(w) := geq(w) \ {u}; 26 foreach w0 ∈ pre(w) do 27 if post(w0 ) ∩ leq(u) = ∅ then 28 removeLeq(u) := removeLeq(u) ∪ {w0 }; 29 foreach u0 ∈ pre(u) do 30 if post(u0 ) ∩ geq(w) = ∅ then 31 removeGeq(w) := removeGeq(w) ∪ {u0 }; // prevLeq(v) := leq(v) 32 removeLeq(v) := ∅; 33 until no change occurred during the last iteration; removeLeq(v) = pre(prevLeq(v)) \ pre(leq(v)). (7) It can be checked that the equivalences (6) and (7) are invariants of the “repeat” loop if the sets prevGeq(v) and prevLeq(v) are computed as in the RefinedCom- parison algorithm by uncommenting the corresponding lines. Thus, the Efficient- Comparison algorithm reflects the RefinedComparison algorithm and is correct. We use the same idea and technique of [6] for analyzing the complexity of the EfficientComparison algorithm. Let n = |V |, m = |E| and assume that |A| is a constant. We also assume that the algorithm is modified by using and maintaining two arrays countP ostGeq[1..n, 1..n] and countP ostLeq[1..n, 1..n] of natural numbers such that countP ostGeq[w0 , u] = |post(w0 ) ∩ geq(u)| and countP ostLeq[w0 , u] = |post(w0 ) ∩ leq(u)| for all vertices w0 and u from V . These arrays are initialized in time O((m + n)n). Whenever a vertex w is removed from geq(u) (resp. leq(u)), the counters countP ostGeq[w0 , u] (resp. countP ostLeq[w0 , u]) are decremented for all predecessors w0 of w. The costs of these decrements is absorbed in the cost of the “if” statements at the lines 16, 19, 27, 30 of the algorithm. Using the arrays countP ostGeq and countP ostLeq, the test post(w0 ) ∩ geq(u) = ∅ at the line 16 and the similar ones at the lines 19, 27, 30 of those “if” statements can be executed in constant time (e.g., by checking if countP ostGeq[w0 , u] = 0 for the case of the line 16). The initialization of geq(v) and leq(v) for all v ∈ V requires time O(n2 ). The initialization of removeGeq(v) and removeLeq(v) for all v ∈ V requires time O((m + n)n). Given two vertices v and w, if the test w ∈ removeGeq(v) at the line 12 is positive in iteration i of the “repeat” loop, then that test is negative in all the iterations j > i. This is due to the invariant I4 and that – in all the iterations, w ∈ removeGeq(v) implies that w ∈ / pre(geq(v)), – the value of prevGeq(v) in all the iterations j > i is a subset of the value of geq(v) in the iteration i. It follows that the test w ∈ geq(u) at the line 13 is executed Σv Σw |pre(v)| = O((m + n)n) times. This test is positive at most once for every w and u, because after a positive test w is removed from geq(u) and never put back. Thus, the body of the “if” statement at the line 13 contributes time Σw Σu (1 + |pre(w)| + |pre(u)|) = O((m + n)n). This implies that the “if” statement at the line 11 contributes time O((m + n)n). Similarly, the “if” statement at the line 22 con- tributes time O((m + n)n). Summing up, the (modified) EfficientComparison algorithm runs in time O((m + n)n). We arrive at: Theorem 3.1. Given a labeled graph G with n vertices and m edges, the largest bisimulation-based auto-comparison of G and the directed similarity relation of G in the setting without counting successors can be computed in time O((m + n)n). 4 The Case with Counting Successors In this section, we present the ComparisonWithCountingSuccessors algorithm (on page 8) for computing the largest bisimulation-based auto-comparison of a given labeled graph G = hV, E, A, Li in the setting with counting successors. It uses the following data structures: – leq ⊆ V 2 , – remove ⊆ V 2 , – f : V 3 → V is a partial mapping, – g : V 3 → V is a partial mapping. Algorithm 4: ComparisonWithCountingSuccessors input : a labeled graph G = hV, E, A, Li. output : the relation leq. 1 set leq, remove to empty sets and f , g to empty mappings; 0 2 foreach u, u ∈ V do 3 if L(u) ⊆ L(u0 ) and |post(u)| = |post(u0 )| then 4 leq := leq ∪ {hu, u0 i}, W := post(u0 ); 5 foreach v ∈ post(u) do 6 extract v 0 from W , f (u, v, u0 ) := v 0 , g(u0 , v 0 , u) := v; 7 else remove := remove ∪ {hu, u0 i}; 8 while remove 6= ∅ do 9 extract (v, v 0 ) from remove; 10 foreach u ∈ pre(v) and u0 ∈ pre(v 0 ) such that f (u, v, u0 ) = v 0 do 11 undefine f (u, v, u0 ) and g(u0 , v 0 , u); 12 set g 0 to the empty mapping; 13 S := {v}, T 0 := ∅; 14 repeat 15 S 0 := {w0 ∈ post(u0 ) | ∃w ∈ S hw, w0 i ∈ leq} \ T 0 ; 16 foreach w0 ∈ S 0 do 17 set g 0 (w0 ) to an element w of S such that hw, w0 i ∈ leq; 18 S := {g(u0 , w0 , u) | w0 ∈ S 0 and w0 6= v 0 }, T 0 := T 0 ∪ S 0 ; 19 until S 0 = ∅ or v 0 ∈ S 0 ; 20 if S 0 = ∅ then 21 delete the pair hu, u0 i from leq; 22 undefine f (u, w, u0 ) and g(u0 , w0 , u) for any w, w0 ; 23 remove := remove ∪ {hu, u0 i}; 24 break; 25 w0 := v 0 ; 26 repeat 27 w := g 0 (w0 ), w00 := f (u, w, u0 ); 28 f (u, w, u0 ) := w0 , g(u0 , w0 , u) := w, w0 := w00 ; 29 until w = v; The variable leq will keep the relation to be computed .c . As an invariant, leq is a superset of .c . A pair hu, u0 i is deleted from leq and inserted into the set remove only when we already know that u 6.c u0 . At the beginning (in the steps 1–7), the relation leq is initialized to {hu, u0 i ∈ V 2 | L(u) ⊆ L(u0 ) ∧ |post(u)| = |post(u0 )|} and the relation remove is initialized to V 2 \ leq. Then, during the (main) “while” loop, we refine the relation leq by extracting and processing each pair hv, v 0 i from the relation remove. As invariants of that main loop, for all u, w, u0 , w0 ∈ V , leq ∩ remove = ∅, (8) f (u, w, u0 ) = w0 ⇒ hu, wi ∈ E ∧ hu, u0 i ∈ leq ∧ (9) hu0 , w0 i ∈ E ∧ hw, w0 i ∈ leq ∪ remove, g(u , w , u) = w ⇔ f (u, w, u0 ) = w0 , 0 0 (10) if leq(u, u0 ) holds, then the function λw ∈ post(u).f (u, w, u0 ) is well-defined and is a bijection between post(u) and post(u0 ) and (11) {hw, w0 i | w ∈ post(u), w0 = f (u, w, u0 )} ⊆ leq ∪ remove. Processing a pair hv, v 0 i extracted from the set remove is done as follows. For each u ∈ pre(v) and u0 ∈ pre(v 0 ) such that f (u, v, u0 ) = v 0 , we want to repair the values of the data structures so that the above invariants still hold. We first undefine f (u, v, u0 ) and g(u0 , v 0 , u) (at the line 11). Figure 1 illustrates the “repeat” loop at the lines 14–19 and its initialization at the line 13: after the initialization, S = {v} and T 0 = ∅; after the first iteration, S 0 = S10 , S = S1 and T 0 = S10 ; after the second iteration, S 0 = S20 , S = S2 and T 0 = S10 ∪ S20 ; observe that |S1 | = |S10 | and |S2 | = |S20 |. Since S 0 is disjoint with the value of T 0 in the previous iteration and T 0 is monotonically extended by S 0 , the loop will terminate with S 0 = ∅ or v 0 ∈ S 0 . Fig. 1. An illustration for the steps 14–19 of Algorithm 4. In the case S 0 = ∅, for T = {v} ∪ {w ∈ post(u) | ∃w0 ∈ T 0 f (u, w, u0 ) = w}, we have that |T | = |T 0 | + 1 and T 0 = {w0 ∈ post(u0 ) | ∃w ∈ T hw, w0 i ∈ leq} (to see this, one can use Figure 1 to help the imagination), and as a consequence, u 6.c u0 , because otherwise the condition (4) with Z replaced by .c cannot hold (recall that leq is a superset of .c ). So, in the case S 0 = ∅, we delete the pair hu, u0 i from the relation leq, add it to the relation remove, and modify the mappings f and g appropriately. In the case v 0 ∈ S 0 , the mappings f and g are repaired at the steps 25–29, using the mapping g 0 initialized at the step 12 and updated at the step 17. This is illustrated in Figure 2, where the dotted arrows from post(u) to post(u0 ) represent some pairs hw, f (u, w, u0 )i such that f (u, w, u0 ) ∈ T 0 w.r.t. the old (i.e., previous) value of f , and the normal arrows from post(u0 ) to post(u) represent some pairs hw0 , g 0 (w0 )i such that w0 ∈ T 0 . The repair relies on updating f so that those dotted arrows are replaced by the inverse of those normal arrows, and updating g to satisfy the invariant (10). Fig. 2. An illustration for the steps 25–29 of Algorithm 4. Technically, it can be checked that the conditions (8)–(11) are invariants of the (main) “while” loop. When the loop terminates, we have that remove = ∅, and the invariants (9) and (11) guarantee that leq satisfies the condition (4) with Z replaced by leq. As the condition (1) with Z replaced by leq holds due to the initialization of leq, it follows that the resulting relation leq is a bisimulation- based auto-comparison of the given labeled graph G in the setting with counting successors. As each pair hu, u0 i deleted from leq during the computation satisfies u 6.c u0 , we conclude that the resulting relation leq is the largest bisimulation- based auto-comparison of G with counting successors. Let n = |V |, m = |E| and assume that |A| is a constant. Our complexity analysis for the ComparisonWithCountingSuccessors algorithm is straightfor- ward. The steps 1–7 for initialization run in time O((m + n)n). The body of the “foreach” loop at the line 10 runs no more than (m + n)2 times totally. The “repeat” loop at the lines 14–19 runs in time O(n2 ). The steps 25–29 run in time O(n). Summing up, the algorithm runs in time O((m + n)2 n2 ). We arrive at: Theorem 4.1. Given a labeled graph G with n vertices and m edges, the largest bisimulation-based auto-comparison of G and the directed similarity relation of G in the setting with counting successors can be computed in time O((m+n)2 n2 ). 5 Conclusions By using the idea of Henzinger et al. [6] for computing the similarity relation, we have given an efficient algorithm, with complexity O((m + n)n), for comput- ing the largest bisimulation-based auto-comparison and the directed similarity relation of a labeled graph for the setting without counting successors. More- over, we have provided the first algorithm with a polynomial time complexity, O((m + n)2 n2 ), for computing such relations but for the setting with counting successors. One can adapt this latter algorithm to obtain the first algorithm with a polynomial time complexity for computing the similarity relation in the setting with counting successors. Our algorithms can also be reformulated and extended for interpretations in various modal and description logics (instead of labeled graphs). Acknowledgements This work was done in cooperation with the project 2011/02/A/HS1/00395, which is supported by the Polish National Science Centre (NCN). References 1. P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Number 53 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. 2. B. Bloom and R. Paige. Transformational design and implementation of a new effi- cient solution to the ready simulation problem. Sci. Comput. Program., 24(3):189– 220, 1995. 3. A.R. Divroodi. Bisimulation Equivalence in Description Logics and Its Applications. PhD thesis, University of Warsaw, 2015. Available at http://www.mimuw.edu.pl/wiadomosci/aktualnosci/doktoraty/pliki/ali_ rezaei_divroodi/ad-dok.pdf. 4. A.R. Divroodi and L.A. Nguyen. Bisimulation-based comparisons for interpreta- tions in description logics. In Proceedings of Description Logics’2013, volume 1014 of CEUR Workshop Proceedings, pages 652–669. CEUR-WS.org, 2013. 5. M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137–161, 1985. 6. M.R. Henzinger, T.A. Henzinger, and P.W. Kopke. Computing simulations on finite and infinite graphs. In Proceedings of FOCS’1995, pages 453–462. IEEE Computer Society, 1995. 7. J. Hopcroft. An n log n algorithm for minimizing states in a finite automa- ton. Available at ftp://reports.stanford.edu/pub/cstr/reports/cs/tr/71/ 190/CS-TR-71-190.pdf, 1971. 8. N. Kurtonina and M. de Rijke. Simulating without negation. J. Log. Comput., 7(4):501–522, 1997. 9. R. Paige and R.E. Tarjan. Three partition refinement algorithms. SIAM J. Com- put., 16(6):973–989, 1987. 10. J. van Benthem. Modal Correspondence Theory. PhD thesis, Mathematisch Insti- tuut & Instituut voor Grondslagenonderzoek, University of Amsterdam, 1976.