=Paper=
{{Paper
|id=Vol-1698/CS&P2016_23_Nguyen_Computing-Bisimulation-Based-Comparisons
|storemode=property
|title=Computing Bisimulation-Based Comparisons
|pdfUrl=https://ceur-ws.org/Vol-1698/CS&P2016_23_Nguyen_Computing-Bisimulation-Based-Comparisons.pdf
|volume=Vol-1698
|authors=Linh Anh Nguyen
|dblpUrl=https://dblp.org/rec/conf/csp/Nguyen16
}}
==Computing Bisimulation-Based Comparisons==
https://ceur-ws.org/Vol-1698/CS&P2016_23_Nguyen_Computing-Bisimulation-Based-Comparisons.pdf
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.