By using the idea of Henzinger et al. for computing the similarity relation, we give an e cient algorithm, with complexity O((m + n)n), for computing the largest bisimulation-based autocomparison 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 rst algorithm with a polynomial time complexity, O((m + n)2n2), for computing such relations but for the setting with counting successors (like the case with graded modalities in modal logics and quali ed number restrictions in description logics).
In a transition system, bisimilarity between states is an equivalence relation de ned 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 y0 that is bisimilar to y, and vice versa (i.e., each transition from x0 to a state y0 can be simulated by a transition from x to a state y that is bisimilar to y0) [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 i 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 nitely-branching models) [10, 5, 1].
Simulation between states in a transition system is a pre-order de ned inductively 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 y0 that simulates y. Notice the lack of the backward direction. Similarity is an equivalence relation de ned 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 simulates x i x0 satis es all existential formulas (in negation normal form) satis ed 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 de ned 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 y0 such that y . y0; and conversely, for each transition from x0 to a state y0, there exists a transition from x to a state y such that y . y0. In the context of description logic, such a relation is called the largest bisimulationbased auto-comparison of the considered interpretation [4, 3]. The relation ', de ned by x ' x0 i 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 i x0 satis es all semi-positive formulas satis ed 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 di erent kinds of transition systems and di erent variants or extensions of modal logic. For example, when transitions are labeled, the transitions 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 comparison [3]. Some of such constructors are quali ed 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 similarity, formulated for ( nite) labeled graphs, and the objective is to provide e cient 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 computing bisimilarity [9] are currently the most e cient 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 without 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 nite automata instead of deterministic ones. The currently most e cient algorithms, with complexity O((m + n)n), for computing the similarity relation were rst 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 devoted 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 e cient, having a high 1 The term \bisimulation-based comparison" of [4, 3] is a synonym of the term \directed 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 exponential time complexity for the case with counting successors (i.e., quali ed number restrictions).
In this work, by using the idea of Henzinger et al. [6] for computing the similarity relation, we give an e cient 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 rst algorithm with a polynomial time complexity, O((m + n)2n2), 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
A ( nite) labeled graph is a tuple G = hV; E; A; Li, where V is a nite set of vertices, E V 2 is a set of edges, A is a nite 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 2 R. For x 2 V , we denote post (x) = fy 2 V j E(x; y)g and pre(x) = fy 2 V j E(y; x)g.
A relation Z V 2 is called a bisimulation-based auto-comparison of G without counting successors if it satis es the following conditions for every x; y; x0; y0 2 V :
Z(x; x0) ) L(x)
L(x0) Z(x; x0) ^ y 2 post (x) ) 9y0 2 post (x0) Z(y; y0)
Z(x; x0) ^ y0 2 post (x0) ) 9y 2 post (x) Z(y; y0):
A relation Z V 2 is called a bisimulation-based auto-comparison of G with
counting successors if it satis es (
We write x . x0 (resp. x .c x0) to denote that there exists a bisimulationbased 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.
(
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 rst two algorithms, SchematicComparison and Re nedComparison, are used to help to understand the last one, E cientComparison. The idea of the E cientComparison 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 2 V , where leq (v) = fu 2 V j u . vg and geq (v) = fu 2 V j v . ug with .
being the relation de ned 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 :
fhu; vi 2 V 2 j u 2 leq (v)g:
(
The SchematicComparison algorithm (on page 5) initializes the sets leq (v)
and geq (v), for v 2 V , to satisfy the condition (
The Re nedComparison algorithm (on page 5) re nes the
SchematicComparison algorithm by using two additional mappings prevGeq and prevLeq , which
approximate the mappings geq and leq , respectively. The mappings geq and
leq are re ned by reducing the sets geq (v) and leq (v), for v 2 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 re nement is done by making updates only for
w 2 pre(prevGeq (v)) n pre(geq (v)) (resp. w 2 pre(prevLeq (v)) n pre(leq (v)))
instead of for w 2 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
Re nedComparison algorithm are invariants of the \repeat" loop. When the
algorithm terminates, we have geq (v) = prevGeq (v) and leq (v) = prevLeq (v) for all
v 2 V , and hence the relation . speci ed by (
The E cientComparison algorithm (on page 6) modi es the Re nedComparison algorithm in that instead of maintaining the sets prevGeq (v) and prevLeq (v), for v 2 V , it maintains the sets removeGeq (v) = pre(prevGeq (v)) n pre(geq (v)); 4 repeat
// assert: I0: 8u; w 2 V w 2 geq(u) $ u 2 leq(w) 5 if there are u; v; w 2 V such that v 2 post (u), w 2 geq(u) and
post (w) \ geq(v) = ; then 6 geq(u) := geq(u) n fwg, leq(w) := leq(w) n fug; if there are u; v; w 2 V such that v 2 post (u), w 2 leq(u) and post (w) \ leq(v) = ; then
leq(u) := leq(u) n fwg, geq(w) := geq(w) n fug; 9 until no change occurred during the last iteration ; 20 until no change occurred during the last iteration ;
Algorithm 2: Re nedComparison
2 prevGeq(v) := V , prevLeq(v) := V ; 3 if post (v) = ; then 4 geq(v) := fu 2 V j L(v) 5 leq(v) := fu 2 V j L(u) else
L(u) and post (u) = ;g;
L(v) and post (u) = ;g; 9 repeat // assert: // I1: 8v 2 V geq(v) prevGeq(v) ^ leq(v) prevLeq(v) // I2: 8u; v; w 2 V v 2 post (u) ^ w 2 geq(u) ! post (w) \ prevGeq(v) 6= ; // I3: 8u; v; w 2 V v 2 post (u) ^ w 2 leq(u) ! post (w) \ prevLeq(v) 6= ; if there exists v 2 V such that geq(v) 6= prevGeq(v) then foreach u 2 pre(v) and w 2 pre(prevGeq(v)) n pre(geq(v)) do if w 2 geq(u) then
geq(u) := geq(u) n fwg, leq(w) := leq(w) n fug; prevGeq(v) := geq(v); if there exists v 2 V such that leq(v) 6= prevLeq(v) then foreach u 2 pre(v) and w 2 pre(prevLeq(v)) n pre(leq(v)) do if w 2 leq(u) then
leq(u) := leq(u) n fwg, geq(w) := geq(w) n fug; prevLeq(v) := leq(v);
// prevGeq(v) := V , prevLeq(v) := V if post (v) = ; then geq(v) := fu 2 V j L(v) leq(v) := fu 2 V j L(u) else removeGeq(v) := pre(V ) n pre(geq(v)); removeLeq(v) := pre(V ) n pre(leq(v)); 10 repeat // assert: // I4: 8v 2 V removeGeq(v) = pre(prevGeq(v)) n pre(geq(v)) // I5: 8v 2 V removeLeq(v) = pre(prevLeq(v)) n pre(leq(v)) if there exists v 2 V such that removeGeq (v) 6= ; then foreach u 2 pre(v) and w 2 removeGeq(v) do if w 2 geq(u) then geq(u) := geq(u) n fwg, leq(w) := leq(w) n fug; foreach w0 2 pre(w) do if post (w0) \ geq(u) = ; then
removeGeq(u) := removeGeq(u) [ fw0g; foreach u0 2 pre(u) do if post (u0) \ leq(w) = ; then
removeLeq(w) := removeLeq(w) [ fu0g; // prevGeq(v) := geq(v) removeGeq(v) := ;; if there exists v 2 V such that removeLeq (v) 6= ; then foreach u 2 pre(v) and w 2 removeLeq(v) do if w 2 leq(u) then leq(u) := leq(u) n fwg, geq(w) := geq(w) n fug; foreach w0 2 pre(w) do if post (w0) \ leq(u) = ; then
removeLeq(u) := removeLeq(u) [ fw0g; foreach u0 2 pre(u) do if post (u0) \ geq(w) = ; then
removeGeq(w) := removeGeq(w) [ fu0g; // prevLeq(v) := leq(v) removeLeq(v) := ;; 33 until no change occurred during the last iteration ; removeLeq (v) = pre(prevLeq (v)) n 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 Re nedComparison algorithm by uncommenting the corresponding lines. Thus, the E cientComparison algorithm re ects the Re nedComparison algorithm and is correct.
We use the same idea and technique of [6] for analyzing the complexity of the E cientComparison algorithm. Let n = jV j, m = jEj and assume that jAj is a constant. We also assume that the algorithm is modi ed 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] = jpost (w0) \ geq (u)j and countP ostLeq[w0; u] = jpost (w0) \ leq (u)j 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 2 V requires time O(n2). The initialization of removeGeq (v) and removeLeq (v) for all v 2 V requires time O((m + n)n). Given two vertices v and w, if the test w 2 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 2 removeGeq (v) implies that w 2= 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 2 geq (u) at the line 13 is executed v wjpre(v)j = 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 + jpre(w)j + jpre(u)j) = 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 contributes time O((m + n)n). Summing up, the (modi ed) E cientComparison 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
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; 2 foreach u; u0 2 V do 3 if L(u) L(u0) and jpost (u)j = jpost (u0)j then 4 leq := leq [ fhu; u0ig, W := post (u0); 5 foreach v 2 post (u) do 6 extract v0 from W , f (u; v; u0) := v0, g(u0; v0; u) := v; 7
else remove := remove [ fhu; u0ig; 8 while remove 6= ; do 9 extract (v; v0) from remove; 10 foreach u 2 pre(v) and u0 2 pre(v0) such that f (u; v; u0) = v0 do 11 unde ne f (u; v; u0) and g(u0; v0; u); 12 set g0 to the empty mapping; 13 S := fvg, T 0 := ;; 14 repeat 15 S0 := fw0 2 post (u0) j 9w 2 S hw; w0i 2 leqg n T 0; 16 foreach w0 2 S0 do 17 set g0(w0) to an element w of S such that hw; w0i 2 leq;
The variable leq will keep the relation to be computed .c. As an invariant, leq is a superset of .c. A pair hu; u0i 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 fhu; u0i 2 V 2 j L(u) L(u0) ^ jpost (u)j = jpost (u0)jg and the relation remove is initialized to V 2 n leq . Then, during the (main) \while" loop, we re ne the relation leq by extracting and processing each pair hv; v0i from the relation remove. As invariants of that main loop, for all u; w; u0; w0 2 V , leq \ remove = ;; f (u; w; u0) = w0 ) hu; wi 2 E ^ hu; u0i 2 leq ^
hu0; w0i 2 E ^ hw; w0i 2 leq [ remove, g(u0; w0; u) = w , f (u; w; u0) = w0; if leq (u; u0) holds, then the function w 2 post (u):f (u; w; u0) is well-de ned and is a bijection between post (u) and post (u0) and fhw; w0i j w 2 post (u); w0 = f (u; w; u0)g leq [ remove. (8) (9) (10) (11)
Processing a pair hv; v0i extracted from the set remove is done as follows. For each u 2 pre(v) and u0 2 pre(v0) such that f (u; v; u0) = v0, we want to repair the values of the data structures so that the above invariants still hold. We rst unde ne f (u; v; u0) and g(u0; v0; 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 = fvg and T 0 = ;; after the rst iteration, S0 = S10, S = S1 and T 0 = S0 ; after the second iteration, S0 = S0 , S = S2 and T 0 = S10 [ S0 ; 1 2 2 observe that jS1j = jS10j and jS2j = jS20j. Since S0 is disjoint with the value of T 0 in the previous iteration and T 0 is monotonically extended by S0, the loop will terminate with S0 = ; or v0 2 S0.
In the case S0 = ;, for T = fvg [ fw 2 post (u) j 9w0 2 T 0 f (u; w; u0) = wg,
we have that jT j = jT 0j + 1 and T 0 = fw0 2 post (u0) j 9w 2 T hw; w0i 2 leq g (to
see this, one can use Figure 1 to help the imagination), and as a consequence,
u 6.c u0, because otherwise the condition (
In the case v0 2 S0, the mappings f and g are repaired at the steps 25{29, using the mapping g0 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) 2 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; g0(w0)i such that w0 2 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).
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 satis es the condition (
Let n = jV j, m = jEj and assume that jAj is a constant. Our complexity analysis for the ComparisonWithCountingSuccessors algorithm is straightforward. 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)2n2). 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)2n2). 5
By using the idea of Henzinger et al. [6] for computing the similarity relation, we have given an e cient 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 have provided the rst algorithm with a polynomial time complexity, O((m + n)2n2), for computing such relations but for the setting with counting successors. One can adapt this latter algorithm to obtain the rst 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).
This work was done in cooperation with the project 2011/02/A/HS1/00395,
which is supported by the Polish National Science Centre (NCN).
6. M.R. Henzinger, T.A. Henzinger, and P.W. Kopke. Computing simulations on
nite and in nite 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 nite
automaton. 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(