The simulation preorder is widely used both as a behavioral relation in concurrent systems, and as an abstraction tool to reduce the state space in model checking, were memory requirement is clearly a critical issue. Therefore, in this context a simulation algorithm should address both time and space efficiency. In this paper, we rely on the notion of rank to design an efficient simulation algorithm. It turns out that such algorithm outperforms-both in terms of time and in terms of space-the best simulation algorithms in the literature, on the class of acyclic graphs.
the branching temporal logics CTL and CTL∗ [
State of the Art Among the algorithms for computing the simulation preorder, the
most well known ones are by Henzinger, Henzinger and Kopke [
Our Contribution We propose a simulation algorithm that has optimal performances
w.r.t. both time and space on acyclic graphs, outperforming [
In this section we introduce the basic notations we use in the rest of the paper. Definition 1. Let V be a set and Q ⊆ V × V a binary relation over V : – Q is said to be a preorder over V if and only if Q is reflexive and transitive; – Q is said to be a partial order over V if and only if Q is reflexive, antisymmetric, and transitive; – Q is said to be acyclic if and only if its transitive closure is antisymmetric. We will use Q+ to refer to the transitive closure of Q and Q∗ to refer to the reflexive and transitive closure of Q.
Notice that if a relation is acyclic, then it is antisymmetric, while the converse does not hold (unless it is transitive).
Definition 2. A triple G = hV, E, Σi is said to be a labelled graph if and only if G− = hV, Ei is a finite graph and Σ is a partition over V . We say that two nodes v1, v2 ∈ V have the same label if they belong to the same class of Σ.
An equivalent way to define labelled graphs is to use a labelling function ℓ : V → L, where L is a finite set of labels (inducing of a partition ΣL of V ). Given a node v ∈ V we will use [v]Σ (or [v], if Σ is clear from the context) to denote the class of Σ to which v belongs.
Example 1. A Kripke Structure is a labelled graph and, vice-versa, each connected labelled graph can be seen as a Kripke Structure in which two worlds satisfy the same set of atomic propositions if and only if their labels are equal.
Definition 3. Let G = hV, E, Σi be a labelled graph. A relation ≤⊆ V × V is said to be a simulation over G if and only if: 1. v ≤ u → [v]Σ = [u]Σ ; 2. (v ≤ u ∧ vEv1) → ∃u1(uEu1 ∧ v1 ≤ u1).
In this case we also say that u simulates v.
We say that u and v are sim-equivalent (u ≡s v) if there exist two simulations ≤1 and ≤2, such that n ≤1 m and m ≤2 n.
Notice that a simulation can be neither reflexive nor transitive (e.g. the empty relation
is always a simulation), however the reader can easily verify that given an arbitrary
simulation its reflexive and transitive closure is always a simulation. A simulation ≤s
over G is said to be maximal if for all the simulations ≤ over G it holds ≤⊆≤s. Given
a labelled graph G = hN, E, Σi there always exists a unique maximal simulation ≤s
over G. Moreover ≤s is a preorder [
Example 2. Consider the labelled graph G = hV, E, Σi depicted in Figure 1, where V = {x, y, z}, E = {(x, y), (x, z), (y, z)}, and Σ = {α = {x, y}, β = {z}}. The maximum simulation preorder on G is given by I ∪ {(y, x)}, where I denotes the identity relation over V . β
z
Given a labelled graph G, the simulation problem consists in determining the
maximum simulation preorder on G, and can be elegantly encoded in terms of a
coarsest partition pair problem [
Definition 4 (Partition Pairs). Let V be a set. A partition pair on V is a pair hΣ, Ri, where Σ is a partition on V and R is a reflexive relation on Σ.
Given a set V , each preorder relation P on V induces a corresponding partition pair hV≡P , P i, where ≡P is the equivalence relation ≡P = {(u, v) | u ≺P v ∧ v P u}, and P = {(α, β) ∈ V≡P | ∃u ∈ α, ∃v ∈ β.(u P v)}. In particular, given a labelled graph G = hV, E, Σi, we denote by hV≡S , Si the partition pair on V corresponding to the maximum simulation preorder S of G consistent w.r.t. Σ.
Definition 5. Let hΣ, Ri, hΠ, P i be two partition pairs on V :
hΠ, P i ⊑ hΣ, Ri ⇔ Π is finer than Σ and P ⊆ R(Π) where R(Π) denotes the relation on Π induced by R ⊆ Σ × Σ, i.e.:
∀α, β ∈ Π((α, β) ∈ R(Π) ⇔ ∃α′, β′((α′, β′) ∈ R ∧ α ⊆ α′ ∧ β ⊆ β′)) Given two sets of nodes α, β ⊆ V we write α →∃ β to denote that there exists a node a ∈ α which reaches a node b ∈ β, i.e., (a, b) ∈ E. Similarly, α →∀ β denotes that each node in α reaches a node in β.
Definition 6 (Stability). Let G = hV, Ei be a graph, let hΣ, Ri be a partition pair on V . hΣ, Ri is said stable w.r.t. the transition relation of the graph E iff: ∀α, β ∈ Σ(α →∃ β ⇒ [{δ | δ ∈ R(α)} →∀ [{δ | δ ∈ R(β)} Definition 7 (Coarsest Partition Pair Problem (CPPP)). Let G = hV, E, Σi be a labelled graph, and consider the identity relation I on Σ. The coarsest partition pair problem asks to determine the coarsest partition pair hΠ, P i ⊑ hΣ, Ii stable w.r.t. E. Lemma 1 (CPPP as Simulation Problem). Let G = hV, E, Σi be a labelled graph. The coarsest partition pair problem is well defined and admits as unique solution the partition pair hV≡S , Si, corresponding to the maximum simulation preorder on G consistent w.r.t. Σ.
Proof. We show that the unique solution to the CPPP is the partition pair hV≡S , Si ⊑ hΣ, Ii corresponding to the maximum simulation preorder S on G = hV, Ei consistent w.r.t. Σ. We start by proving that hV≡S , Si is stable w.r.t. E. Let α, β ∈ V≡S and assume that α →∃ β. Then, there exist two nodes s ∈ α, s′ ∈ β such that s → s′. Consider an arbitrary node p ∈ S{δ | δ ∈ S(α)}. Since s a node p′ such that p → p′ and s′
choice of p ∈ S{δ | δ ∈ S(α)} guarantees that S{δ | δ ∈ S(α)} →∀ S{δ | δ ∈ S(β)},
i.e. hV≡S , Si is stable w.r.t E.
To conclude our thesis, assume by absurd that there exists a partition pair hΠ, P i ⊑ hΣ, Ii stable w.r.t. E and such that ¬(hΠ, P i ⊑ hV≡S , Si). Consider the relation <hΠ,P i⊆ V × V , where <hΠ,P i= {(s, s′) | ([s]Π , [s′]Π ) ∈ P }. By our assumption stating that ¬(hΠ, P i ⊑ hV≡S , Si), we have that <hΠ,P i*
lows by proving that <hΠ,P i is a simulation on G = hV, Ei consistent w.r.t. Σ. In fact, in that case the relation <hΠ,P i ∪ including the maximum simulation preorder
S . To prove that <hΠ,P i is a simulation on G = hV, Ei consistent w.r.t. Σ, let (s, s′) ∈<hΠ,P i. By hΠ, P i ⊑ hΣ, Ii, we have that [s]Σ = [s′]Σ . Consider p such that s → p. Then [s]Π →∃ [p]Π . Since hΠ, P i is stable w.r.t. E we have that s′ ∈ S{δ | δ ∈ P ([s]Π )} has an edge to a node p′ ∈ S{δ | δ ∈ P ([p]Π )}, i.e. to a node p′ such that (p, p′) ∈<hΠ,P i. ⊔⊓ 3
An Optimal Simulation Algorithm on Acyclic Graphs In this section, we introduce an optimal simulation algorithm (w.r.t. both time and space) on acyclic graphs. Such a procedure relies on solving the coarsest partition pair problem (i.e. computing the maximum simulation preorder) proceeding by rank. The notion of rank, introduced in Definition 8, allows one to perform a preliminary partition in the given labelled graph. This is useful to drive the successive computation, as stated in Lemma 2. defined as: Definition 8. Let G = hV, Ei be an acyclic graph, let v ∈ V . The rank of the node v is rank(v) = 0 max{1 + rank (u) | (v, u) ∈ E} if E(v) = ∅, otherwise.
Example 3. Consider the labelled graph in Figure 1, described in Example 2. In such a graph, node x has rank 2, node y has rank 1 and node z has rank 0.
Lemma 2 (Rank & Simulation). Let G = hV, Ei be an acyclic graph, and consider a partition Σ on V . Then:
hV≡S , Si ⊑ hV≡R , Ri where hV≡S , Si is the partition pair on V encoding the maximum simulation consistent w.r.t. Σ, and hV≡R , Ri is the partition pair on V corresponding to the rank-labelling preorder
R= {(u, v) | rank (u) ≤ rank (v)}.
Proof. By absurd, assume that ¬(hV≡S , Si ⊑ hV≡R , Ri). It follows that the maximum simulation preorder
S is not included in the relation {(s, s′) | ([s]≡R , [s′]≡R ) ∈ R}, i.e. there exists two nodes s ∈ V , s′ ∈ V such that s S s′ and rank (s) > rank (s′).
Let r = rank (s) > rank (s′). Since rank (s) = r, we can determine a sequence of there exists a corresponding sequence of r nodes s′1, . . . , s′r such that r nodes s1, . . . , sr such that s → s1 V1≤i<r si → si+1. By definition of simulation, ^
⊔⊓ within Example 2. The algorithm SolveCPPP in Table 1 terminates upon the execution of the first loop at line 3, that uses the information given by the rank to refine the initial partition pair hΣ, Ii to the partition pair hΠ, P i, where Π = {α = {x}, α1 = {y}, β = {z}} and P = I ∪ {(α1, α)}. In fact, in this case the preprocessing provided by the loop at line 3 is sufficient to solve the simulation problem. 4
In this section, we prove the correctness of our simulation algorithm on acyclic graphs, as well as its complexity. 4.1
Correctness Lemma 3, below, shows that the preprocessing step correctly computes the partition pair induced by the rank labelling of the graph.
Lemma 3. The loop at line 3 in the algorithm SolveCPPP(hV, Ei, hΣ, Ii) terminates computing the partition pair hΠ, P i and the variable rankMax, where: • rankMax= max{rank (v) | v ∈ V }, • Π ⊑ Σ is the coarsest partition finer than the rank-labelling partition V≡R , • P = {(α, β) | rank (α) ≤ rank (β) ∧ ∃γ ∈ Σ(α ⊆ γ ∧ β ⊆ γ)} Proof. This can be easily proved by induction on the number of loop iterations. ⊔⊓ Algorithm 1: SOLVECPPP input : G = hV, Ei,hΣ, I = {(α, α) | α ∈ Σ}i output: hV≡S , Si: partition pair encoding the maximum simulation preorder S on G consistent w.r.t. Σ. 1 begin
/* Initial refinement & rank-ordering of the classes. */ 2 notRanked := V ; rankMax := −1 3 repeat 4 forall α ∈ Σ | α ⊆ notRanked ∧ α * pre(notRanked) do 5 if α 6= α \ pre(notRanked) then 6 α1 := α\pre(notRanked); α := α\α1; rank(α1) := rankMax+1; Σ := Σ ∪ {α1}; sim := sim ∪ {(γ, α1) | (γ, α) ∈ sim} ∪ {(α1, α)} Lemma 4 and Theorem 1 define crucial invariants and prove their validity throughout the execution of the main loop at line 12. Such invariants define the correctness of our simulation algorithm.
Lemma 4. Consider the overall execution of the for-loop at line 12 guarded by the variable 1 ≤ rk ≤ rankM ax. Whenever a class γ is involved either in a split or in a refinement of its simulator set S{β | (γ, β) ∈ sim}, the following statement holds: rank (γ) ≥ rk Proof. Denote by hΣi, simii the partition pair in input to the i-th iteration of the forloop at line 12. Moreover, if γ is a class processed within the i-th execution of the for-loop at lines 12, let γi denote the unique class γi ∈ Σi such that γi ⊇ γ.
Given the above notations, consider the i-th execution of the for-loop at lines 12 (for which rk = i) and let γ be a class in a partition pair processed within such an iteration. Assume that either γ ⊂ γi, or S{β | (γ, β) ∈ sim} 6= S{βi | (γi, βi) ∈ simi}. Then, there exists a pair of classed {α, β} ⊆ Σi such that rank (β) = i − 1, α →∃ β and γi ∈ simi(α). rank (β) = i − 1 ∧ α →∃ β implies rank (α) ≥ i. Lemma 3 allows then to conclude that rank (γ) = rank (γi) ≥ i. ⊔⊓ Theorem 1. The following invariants hold at the beginning of each iteration of the for-loop at line 12, within the the algorithm SolveCPPP(hV, Ei, hΣ0, Ii). 1. For each node v ∈ V such that rank (v) < rk: Base (rk = 1). The first two items in our statement follow directly from Lemma 2 and Lemma 3, while the third item holds trivially since no class β ∈ Σ has a rank strictly lower than rk − 1 = 0.
Inductive Step (1 < rk). Given i ≥ 1, denote by hΣi, simii the partition pair in input to the i-th execution of the for-loop at line 12. Given γ ∈ Σi>1, denote by γi−1 the only class in Σi−1 such that γi−1 ⊇ γ. 1. In order to prove our inductive step for item (3), consider hΣi=rk>1, simi=rk>1i and let α ∈ Σi such that α → β ∧ rank (β) < i − 1. By rank (β) < i − 1 and Lemma 4 we have βi−1 = β and S{δ | (β, δ) ∈ simi} = S{δ | (βi−1, δ) ∈ simi−1} = simβ. Hence, if rank (β) < (i − 1) − 1 we can conclude our thesis exploiting the inductive hypothesis for which S{δ | (αi−1, δ) ∈ simi−1} →∀ simβ. Otherwise, assume rank (β) = i − 1 and suppose by contradiction that ¬(S{δ | (α, δ) ∈ simi} →∀ simβ). Let α∗ ⊃ α be the superclass of α at the moment in which β gets selected at line 13 with rk = i − 1. Within the execution of the most internal foreach-loop at line 14, if α∗ contains some state that does not reach simβ, then α∗ gets split into the two subclasses: α1∗ := α∗ \ simβ and α∗ := α∗ \ α1. By α →∃ β ⊆ simβ, we have that the statement α ⊆ α∗ is true both before and after such a split. Moreover, the loop at line 19 processes each class γ ∈ simi∗−1(α∗ ⊇ α). If γ contains some state that does not reach simβ, then γ gets split into the two subclasses γ1 := γ \simβ and γ := γ \α1, and γ1 is removed from the simulators of α∗ ⊇ α (line 23). Hence, once β have been considered at line 13 within the i − 1-th execution of the for-loop at line 12, we have that each node belonging to a class simulating α∗ has a successor in simβ. Each subsequent refinement of α∗ or its set of simulators will maintain this property, and thus we get to the contradiction of our assumption ¬(S{δ | (α, δ) ∈ simi} →∀ simβ 2. We now proceed proving the inductive step for item (1). Let i = rk > 1 and consider the hΣi, simii. Let v ∈ V such that rank (v) < rk − 1. Then, item (1) holds by Lemma 4 and by inductive hypothesis. Let v such that rank (v) = rk − 1. Then, by inductive hypothesis on item (2) we have: Moreover, the inductive step already proved on item (3) ensures that: (α →∃ β ∧ rank (β) < rk − 1) ⇒ [{γ | (α, γ) ∈ sim} →∀ [{γ | (β, γ) ∈ sim} (1) (2) ⊔⊓ 4.2
Complexity We finally establish the complexity of our simulation algorithm on acyclic graphs. In particular, Theorem 2 shows that our procedure uses O(|E||V≡S |) time and requires Since rank (α) = rk − 1, any class reached by α has rank strictly lower than rk − 1. Hence, equations 1 and 2 guarantee that: [v]Σi = [v]Σi+1 ⊆ α by inductive hypothesis. If rank(v) = rk, there are two cases to consider. In the first case, [v]Σi = [v]Σi+1 (i.e. the class of v gets not split within the i-th iteration of the loop at line 13) and we are done. In the second case, [v]Σi gets split into α, α1 within the i-th execution of the loop at line 13. By contradiction, assume there exist two states u ∈ α, u′ ∈ α1 such that u ≡S u′. By definition of α, α1, u has a successor into a class β of rank r < rk, and u′ has no successor in any class β′ ∈ sim(β). By inductive hypothesis, this implies that there exists z such that (u, z) ∈ E and u′ has no successor z′ such that z ≤S z′, contradicting our hypothesis u ≡S u′.
O(|V≡S |2 + |V | log(|V≡S |)) bits to compute a simulation preorder on a given acyclic
labelled graph G = hV, E, Σi. Therefore, it has optimal performances w.r.t. both time
and space on acyclic graphs, outperforming [
Theorem 2. The algorithm SolveCPPP(G = hV, Ei, hΣ, Ii) performs O(|V≡S ||E|) steps and uses O(|V≡S |2 + |V | log(|V≡S |)) bits to compute the solution to the coarsest partition pair problem hV≡S , Si.
Proof. Let r = max{rank (v) | v ∈ V }. The cost of the while-loop at line 3 is O(r ∗ |E|) = O(|V≡S ||E|). at line 21, is:
The cost of the loop at line 12, excluded the execution of the innermost if-statement O(Σ1r=1Σβ∈V≡S ,rank (β)=i−1(|pre(β)| ∗ |Σi+1| + |pre([{δ | (β, δ) ∈ sim}|) = = O(|V≡S ||E|) and the classes in sim(γ), sim−1(γ).
In fact, consider a class β such that rank (β) = i − 1. It is possible to distinguish with marks the classes that reach (resp. do not reach/reach with all their nodes) the set S{δ | (β, δ) ∈ sim} at the cost O(pre(S{δ | (β, δ) ∈ sim}). Moreover, the same cost allows one to appropriately mark each node in pre(S{δ | (β, δ) ∈ sim}. Then, fixed β, rank (β) = i−1, the cost of executing lines 14–24 without considering the innermost if-statement, is O(|pre(S{δ | (β, δ) ∈ sim}| + Σα∈pre(β)|sim(α)|).
The innermost if-statement at lines 21–23 is executed only upon the creation of a new class γ1 and cost globally O(|V≡S ||E|). In fact, each execution of lines 21–23 for the creation of the new classes γ1, γ \ γ1 from γ, requires only to scan the nodes in γ
As far as space complexity is concerned we refer to bit complexity without
considering the space required by the graph G, since it is never modified (see, e.g., [
We presented an algorithm for computing the maximum simulation quotient and the
simulation preorder on acyclic graphs. Our algorithm is based on a characterization of
the simulation problem as coarsest partition pair problem and on the notion of rank. The
notion of rank is a standard one in well-founded set theory (see, e.g., [19]) and has been
exploited in [
On the one hand, its generalization to the general case is still an open problem. Unfortunately, when moving from acyclic to cyclic graphs the notion of simulation is not “compositional”, since loops allow to simulate paths of arbitrary length.
On the other hand, another open problem concerns the possibility of developing a linear time simulation algorithm for the acyclic case. Again, there seems to be an intrinsic higher complexity in the notion of simulation w.r.t. bisimulation which does not allow to reach the linear time complexity. In particular, while the notion of bisimulation on acyclic graphs corresponds to equality on well-founded sets, simulation in terms of set theory is a sort of recursive inclusion. 17. F. Ranzato and F. Topparo. A new efficient simulation equivalence algorithm. In Proceedings of Logics in Computer Science (LICS’07), pages 171–180, 2007. 18. F. Ranzato and F. Topparo. Saving space in a time efficient simulation algorithm. In Proceedings of Int. Conference on Application of Concurrency to System design (ACSD’09), pages 60–69, 2009. 19. J. E. Rubin. Set Theory for the Mathematician. New York: Holden-Day, 1967. 20. R. van Glabbeek and B. Ploeger. Correcting a space-efficien simulation algorithm. In Proceedings of Int. Conference on Computer Aided Verification (CAV’08), pages 517–529, 2008.