Computing crisp simulations for fuzzy labeled transition systems

Abstract

The problem of checking whether a state in a finite fuzzy labeled transition system (FLTS) crisply simulates another is one of the fundamental problems of the theory of FLTSs. This problem is of the same nature as computing the largest crisp simulation between two finite FLTSs. A naive approach to the latter problem is to crisp the given FLTSs and then apply one of the currently known best methods to the obtained crisp labeled transition systems. The complexity of the resulting algorithms is of order O (l (m + n) n), where l is the number of fuzzy values occurring in the specification of the input FLTSs, m is the number of transitions and n is the number of states of the input FLTSs. In the worst case, l can be m + n and O (l (m + n) n) is the same as O ((m + n) ²n). In this article, we design an efficient algorithm with the complexity O ((m + n) n) for computing the largest crisp simulation between two finite FLTSs. This gives a significant improvement. We also adapt our algorithm to computing the largest crisp simulation between two finite fuzzy automata.

Keywords

Fuzzy labeled transition systems fuzzy automata simulation bisimulation

1 Introduction

Bisimulations and simulations are used for characterizing similarity between states in automata, labeled transition systems and Kripke models. When applied to domains such as linked data networks or description logics, they can be used for characterizing similarity between objects or individuals.

Bisimulations have the following logical characterization in modal logic: modal formulas are invariant under bisimulations and, in image-finite Kripke models, two states are bisimilar (i.e., in the largest bisimulation relation) iff they cannot be distinguished by any modal formula (see, e.g., [1]). There are different variants of modal logic and different corresponding notions of bisimulation. Besides, the second assertion (called the Hennessy-Milner property) can be made stronger by replacing image-finiteness with modal saturatedness. The largest auto-bisimulation of a Kripke model is an equivalence relation.

Simulations require fewer conditions than bisimulations and characterize only the class of existential modal formulas, which are formulas in negation normal form without universal modal operators. Namely, they do not require the “backward” condition(s) of bisimulations; existential modal formulas are preserved under simulations and, in image-finite Kripke models, a state x′ simulates a state x iff x′ satisfies all existential modal formulas that x satisfies (see, e.g., [1]). The largest auto-simulation of a Kripke model is a pre-order.

Extending the notions of bisimulation and simulation for fuzzy labeled transition systems (FLTSs), we can consider crisp or fuzzy relations for them. Crisp bisimulations/simulations have been studied for FLTSs [3 , 27], weighted automata [25], fuzzy modal logics [8] and fuzzy description logics [15, 19]. Fuzzy bisimulations/simulations have been studied for fuzzy automata [5 , 13], FLTSs [18 , 24], weighted/fuzzy social networks [9, 11], fuzzy modal logics [8] and fuzzy description logics [19, 21]. As shown in [8, 19], the logical characterization of crisp bisimulations differs from the logical characterization of fuzzy bisimulations (in fuzzy modal/description logics under the Gödel semantics) in that it uses a logical language extended with involutive negation or the Baaz projection operator. A similar claim can be stated for the difference between crisp simulations and fuzzy simulations (see [18,20, 18,20]).

The objective of this article is to design an efficient algorithm for computing crisp simulations between finite FLTSs. The motivation is that, as far as we know, there were no algorithms directly formulated for computing the largest crisp simulation between two finite fuzzy graph-based structures (such as FLTSs, fuzzy automata, fuzzy Kripke models, and fuzzy interpretations in description logics).

1.1 Related work

The closest related works are discussed below.

• In [22] Paige and Tarjan gave an efficient algorithm with the complexity O ((m + n) log n) for computing the coarsest partition of a finite crisp graph, where n is the number of vertices and m is the number of edges of the graph. This problem is of the same nature as the problem of computing the largest auto-bisimulation of a finite crisp graph. Bloom and Paige [2] and Henzinger et al. [10] gave algorithms with the complexity O ((m + n) n) for computing the largest auto-simulation of a crisp labeled transition system or a crisp graph, respectively.

•Adapting the idea of the above mentioned algorithm of Henzinger et al. [10], in [14] we gave an algorithm with the complexity O ((m + n) n) for computing the largest directed auto-simulation of a finite crisp graph. Furthermore, in that paper we also gave algorithms with the complexity O((m + n)^2 n^2)for computing the largest auto-simulation and the largest directed auto-simulation of a finite crisp graph for the setting with counting successors.

• In [25] Stanimirović et al. gave algorithms with the complexity O (n³) for computing the greatest right/left invariant Boolean equivalence matrix of a weighted automaton over an additively idempotent semiring. Such matrices are closely related to crisp bisimulations. They also gave algorithms with the complexity O (n⁵) for computing the greatest right/left invariant Boolean quasi-order matrix of a weighted automaton over an additively idempotent semiring. Such matrices are closely related to crisp simulations.

• In [21] Nguyen and Tran gave algorithms with the complexity O ((m + n) n) for computing the greatest fuzzy bisimulation/simulation between two finite fuzzy interpretations in the fuzzy description logic fALC under the Gödel semantics, where n is the number of individuals and m is the number of nonzero instances of roles in the given fuzzy interpretations. They also adapted the algorithms to computing the greatest fuzzy bisimulation/simulation between fuzzy finite automata, as well as for dealing with other fuzzy description logics.

1.2 Our contribution and its significance

In this article, we design an efficient algorithm with the complexity O ((m + n) n) for computing the largest crisp simulation between two finite FLTSs, where n is the number of states and m is the number of transitions of the input FLTSs. Regarding the significance of our contribution, note the following.

• The problem of checking whether a state in a finite FLTS crisply simulates another is one of the fundamental problems of the theory of FLTSs. This problem is of the same nature as computing the largest crisp simulation between two finite FLTSs.

• As stated for the motivation, there were no algorithms directly formulated for computing the largest crisp simulation between two finite fuzzy graph-based structures. One can try to adapt the earlier mentioned algorithm with the complexity O (n⁵) by Stanimirović et al. [25] to computing the largest crisp simulations, but the complexity order O (n⁵) is too high. One can also crisp a given FLTS by treating a fuzzy transition 〈x, ϱ, y〉 with a degree d ∈ (0, 1] as the set of all crisp transitions 〈x, ϱ, d_i〉, y, where d_i ∈ (0, d] is any fuzzy value occurring in the specification of the input FLTS, and then apply one of the algorithms given in [2 , 14] to the obtained crisp labeled transition system. The complexity of the resulting algorithm is of order O (l (m + n) n), where l is the number of fuzzy values occurring in the specification of the input FLTS. In the worst case, l can be m + n and O (l (m + n) n) is the same as O ((m + n) ²n), which is still too high.

1.3 The structure of this article

The rest of this article is structured as follows. In Section 2, we recall FLTSs, define crisp simulations between FLTSs, and present some of their properties. In Section 3, we present our algorithm of computing the largest crisp simulation between two finite FLTSs, prove it correctness and analyze its complexity. In Section 4, we adapt that algorithm to computing the largest crisp simulation between two finite fuzzy automata. We conclude the article in Section 5. A preliminary version of this article is publicly shared as a preprint at [16].

2 Preliminaries

Let SE be a finite set of actions and SV a finite set of state labels. We use ϱ to denote an element of SE and p to denote an element of SV.

A fuzzy labeled transition system (FLTS) is a triple 𝒮 = 〈S, δ, L〉, where S is a non-empty set of states, δ : S × SE × S → [0, 1] is called the transition function, and L : S → (SV → [0, 1]) is called the state labeling function. For states x, y ∈ S, an action ϱ ∈ SE and a state label p ∈ SV, δ (x, ϱ, y) means the fuzzy degree of that there is a transition of ϱ from x to y, whereas L (x) (p) means the fuzzy degree of that p belongs to the label of x. An FLTS 𝒮 = 〈S, δ, L〉 is finite if S is finite and is image-finite if, for every x ∈ S and ϱ ∈ SE, the set {y ∣ δ (x, ϱ, y) >0} is finite.

Given f and g of type Σ_l to [0,1], we write f ≤ g to denote that f (p) ≤ g (p) for all p ∈ SV.

Let 𝒮 = 〈S, δ, L〉 and ^𝒮′ = 〈S′, δ′, L〉′ be FLTSs. A binary relation Z ⊆ S × S′ is called a (crisp) simulation between 𝒮 and ^𝒮′ [20] if the following two conditions hold (for all possible values of the free variables), where → and ∧ denote the usual crisp logical connectives: $Z (x, x^{'}) \to L (x) \leq L^{'} (x^{'})$ (1) $\begin{matrix} Z (x, x^{'}) \land δ (x, ϱ, y) > 0 \to y^{'} \in S^{'} ( \\ Z (y, y^{'}) \land δ (x, ϱ, y) \leq δ (x^{'}, ϱ, y^{'})) . \end{matrix}$ (2) To make it clear, as the connectives → and ∧ are crisp, the conditions mean that:

if Z (x, x′) holds, then L (x) ≤ L′ (x′);

if Z (x, x′) holds and δ (x, ϱ, y) >0, then there exists y′ ∈ S′ such that Z (y, y′) holds and δ (x, ϱ, y) ≤ δ (x′, ϱ, y′).

Remark 2.1.

We allow the empty binary relation to be a simulation between 𝒮 and ^𝒮′. This is for increasing simplicity in talking about the largest simulation between 𝒮 and ^𝒮′.

Some works in the literature on simulations (e.g., [10]) use the condition Z (x, x′) → L (x) = L′ (x′)

instead of Condition (1). Our choice of using(1) is as in [1] and does not reduce the generality, because one can choose SV₂, L₂ and $L_{2}^{'}$ so that L (x) = L′ (x′) over SV iff $L_{2} (x) \leq L_{2}^{'} (x^{'})$ over SV₂ for all 〈x, x′〉 ∈ S × S′.

Proposition 2.2. Let 𝒮, ^𝒮′ and ^𝒮″ be FLTSs and let 𝒮 = 〈S, δ, L〉.

The relation Z = {〈x, x〉 ∣ x ∈ S} is a simulation between 𝒮 and itself.

If Z₁ is a simulation between 𝒮 and ^𝒮′, and Z₂ is a simulation between ^𝒮′ and ^𝒮″, then Z₁ ∘ Z₂ is a simulation between 𝒮 and ^𝒮″.

If 𝒵 is a set of simulations between 𝒮 and ^𝒮′, then ⋃𝒵 is also a simulation between 𝒮 and ^𝒮′.

The proof of this proposition is straightforward.

The following corollary follows from the third assertion of Proposition 2.2.

Corollary 2.3. The largest simulation between two arbitrary FLTSs exists.

A (crisp) auto-simulation of 𝒮 is a simulation between 𝒮 and itself. The following corollary immediately follows from Proposition 2.2.

Corollary 2.4. The largest auto-simulation of a FLTS is a pre-order.

Example 2.5.Let SE = {ϱ}, SV = {p} and let 𝒮 and ^𝒮′ be the FLTSs specified below. They are illustrated in Fig. 1.

Fig. 1

An illustration for Example 2.5.

• 𝒮 = 〈S, δ, L〉, where S = {a, b, c, d}, L (a) (p) =0.8, L (b) (p) =0.8, L (c) (p) =0.7, L (d) (p) =0.9, δ (a, ϱ, b) =0.7, δ (b, ϱ, c) =0.6, δ (b, ϱ, d) =0.7, δ (c, ϱ, d) =0.5, δ (d, ϱ, b) =0.6 and δ (x, ϱ, y) =0 for the other triples 〈x, ϱ, y with x, y〉 ∈ S;

• ^𝒮′ = 〈S′, δ′, L′〉, where S′ = {e, f}, L′ (e) (p) =0.8, L′ (f) (p) =0.9, δ′ (e, ϱ, e) =0.6, δ′ (e, ϱ, f) =0.7, δ′ (f, ϱ, e) =0.6 and δ′ (x, ϱ, y) =0 for the other triples 〈x, ϱ, y〉 with x, y ∈ S′.

It can be checked that Z₀ = {〈b, e〉, 〈c, e〉, 〈d, f〉} is a simulation between 𝒮 and ^𝒮′. Let Z be the largest simulation between 𝒮 and ^𝒮′. We show that Z = Z₀ by justifying that ${〈 a, e 〉, 〈 a, f 〉, 〈 b, f 〉, 〈 c, f 〉, 〈 d, e 〉} \cap Z = \emptyset .$ Observe the following.

〈d, e〉 ∉ Z because L (d) ≰ L′ (e).

〈c, f〉 ∉ Z because (2) CS 2 cannot hold for 〈x, x′, y = 〉〉〈c, f, d〉 (since 〈d, e ∉ Z).

〈b, f〉 ∉ Z because (2) CS 2 cannot hold for 〈x, x′, y = 〈b, f, d.

〈a, e〉 ∉ Z because (2) CS 2 cannot hold for 〈x, x′, y = 〉〈a, e, b〉 (since 〈b, f ∉ Z).

〈a, f〉 ∉ Z because (2) CS 2 cannot hold for 〈x, x′, y = 〉〈a, f, b〉.

Therefore, {〈b, e〉, 〈c, e〉, 〈d, f〉} is the largest simulation between 𝒮 and ^𝒮′.

3 Computing simulations

In this section, we design an algorithm for computing the largest simulation between two given finite FLTSs 𝒮 = 〈S, δ, L〉 and ^𝒮′ = 〈S′, δ′, L〉′.

For ϱ ∈ SE, x, y ∈ S and x′, y′ ∈ S′, we denote $\begin{matrix} {Next}_{ϱ} (x) & = & {y \in S ∣ δ (x, ϱ, y) > 0} \\ {Next}_{'}^{ϱ} (x^{'}) & = & {y^{'} \in S^{'} ∣ δ^{'} (x^{'}, ϱ, y^{'}) > 0} \\ {Prev}_{ϱ} (y) & = & {x \in S ∣ δ (x, ϱ, y) > 0} \\ {Prev}_{'}^{ϱ} (y^{'}) & = & {x^{'} \in S^{'} ∣ δ^{'} (x^{'}, ϱ, y^{'}) > 0} . \end{matrix}$

3.1 The skeleton of the algorithm

We first formulate our algorithm on an abstract level without implementation details. The aim is to facilitate understanding the skeleton of the algorithm and its correctness. Implementation details and complexity analysis will be presented in the next subsection.

It can be checked that Condition (2) holds for all ϱ ∈ SE, x, y ∈ S and x′ ∈ S′ iff the following condition holds for all ϱ ∈ SE, y ∈ S and x′ ∈ S′, where the suprema are taken in the complete lattice [0,1].

$\begin{matrix} sup {δ (x, ϱ, y) ∣ x \in {Prev}_{ϱ} (y) \land 〈 x, x^{'} \in Z} \leq \\ sup {δ^{'} (x^{'}, ϱ, y^{'}) ∣ y^{'} \in {Next}_{'}^{ϱ} (x^{'}) \land 〈 y, y^{'} \in Z} \end{matrix}$ (3)

Fig. 2 is helpful for illustrating Condition(3). It is worth emphasizing that this condition is involved with 〈ϱ, y, x〉′. Thus, the diagonal 〈y, x〉′ in the figure forms the main axis. Our algorithm constructs the largest relation Z ⊆ S × S′ that satisfies Conditions (1) and (3) for all possible values of the free variables. The idea is to initialize Z by setting it to the largest subset of S × S′ that satisfies Condition (1) and then repeatedly refine Z by propagating necessary removals of pairs from Z. Using Fig. 1 for illustration, the propagation is done backward through the structures of the FLTSs 𝒮 and ^𝒮′ as follows: if the pair 〈y, y′ is deleted from Z, then to satisfy Condition (3), we may need to remove also the pair 〈x, x〉′ from Z, which in turn may trigger other removals. Our algorithm can be informally expressed as follows:

Initialize Z by setting it to the largest subset of S × S′ that satisfies Condition(1).

Initialize removeZ by setting it to the empty set. This variable stands for the set of pairs removed from Z and remained to be processed. So, Z ∪ removeZ plays the role of a subset of a previous value of Z.

For each 〈ϱ, y, x〉′ ∈ SE × S × S′, move all the pairs 〈x, x〉′ ∈ Z that falsify Condition(3) to the set removeZ. This can be restated as follows: for each 〈ϱ, y, x〉′ ∈ SE × S × S′ and x ∈ _Prevϱ (y), if 〈x, x〉′ ∈ Z but the following condition does not hold, then move 〈x, x〉′ from Z to removeZ. $\begin{matrix} δ (x, ϱ, y) \leq sup {δ^{'} (x^{'}, ϱ, y^{'}) ∣ \\ y_{'}^{\in} {Next}_{'}^{ϱ} (x^{'}) \land 〈 y, y^{'} \in Z} \end{matrix}$ (4)

While removeZ≠ ∅:

extract 〈y, y〉′ from removeZ;

for each ϱ ∈ SE, x′ ∈ _PrevPϱ (y′) and x ∈ _Prevϱ (y), if 〈x, x〉′ ∈ Z but the following condition does not hold, then move 〈x, x′ from Z to removeZ. $\begin{matrix} δ (x, ϱ, y) \leq sup {δ^{'} (x^{'}, ϱ, z^{'}) ∣ z_{'}^{\in} {Next}_{'}^{ϱ} (x^{'}) \\ \land 〈 y, z^{'} \in Z \cup removeZ} \end{matrix}$ (5)

Fig. 2

An illustration for the algorithms given in Section 3.

The steps 1-3 together form the initialization, whereas the step 4 is the main loop of the algorithm. The pseudocode is formulated as Algorithm 1 given below.

procedure proc:ProcessPrev ProcessPrev (ϱ, y, x′) // process _Prevϱ (y) with respect to 〈ϱ, y, x〉′

d : = sup {δ′ (x′, ϱ, y′) ∣ y′ ∈ _NextPϱ (x′) and 〈y, y〉′ ∈ Z ∪ removeZ;

x ∈ _Prevϱ (y):

If δ (x, ϱ, y) > d and 〈x, x〉′ ∈ Z:

move 〈x, x〉′ from Z to removeZ;

Algorithm 1 ComputeSimulation Input finite FLTSs 𝒮 = 〈S, δ, L〉, S′, δ′, L′. Output the largest simulation between 𝒮 and ^𝒮′.

Z : = {〈x, x〉′ ∈ S × S′ ∣ L (x) ≤ L′ (x′)};

removeZ : =∅;

ForEach 〈ϱ, y, x〉′ ∈ SE × S × S′:

ProcessPrev (ϱ, y, x′);

While removeZ≠ ∅:

extract 〈y, y〉′ from removeZ;

ForEach ϱ ∈ SE and x′ ∈ _PrevPϱ (y′):

ProcessPrev (ϱ, y, x′);

Return Z;

Example 3.1. Let SE = {ϱ}, SV = {p} and let 𝒮 and ^𝒮′ be the FLTSs specified in Example 2.5. Consider the execution of Algorithm 1 for 𝒮 and ^𝒮′.

• After executing the statement statement 2, we have that Z = ({a, b, c} × {e, f}) ∪ {〈d, f} and removeZ =∅. •.

• Executing the “foreach” loop specified by the statements 3 and 4, for the iteration involved with 〈ϱ, y, x′,

if 〈ϱ, y, x〉′ ∈ {〈ϱ, a, e〉, 〈ϱ, a, f〉, 〈ϱ, b, e〉}, then no changes are made,

if 〈ϱ, y, x〉′ = 〈ϱ, b, f, then 〈a, f is moved from Z to removeZ,

if 〈ϱ, y, x〉′ ∈ {〈ϱ, c, e〉, 〈ϱ, c, f〉, 〈ϱ, d, e〉}, then no changes are made,

if 〈ϱ, y, x〉′ = 〈ϱ, d, f〉, then 〈b, f〉 and 〈c, f〉 are moved from Z to removeZ.

Consider, for example, the case 〈ϱ, y, x〉′ = 〈ϱ, b, f〉〉 and the execution of ProcessPrev (ϱ, y, x′). After executing the first statement of this procedure we have d = δ′ (f, ϱ, e) =0.6. Since _Prevϱ (b) = {a, d}, δ (a, ϱ, b) =0.7 > d, 〈a, f〉 ∈ Z and δ (d, ϱ, b) =0.6notgreaterthand, the execution of the “foreach” loop of ProcessPrev (ϱ, y, x′) moves only 〈a, f〉 from Z to removeZ.

• Before executing the statement 5, we have that $\begin{matrix} Z & = & ({a, b, c} \times {e}) \cup {〈 d, f} \\ removeZ & = & {〈 a, f 〉, 〈 b, f 〉, 〈 c, f 〉} . \end{matrix}$

• Executing the “while” loop, for the iteration involved with 〈y, y〉′ which is extracted from removeZ,

if 〈y, y〉′ = 〈a, f〉, then no additional changes are made,

if 〈y, y〉′ = 〈b, f〉, then 〈a, e〉 is moved from Z to removeZ,

if 〈y, y〉′ ∈ {〈c, f〉, 〈a, e〉}, then no additional changes are made.

• The algorithm returns Z = {〈b, e, 〈c, e, 〈d, f}. This coincides with the claim of Example 2.5 that this relation is the largest simulation between 𝒮 and ^𝒮′.

Lemma 3.2. The following assertions are invariants of the “while” loop of Algorithm 1:

The largest simulation between 𝒮 and ^𝒮′ is a subset of Z.

For all 〈ϱ, y, x〉′ ∈ SE × S × S′, if x ∈ _Prevϱ (y) and Z [x, x′] holds, then (5) holds.

Proof. Let Z₀ be the largest simulation between 𝒮 and ^𝒮′. It must satisfy Condition (3), i.e.,

$\begin{matrix} sup {δ (x, ϱ, y) ∣ x \in {Prev}_{ϱ} (y) \land 〈 x, x^{'} \in Z_{0}} \leq \\ sup {δ^{'} (x^{'}, ϱ, y^{'}) ∣ y^{'} \in {Next}_{'}^{ϱ} (x^{'}) \land 〈 y, y^{'} \in Z_{0}} . \end{matrix}$ (6) The first assertion is an invariant of the loop because it holds after the initialization (i.e., after executing the statement 1) and the removal of any pair from Z at a later step is justifiable by using (6) and the induction assumption (which means that after such a removal it still holds that Z₀ ⊆ Z). It is straightforward to check that the second assertion is also an invariant of the “while” loop of Algorithm 1.

Theorem 3.3. HDKAL Algorithm 1 always terminates and returns the largest simulation between the input FLTSs.

Proof. After the initialization at the statement 1, no pairs are added to Z. The pairs added to removeZ are the ones extracted from Z. Hence, the total number of pairs added to removeZ is bounded. Each iteration of the “while” loop of Algorithm 1 extracts one pair from removeZ. Hence, the loop and the algorithm itself always terminate. At the end, we have that removeZ =∅. Hence, by the second assertion of Lemma 3.2, the resulting Z satisfies Condition(3) (for all possible values of the free variables). Due to the initialization, it also satisfies Condition(1). Thus, it is a simulation between 𝒮 and ^𝒮′. By the first assertion of Lemma 3.2, it follows that the returned Z is the largest simulation between 𝒮 and ^𝒮′.

3.2 Implementation details and complexity analysis

By |δ| we denote | {〈x, ϱ, y ∈ S × SE × S : δ (x, ϱ, y) >0} |, and similarly for |δ′|. Let n = |S| + |S′| and m = |δ| + |δ′|. Assume that |SE| and |SV| are constants. In this subsection, we give details on how to implement Algorithm 1 so that its complexity is of order O ((m + n) n). In particular, we provide an improved algorithm together with a complexity analysis.

For simplicity, without loss of generality we assume that S = 0 . . (|S|-1), S′ = 0 . . (|S′|-1) and SE = 0 . . (|SE|-1). In practice, the input data for 𝒮 and ^𝒮′ can be given in a friendly format using names for states and actions, but the conversion (using maps) for the input as well as for the output can be done in time O ((m + n) log n), which is within O ((m + n) n). From the input data we construct arrays NextP, Prev, PrevP, T and T′ such that, for ϱ ∈ SE, x, y ∈ S and x′, y′ ∈ S′, NextP [ϱ, x′] is a vector representing _NextPϱ (x′), T [x, ϱ, y] = δ (x, ϱ, y), and similarly for Prev [ϱ, y], PrevP [ϱ, y′] and T′ [x′, ϱ, y′]. The construction can be done in time O (n²). Note that T stands for δ, whereas T′ stands for δ′.

We use an array TransID^′ : S′ × SE × S′ → 0 . . (|δ′|-1) for identifying transitions of ^𝒮′ so that, if $〈 x_{1}^{'}, r_{1}, y_{1}^{'}$ and $〈 x_{2}^{'}, r_{2}, y_{2}^{'}$ are different triples from S′ × SE × S′ such that $T^{'} [x_{1}^{'}, r_{1}, y_{1}^{'}] > 0$ and $T^{'} [x_{2}^{'}, r_{2}, y_{2}^{'}] > 0$ , then ${TransID}^{'} [x_{1}^{'}, r_{1}, y_{1}^{'}] \neq {TransID}^{'} [x_{2}^{'}, r_{2}, y_{2}^{'}]$ . Such an array can be constructed in time O (n² + m log m). After having been constructed, TransID^′ will never change.

For the improved algorithm, we implement Z as an array of type S × S′ → Bool and removeZ as a queue. We also use the variables rcNextP, rcNextElemP and rcPrev for representing the arrays described below:

• rcNext^′ is an array such that, for 〈ϱ, y, x〉′ ∈ SE × S × S′, rcNextP [ϱ, y, x′] is a doubly linked list consisting of the states y′ ∈ _NextPϱ (x′) such that Z [y, y′] lor (〈y, y〉′ ∈ removeZ) holds. The list is sorted in ascending order with respect to T′ [x′, ϱ, y′]. The prefix “rc” stands for “remaining for consideration”. The state contained in an element of rcNextP [ϱ, y, x′] is called the key of that element.

• rcNextElem^′ is an array with indices from S × (0 . . (|δ′|-1)) such that, if Z [y, y′] lor (〈y, y′ ∈ removeZ), ϱ ∈ SE, x′ ∈ _PrevPϱ (y′) and e′ = TransID^′ [x′, ϱ, y′], then rcNextElemP [y, e′] is (a reference to) the element of the doubly linked list rcNextP [ϱ, y, x′] whose key is y′.

• rcPrev is an array such that, for 〈ϱ, y, x〉′ ∈ SE × S × S′, rcPrev [ϱ, y, x′] is a vector consisting of the states x ∈ _Prevϱ (y) such that the following condition (which is a reformulation of(5)) holds

$\begin{matrix} T [x, ϱ, y] \leq sup {T^{'} [x^{'}, ϱ, y^{'}] ∣ y^{'} \in {Next}_{'}^{ϱ} (x^{'}) \land \\ (Z [y, y^{'}] (〈 y, y^{'} \in removeZ))} \end{matrix}$ (7) and the vector is sorted in ascending order with respect to T [x, ϱ, y].

Algorithm 2 given below is a reformulation of Algorithm 1 using the above described data structures. It is given together with its subroutines Initialize and UpdateRcPrev (for updating rcPrev). The procedure UpdateRcPrev corresponds to the procedure ProcessPrev used in Algorithm 1.

Algorithm 2 ComputeSimulationEfficiently Input finite FLTSs 𝒮 = 〈S, δ, L〉, 〈S′, δS′, δ′, L〉′Output the largest simulation between 𝒮 and ^𝒮′.

Initialize ();

while removed Z tp is not empty:

extract 〈y, y〉′ from removeZ_tp;

ForEach ϱ ∈ SE and x′ ∈ PrevP [ϱ, y′];

e′ : = EdgeIDp [x′, ϱ, y′]

u : = rcNextElemP [y, e′];

delete u from rcNextP [ϱ, y, x′];

rcNextElemP [y, e′] : = Null;

UpdateRcPrev (ϱ, y, x′);

Return the relation corresponding to Z;

procedure Initialize ()

construct arrays NextP, Prev, PrevP, T, T′ and TransID^′ according to their specifications;

ForEach 〈x, x〉′ ∈ S × S′:

Z [x, x′] : = L (x) ≤ L′ (x′);

set removeZ to the empty queue;

ForEach 〈ϱ, x〉′ ∈ SE × S′:

sort NextP [ϱ, x′] in ascending order w.r.t.wcc T′ [x′, ϱ, y′] for y′ ∈ NextP [ϱ, x′];

ForEach 〈ϱ, y〉 ∈ SE × S:

sort Prev [ϱ, y] in ascending order w.r.t. T [x, ϱ, y] for x ∈ Prev [ϱ, y];

ForEach y ∈ S and e′ ∈ 0 . . (|δ′|-1):

rcNextElemP [y, e′] : = Null;

ForEach 〈ϱ, y, x〉′ ∈ SE × S × S′:

construct a vector rcPrev [ϱ, y, x′] of all x ∈ Prev [ϱ, y] such that Z [x, x′] holds, preserving the order;

construct a doubly linked list rcNextP [ϱ, y, x′] whose elements’ keys are all y′ ∈ NextP [ϱ, x′] such that Z [y, y′] holds, preserving the order;

ForEach element u of rcNextP [ϱ, y, x′]:

let y′ be the key of u;

let e′ = TransID^′ [x′, ϱ, y′];

rcNextElemP [y, e′] : = u

ForEach 〈ϱ, y, x〉′ ∈ SE × S × S′:

UpdateRcPrev (ϱ, y, x′)

procedure :UpdateRcPrev UpdateRcPrev (ϱ, y, x′) for updating rcPrev

If rcNextP [ϱ, y, x′] is empty:

d:= 0;

else:

let y′ be the key of the last element of rcNextP [ϱ, y, x′];

d : = T′ [x′, ϱ, y′]

while rcPrev [ϱ, y, x′] is not empty

let x be the last element of rcPrev [ϱ, y, x′]

if T [x, ϱ, y] ≤ d:

break;

delete from rcPrev [ϱ, y, x′] the last element;

If Z [x, x′]:

Z [x, x′] : = false;

add 〈x, x′〉 to removed_Z_tp;

Roughly speaking, the reformulation relies on the following two points:

• Computing d specified by the statement 1 of the procedure ProcessPrev (ϱ, y, x′) used in Algorithm 1 is implemented in Algorithm 2 by the statements 1-5 of the procedure UpdateRcPrev (ϱ, y, x′) so that its cost is bounded by a constant. It is done by using the sorted list rcNextP [ϱ, y, x′]. This list is doubly linked so that deleting any element from the list can be done in constant time. Such a deletion is triggered when a pair 〈y, y′ is extracted from removeZ by the statement 3 of Algorithm 2. In such a situation, to guarantee that rcNextP satisfies its specification, we need to delete the element u whose key is y′ from the list rcNextP [ϱ, y, x′]. A reference to u is kept in rcNextElemP [y, e′], where e′ = TransID^′ [x′, ϱ, y′]. The deletion is done by the statements 5-8 of Algorithm 2. This shows the key role of the arrays rcNextP, rcNextElemP and TransID^′.

• When dealing with a triple 〈ϱ, y, x′ ∈ SE × S × S′, moving pairs 〈x, x′ from Z to removeZ as done in the loop specified by the statements 2-4 of the procedure ProcessPrev (ϱ, y, x′) (used in Algorithm 1) is implemented in Algorithm 2 by the 6-13 of the procedure UpdateRcPrev (ϱ, y, x′). Once again, the task is realized by using a sorted collection (rcPrev [ϱ, y, x′]). The cost related to each x ∈ _Prevϱ (y) of the task is bounded by a constant. This is the point of the use of the array rcPrev.

We have implemented Algorithm 2 in C++ and shared the code [17]. The reader can experiment with the algorithm by adding statements to the code for displaying the data he or she wants to watch.

Lemma 3.4. The following assertions are invariants of the “while” loop of Algorithm 2:

The data structures rcNextP, rcNextElemP and rcPrev satisfy their specifications.

The largest simulation between 𝒮 and ^𝒮′ is a subset of {〈x, x〉′ ∈ S × S′ ∣ Z [x, x′]}.

For all 〈ϱ, y, x〉′ ∈ SE × S × S′, if x ∈ _Prevϱ (y) and Z [x, x′] holds, then x ∈ rcPrev [ϱ, y, x′].

Proof. It is easy to check that the first assertion is an invariant of the “while” loop of Algorithm 2.

Consider the second assertion and let Z₀ be the largest simulation between 𝒮 and ^𝒮′. Recall that Z₀ satisfies (6). We prove that Z₀ ⊆ {〈x, x〉′ ∈ S × S′ ∣ Z [x, x′]} by induction on the step number during the execution of Algorithm 2. The base case occurs after the initialization of Z by the statement 2 of the procedure Initialize. The induction hypothesis clearly holds for the base case. For the induction step, assume that the induction hypothesis holds before calling the procedure UpdateRcPrev (ϱ, y, x′). We only need to prove that it still holds after executing that procedure. Let d be the value computed by the statements 1-5 of UpdateRcPrev (ϱ, y, x′). By the first invariant, we have that d = sup {δ′ (x′, ϱ, y′) ∣ y′ ∈ _NextPϱ (x′) ∧ (Z [y, y′] lor (〈y, y′ ∈ removeZ))} . By the induction assumption, Z₀ ⊆ {〈x, x′ ∈ S × S′ ∣ Z [x, x′]}. Hence, d ≥ sup {δ′ (x′, ϱ, y′) ∣ y′ ∈ _NextPϱ (x′) ∧ 〈y, y〉′ ∈ Z₀} . By (6), it follows that d ≥ sup {δ (x, ϱ, y) ∣ x ∈ _Prevϱ (y) ∧ 〈x, x〉′ ∈ Z₀} . Therefore, after executing the statements 6-13 of UpdateRcPrev (ϱ, y, x′), it still holds that Z₀ ⊆ {〈x, x〉′ ∈ S × S′ ∣ Z [x, x′]}. This completes the proof of that the second assertion is an invariant of the “while” loop of Algorithm 2.

The third assertion is also an invariant of the loop because it holds after executing the statements 1-17 of the procedure Initialize and, whenever x is deleted from rcPrev [ϱ, y, x′], Z [x, x′] is set to false.

We give below the main theorem of this section.

Theorem 3.5. Algorithm 2 runs in time O ((m + n) n) and returns the largest simulation between the finite FLTSs 𝒮 = 〈S, δ, L and ^𝒮′ = 〈S′, δ′, L〉′, where n = |S| + |S′| and m = |δ| + |δ′|.

Proof. First, consider the complexity of the procedure Initialize.

• As mentioned earlier, constructing the arrays NextP, Prev, PrevP, T and T′ can be done in time O (n²), whereas constructing the array TransID^′ can be done in time O (n² + m log m). Hence, the statement 1 (of the procedure) runs in time O (n² + m log m).

• The statement 2 runs in time O (n²).

• The statement 4 runs in constant time.

• The loops specified by the statements 5-8 run in time O (n + m log m). • The loop specified by the statement 9 runs in time O (nm).

• The loop specified by the statements 11-17 runs in time O (n (n + m)).

• The loop specified by the statements 18 and 19 runs in time O (n (n + m)).

Summing up, the procedure Initialize runs in time O ((m + n) n). Now consider the complexity of the “while” loop of Algorithm 2.

• The statements 3 and 5-8 of Algorithm 2 as well as the statements 1-5 and 7-13 of the procedure UpdateRcPrev (ϱ, y, x′) run in constant time. • Each iteration of the “foreach” loop of Algorithm 2 is involved with a pair 〈y, y〉′ extracted from removeZ and a state x′ ∈ _PrevPϱ (y′).

• Each iteration of the “while” loop of the procedure UpdateRcPrev (ϱ, y, x′) is involved with the triple 〈ϱ, y, x〉′ ∈ SE × S × S′ and a state x ∈ _Prevϱ (y). If x is deleted from rcPrev [ϱ, y, x′], then we ascribe the cost of the involved iteration to the transition 〈x, ϱ, y and x′. Otherwise, the involved iteration is the last one of the loop and we ascribe its cost to the pair 〈y, y〉′ and x′ ∈ _PrevPϱ (y′) which together identify the iteration of the “foreach” loop of Algorithm 2 that calls UpdateRcPrev (ϱ, y, x′). Thus, the “while” loop of Algorithm 2 runs in time O ((m + n) n). The “return” statement of Algorithm 2 runs in time O (n²). Summing up, Algorithm 2 runs in time O ((m + n) n).

At the end of the execution of Algorithm 2, removeZ is empty. Let Z_f = {〈x, x〉′∈ S × S′ ∣ Z [x, x′]} be the relation returned by Algorithm 2. For simplicity, in the rest of this proof, by writing Z we refer to Z_f. By the third and first assertions of Lemma 3.4, it follows that Z satisfies Condition (3) (pay attention to rcPrev and (7)). By the initialization, Z also satisfies Condition Hence, Z is a simulation between 𝒮 and ^𝒮′. Together with the second assertion of Lemma 3.4, this implies that Z is the largest simulation between 𝒮 and ^𝒮′.

3.3 Performance tests

We have conducted performance tests for our implementation of Algorithm 2 [17]. The tests were done on a laptop with Intel^® Core^TM i3-3120M CPU @ 2.50GHz×4 and 4 GB RAM. The settings for SV, SE and input FLTSs 𝒮 = 〈S, δ, L〉 and ^𝒮′ = 〈S′, δ′, L〉′ are as follows:

〈|SV|, |SE|〉 is 〈1, 1〉, 〈1, 5〉 or 〈5, 5〉;

|S| = |S′| = n/2, n ∈ {50, 100, 150, …, 500};

|δ| ≃ |δ′| and m = |δ| + |δ′| is approximately equal to one of the following values:

|SE| · n,

|SE| · n · log(n/2),

|SE| · n²/4;

δ and δ′ are randomly generated so that:

the sets {y ∈ S ∣ δ (x, ϱ, y) >0} and {y′ ∈ S′ ∣ δ′ (x′, ϱ, y′) >0}, for ϱ ∈ SE, x ∈ S and x′ ∈ S′, have approximately equal sizes;

the multisets {δ (x, ϱ, y)∣ y ∈ S, δ (x, ϱ, y) >0} and {δ′ (x′, ϱ, y′)∣ y′ ∈ S′, δ′ (x′, ϱ, y′) >0}, for ϱ ∈ SE, x ∈ S and x′ ∈ S′, have uniform distributions;

L and L′ are randomly generated.

Plots about the time needed for performing the tests are displayed in Fig. 3.

Fig. 3

Results of the performance tests specified in Section 3.3. Each of the subplots displays the time consumed for the tests specified by the given parameters Sl = |SV|, Sa = |SE| and D (density), where D = 1 means m = |SE| · n, D = 2 means m = |SE| · n · log(n/2) and D = 3 means m = |SE| · n²/4. The parameter n is plotted along the horizontal axis, whereas the time (ms) consumed for the corresponding test is plotted along the vertical axis.

As stated earlier, before the current work there were no algorithms directly formulated for computing the largest crisp simulation between two finite fuzzy graph-based structures. One can try to adapt the algorithm with the complexity O (n⁵) by Stanimirović et al. [25] to computing the largest crisp simulations, but the complexity order O (n⁵) is too high. One can also crisp a given FLTS as described in Section 1.2 and then apply one of the algorithms given in [2 , 14] to the obtained crisp labeled transition system. The complexity of the resulting algorithm is of order O ((m + n) ²n). For m = n² - n, this latter complexity order is the same as O (n⁵). The difference between O (n⁵) (respectively, O ((m + n) ²n)) and O ((m + n) n) is huge and clear, like comparing 100⁵ = 10 000 000 000 with 100³ = 1000 000 for the case n = 100. There is no chance for performing a program with the complexity Θ (n⁵) for n = 500 on the laptop mentioned in this subsection, whereas our algorithm has been tested on that laptop and ran in less than 8 seconds for such cases. 1

4 Adapting to fuzzy automata

In this section, we adapt Algorithm 2 to computing the largest crisp simulation between two finite fuzzy automata.

A fuzzy automaton over a (finite) alphabet Σ is a 〈 A = 〈Q, δ, σ, τ〉, where Q is a non-empty set of states, δ : Q × Σ × Q → [0, 1] is called the fuzzy transition function, σ : Q → [0, 1] the fuzzy set of initial states, and τ : Q → [0, 1] the fuzzy set of terminal states (cf. [5]). It is finite if Q is finite.

Let A = 〈Q, δ, σ, τ and A′ = 〈Q′, δ′, σ′, τ′ be fuzzy automata over an alphabet Σ. A relation Z ⊆ Q × Q′ is a (crisp) simulation between A and A′ if the following conditions hold (for all possible values of the free variables), where → and ∧ denote the usual crisp logical connectives: $\begin{matrix} σ (x) > 0 \to \\ E x^{'} \in Q^{'} (Z (x, x^{'}) \land σ (x) < σ^{'} (x^{'})) \end{matrix}$ (8) $\begin{matrix} Z (x, x^{'}) \land δ (x, σ, y) > 0 \to E y^{'} \in Q^{'} \\ (Z (y, y^{'}) \land δ (x, σ, y) < δ^{'} (x^{'}, σ, y^{'})) \end{matrix}$ (9) $Z (x, x^{'}) \land τ (x) > 0 \to τ (x) < τ^{'} (x^{'}) .$ (10)

The above definition of crisp simulations between fuzzy automata is an adaptation of the definition of “forward (fuzzy) simulation” between fuzzy automata introduced by Ćirić et al. in [5].

Given a fuzzy automaton A = 〈Q, δ, σ, τ〉 over an alphabet Σ, we define the FLTS corresponding to A to be the FLTS 𝒮 = 〈S, δ₂〉, L using SE = Σ and SV = {i, f} such that:

• S = Q ∪ {s_i, s_f}, where s_i and s_f are new states, with s_i standing for the new unique initial state, and s_f the new unique final state; • L (s_i) (i) = L (s_f) (f) =1, L (s_i) (f) = L (s_f) (i) =0, and L (x) (i) = L (x) (f) =0 for x ∈ Q (thus, i ∈ SV is used to identify s_i and f ∈ SV is used to identify s_f); • for every ϱ ∈ SE, x, y ∈ Q and z ∈ S:

δ₂ (x, ϱ, y) = δ (x, ϱ, y),

δ₂ (s_i, ϱ, x) = σ (x) and δ₂ (x, ϱ, s_f) = τ (x),

δ₂ (z, ϱ, s_i) = δ₂ (s_f, ϱ, z) = δ₂ (s_i, ϱ, s_f) =0.

The above definition is a counterpart of the definition of the fuzzy interpretation (in description logic) corresponding to a fuzzy automaton [21]. The following lemma can be proved in a straightforward way.

Lemma 4.1. Let A = 〈Q, δ, σ〉, τ and A′ = 〈Q′, δ′, σ′, τ′〉 be fuzzy automata over the same alphabet. Let 𝒮 = 〈S, δ₂, L〉 and $S^{'} = 〈 S^{'}, δ_{2}^{'}, L^{'} 〉$ be the FLTSs corresponding to A and A′, respectively. Let s_i, s_f ∈ S and $s_{i}^{'}, s_{f}^{'} \in S^{'}$ be the states such that $L (s_{i}) (i) = L (s_{f}) (f) = L^{'} (s_{i}^{'}) (i) = L^{'} (s_{f}^{'}) (f) = 1$ . If Z ⊆ Q × Q′, then Z is a simulation between A and A′ iff $Z \cup {〈 s_{i}, s_{i}^{'}, 〈 s_{f}, s_{f}^{'} 〉}$ is a simulation between 𝒮 and ^𝒮′.

Let Algorithm 2’ be the algorithm that, given finite fuzzy automata A = 〈Q, δ, σ, τ〉 and A′ = 〈Q′, δ′, σ′, τ′〉 over the same alphabet Σ, computes the largest simulation between A and A′ as follows:

construct the FLTS 𝒮 = 〈S, δ₂, L〉 that corresponds to A and let s_i, s_f ∈ S be the added states (with L (s_i) (i) = L (s_f) (f) =1);

construct the FLTS $𝒮^{'} = 〈 S^{'}, δ_{2}^{'}, L^{'} 〉$ that corresponds to A′ and let $s_{i}^{'}, s_{f}^{'} \in S^{'}$ be the added states (with $L^{'} (s_{i}^{'}) (i) = L^{'} (s_{f}^{'}) (f) = 1$ );

run Algorithm 2 to compute the largest simulation Z between 𝒮 and ^𝒮′;

return $Z - {〈 s_{i}, s_{i}^{'}, 〈 s_{f}, s_{f}^{'} 〉}$ .

Theorem 4.2. Algorithm 2’ returns the largest simulation between the given finite fuzzy automata A = 〈Q, δ, σ, τ〉 and A′ = 〈Q′, δ′, σ′, τ′〉, which are over the same alphabet Σ. Its complexity is of order O ((m + n) n), where n = |Q| + |Q′| and m = |δ| + |δ′|, with $\begin{matrix} | δ | & = & | {〈 x, ϱ, y \in Q \times Σ \times Q : δ (x, ϱ, y) > 0} | \\ | δ^{'} | & = & | {〈 x^{'}, ϱ, y^{'} \in Q^{'} \times Σ \times Q^{'} : δ (x^{'}, ϱ, y^{'}) > 0} | . \end{matrix}$

This theorem follows immediately from Lemma 4.1 and Theorem 3.5 and the fact that the first two steps of the algorithm (for constructing 𝒮 and ^𝒮′) can be done in time O (m + n).

5 Concluding remarks

As far as we know, before the current work there were no algorithms directly formulated for computing the largest crisp simulation between two finite fuzzy graph-based structures (such as FLTSs, fuzzy automata, fuzzy Kripke models, and fuzzy interpretations in description logics). One can try to adapt the algorithm with the complexity O (n⁵) of computing the greatest right/left invariant Boolean quasi-order matrix of a weighted automaton over an additively idempotent semiring, given by Stanimirović et al. in [25], to obtain an algorithm for that task. However, the complexity order O (n⁵) is too high. Crisping a given finite fuzzy graph and then applying one of the algorithms given in [2 , 14] to the obtained crisp graph also results in an algorithm with the high complexity order O (l (m + n) n), where l is the number of fuzzy values occurring in the specification of the input graph and, in the worst case, can be m + n.

In this article, we have given an efficient algorithm with the complexity O ((m + n) n) for computing the largest crisp simulation between two finite FLTSs, where n is the number of states and m is the number of transitions of the input FLTSs. We have also adapted it to computing the largest crisp simulation between two finite fuzzy automata.

In the preprint [16], we extended and adapted Algorithm 2 (ComputeSimulationEfficiently ) to obtain an efficient algorithm, named ComputeDirectedSimulationEfficiently , with the complexity O ((m + n) n) for computing the largest crisp directed simulation between two finite fuzzy labeled graphs. The notion of directed simulation was introduced by Kurtonina and de Rijke [12] for modal logic. It was later formulated and studied by Divroodi and Nguyen [7] for description logics. Directed simulations are similar to bisimulations in that they use both the “forward” and “backward” conditions. The difference is that, if a state x is directedly simulated by a state x′, then the label of x is only required to be a subset of the label of x′, whereas two states in a bisimulation relation must have the same label. Directed simulations characterize the class of positive modal formulas [12]. That is, positive modal formulas are preserved under directed simulations and, in image-finite Kripke models, a state x′ directedly simulates a state x iff x′ satisfies all positive modal formulas that x satisfies. The largest directed auto-simulation of a Kripke model is a pre-order. The notion of fuzzy labeled graphs used in [16] covers FLTSs, fuzzy Kripke models and fuzzy interpretations in description logic. Fuzzy automata are also a special case of fuzzy labeled graphs. Due to the lack of space, the additional results of [16] are not included in the current article.

We have implemented both the algorithms ComputeSimulationEfficiently and ComputeDirectedSimulationEfficiently in C++. The source code together with test results is available online [17].

Footnotes

Acknowledgment

The author would like to thank the reviewers for useful comments.

Counting from 1 to 500⁵ in Python using the mentioned laptop would take about 10 days.

References

Blackburn

, de Rijke

and Venema

Modal Logic. Number 53 in Cambridge Tracts in Theoretical Computer Science, Cambridge University Press (2001).

Bloom

and Paige

, Transformational design and implementation of a new efficient solution to the ready simulation problem, Sci Comput Program 24(3) (1995), 189–220.

Cao

, Chen

and Kerre

E.E.

, Bisimulations for fuzzytransition systems, IEEE Trans Fuzzy Systems 19(3) (2011), 540–552.

Cao

, Sun

S.X.

, Wang

and Chen

, A behavioral distance for fuzzy-transition systems, IEEE Trans Fuzzy Systems 21(4) (2013), 735–747.

Ćirić

, Ignjatović

, Damljanović

and Basic

, Bisimulations for fuzzy automata, Fuzzy Sets and Systems 186(1) (2012), 100–139.

Ćirić

, Ignjatović

, Jancić

and Damljanović

, Computation of the greatest simulations and bisimulations between fuzzy automata, Fuzzy Sets and Systems 208 (2012), 22–42.

Divroodi

A.R.

and Nguyen

L.A.

, On directed simulations in description logics, J Log Comput 27(7) (2017), 1955–1986.

Fan

T.-F.

, Fuzzy bisimulation for Gödel modal logic, IEEE Trans. Fuzzy Systems 23(6) (2015), 2387–2396.

Fan

T.-F.

and Liau

C.-J.

, Logical characterizations of regular equivalence in weighted social networks, Artif Intell 214 (2014), 66–88.

10.

Henzinger

M.R.

, Henzinger

T.A.

and Kopke

P.W.

, Computing simulations on finite and infinite graphs, In Proceedings of FOCS’1995, pages 453–462. IEEE Computer Society, (1995).

11.

Ignjatović

, Ćirić

and Stanković

, Bisimulations in fuzzy social network analysis, In Proceedings of IFSA EUSFLAT-15. Atlantis Press, (2015).

12.

Kurtonina

and de Rijke

, , Simulating without negation, J Log Comput 7(4) (1997), 501–522.

13.

Micić

, Jančić

and Stanimirović

, Computation of the greatest right and left invariant fuzzy quasi-orders and fuzzy equivalences, Fuzzy Sets and Systems 339 (2018), 99–118.

14.

Nguyen

L.A.

, Computing bisimulation-based comparisons, Fundam Inform 157(4) (2018), 385–401.

15.

Nguyen

L.A.

, Bisimilarity in fuzzy description logics under the Zadeh semantics, IEEE Trans Fuzzy Systems 27(6) (2019), 1151–1161.

16.

Nguyen

L.A.

, Computing crisp simulations and crisp directed simulations for fuzzy graph-based structures, CoRR, abs/2012.01845, (2020).

17.

Nguyen

L.A.

, An implementation of the agorithm given in the current work, Available at https://www.mimuw.edu.pl/~nguyen/compCSfFS, (2020).

18.

Nguyen

L.A.

, Characterizing fuzzy simulations for fuzzy labeled transition systems in fuzzy propositional dynamic logic, Int J Approx Reason 135 (2021), 21–37.

19.

Nguyen

L.A.

, Ha

Q.-T.

, Nguyen

N.T.

, Nguyen

T.H.K.

and Tran

T.-L.

, Bisimulation and bisimilarity for fuzzy description logics under the Gödel semantics, Fuzzy Sets and Systems 388 (2020), 146–178.

20.

Nguyen

L.A.

and Nguyen

N.-T.

, Characterizing crisp simulations and crisp directed simulations between fuzzy labeled transition systems by using fuzzy modal logics, In Proceedings of FUZZ-IEEE (2021), pp. 1-7, doi: 10.1109/FUZZ45933.2021.9494504

21.

Nguyen

L.A.

and Tran

D.X.

, Computing fuzzy bisimulations for fuzzy structures under the Gödel semantics, IEEE Trans Fuzzy Syst 29(7) (2021), 1715–1724.

22.

Paige

and Tarjan

R.E.

, Three partition refinement algorithms, SIAM J Comput 16(6) (1987), 973–989.

23.

Pan

, Cao

, Zhang

and Chen

, Simulation for lattice valued doubly labeled transition systems, Int J Approx Reason 55(3) (2014), 797–811.

24.

Pan

, Li

and Cao

, Lattice-valued simulations for quantitative transition systems, Int J Approx Reason 56 (2015), 28–42.

25.

Stanimirović

, Stamenković

and Ćirić

, Improved algorithms for computing the greatest right and left invariant boolean matrices and their application, Filomat 33(9) (2019), 2809–2831.

26.

, Chen

, Bu

T.-M.

and Deng

, Algorithmic and logical characterizations of bisimulations for non-deterministic fuzzy transition systems, Fuzzy Sets Syst 333 (2018), 106–123.

27.

and Deng

, Logical characterizations of simulation and bisimulation for fuzzy transition systems, Fuzzy Sets Syst 301 (2016), 19–36.