Multi-valued bisimulation quotienting algorithms 1

Abstract

By considering the multi-valued bisimulation quotients, smaller multi-valued models are obtained. This minimization can be exploited for efficient multi-valued model checking. In this paper, we illustrate an application of the multi-valued bisimulation quotients. Further, we present some definitions of partitions of multi-valued Kripke structures. Finally, as the main contribution, in order to generate the multi-valued bisimulation quotient, we provide a series of algorithms and analysis the time complexity of it.

Keywords

Multi-valued Kripke structure bisimulation quotient partition

1 Introduction

Under certain conditions, Bisimulation [1] provides a replacement strategy to deal with the state space explosion problem in model checking. Classical bisimulation requires any truth value of label functions and transition relation must be certainly and accurately, i.e., the truth values of label functions and transition relation limited by “true” or “false”.

However, A majority of realistic systems are more or less having uncertainty. In order to realize bisimulation of uncertain systems, Baier and Katoen combined with Markov chains provided the probabilistic bisimulation [15, 16]. Despite probabilistic model can describe randomized uncertainty, it still can not resolve the issues which are not regulated by probabilistic computing characteristics. Different from probabilistic bisimulation, Pan et al. combined with lattice-valued transition systems proposed a-bisimulation [2] and lattice-valued bisimulation [3]. The non-contradiction law (i.e., a ∧ ¬ a = 0) and excluded middle law(i.e., a ∨ ¬ a = 1) are unrestricted because of lattice-valued transition systems allow more than two truth values like “uninitialized”, “unknown”, “don’t care”, and more. Recently, Cao et al. investigated bisimulation for fuzzy transition systems [4]. And Wu et al. did a deeply study about logical characterizations of bisimulation for fuzzy transition systems [5]. But besides bisimulation, model checking also has great development in uncertain systems [10 –14].

Recently bisimulation studies using complete residuated lattices as truth values. Some well-known algebraic structures such as Heyting algebras [6], Boolean algebras [7] and Lukasiewicz algebras [9] are all particular cases of complete residuated lattices [8]. And being once proved in complete residuated lattice, the result will be valid in any of its special cases. Thus, a lot of authors think the lattices-valued bisimulation covers the bisimulation of above special cases. In spite of complete residuated lattices are general algebraic structures and generalize many algebras with very important application. De Morgen algebra [17], however, are of a special one. Any finite De Morgen algebra with operators ⊗ and → defined as x ⊗ y = x ∧ y, x → y = ⋁ {z : x ∧ z ≤ y}, is a complete residuated lattice. A finite De Morgen algebra with operators → defined as x → y = ¬ x ∨ y, which has been chosen as truth values of multi-valued Kripke structures, is not necessarily a complete residuated lattices. Thus, make a precise distinction between multi-value bisimulation and lattices-value bisimulation is very essential. Unless otherwise explicitly stated, $L$ in this article will be assumed to be a De Morgen algebra.

Related work: We have proved over recent literatures, there are no very applicable multi-valued quotients algorithms for computer debugging yet. Our paper is the attempt to study multi-valued partitions algorithms. It provides some methods to generate the multi-valued pioneer quotient, multi-valued successor quotient and multi-valued quotient. And the methods also apply to generate quotients in classic transfer systems.

Organization of this paper: As truth values of multi-valued Kripke structures, we review some facts of De Morgen algebras and introduce the notions of multi-valued bisimulation. The notions of Multi-valued quotient and an application are presented in Section 3. multi-valued partitions and relevant algorithms are proposed in Section 4. Finally, we conclude the paper in Section 5.

2 Preliminaries

In this section, we start with a short introduction to the definitions of De Morgen algebras, multi-valued Kripke structures, multi-valued bisimulation and partition. For more details, please refer to [15 , 18–21].

Definition 2.1. A de Morgan algebra is a tuple $L = (L, \leq, \land, \lor, \neg, 0, 1)$ where(L, ∧ , ∨) is a distributive lattice, 0 and 1 are the bottom element and the top element, ¬ is negation operation on L, for any x, y ∈ L following laws holds:

law of de Morgan: ¬ (x ∨ y) = ¬ x ∧ ¬ y, ¬ (x ∧ y) = ¬ x ∨ ¬ y.

law of involution: ¬¬ x = x.

law of anti-monotonic: (x ≤ y) ⇔ ¬ x ⩾ ¬ y.

Any finite Boolean algebra regard as a de Morgan algebra with the conditions holds: x ∧ ¬ x = 0, x ∨ ¬ x = 1, where x ∈ L. As the general structure, the result will be valid in any finite Boolean algebra.

Any finite De Morgen algebra is a complete residuated lattice with operators ⊗ and → defined as x ⊗ y = x ∧ y, x → y = ⋁ {z : x ∧ z ≤ y}. But if operators → defined as x → y = ¬ x ∨ y, is not necessarily a complete residuated lattices. That is the reason that the bisimulation in multi-value Kripke structures is different from the bisimulation in lattice-value Kripke structures.

Definition 2.2. Given a De Morgen algebra $L = (L, \leq, \land, \lor, \neg, 0, 1)$ and a set S, an multi-valued set on S as a function f = S → L. The value of f (s) denotes as the membership that s in S. And the following operations hold:

mv-intersection: (f ∩ g) (s) ≜ f (s) ∧ g (s).

mv-union: (f ∪ g) (s) ≜ f (s) ∨ g (s).

mv set inclusion: f ⊆ g ≜ ∀ (s) . (f (s) ≤ g (s)).

mv-equality: f = g ≜ ∀ (s) . (f (s) = g (s)).

mv-complement:¬f (s) ≜ ¬ (f (s)).

Definition 2.3. A multi-valued Kripke structure is a tuple $K = (S, I, R, V, AP, L)$ , where

S is a set of states.

I is an $L$ -subset of S, called the $L$ -set of initial states, and for each s ∈ S, I (s) indicates intuitively the degree to which s is an initial state.

R is the multi-valued transition relation that maps (s, t) ∈ S × S to some $a \in L$ .

V is a label function that maps a pair (s, p) ∈ S × AP to some $a \in L$ .

AP is a finite set of atomic propositions.

$L = (L, \leq, \land, \lor, \neg, 0, 1)$ is a De Morgen algebra.

A multi-valued Kripke structure is called finite if S and AP are finite, we always assume that multi-valued Kripke structures are finite in this paper. For s_i ∈ S, 0 ≤ i ≤ n, p ∈ AP, $a \in L$ , Post_a (s_i) = {s_i+1 ∈ S|R (s_i, s_i+1) ⩾ a} denotes the set of successors of s. Pre_a (s_i) = {s_i-1 ∈ S|R (s_i-1, s_i) ⩾ a} denotes the set of predecessors of s. ρ = s₀s₁s₂ . . . s_n is a path form state s₀ in $K$ . Paths (s₀) is the set of all paths which form state s₀ in $K$ . The multi-valued trace is a composition of V and R. trace (ρ) = V (s₀, p) ∧ R (s₀, s₁) ∧ v (s₁, p) ∧ R (s₁, s₂) ∧ . . . R (s_n-1, s_n) ∧ V (s_n, p) is the trace of the path ρ.

Definition 2.4. Give multi-valued Kripke structures $K_{iitsc} = (S_{i}, I_{i}, R_{i}, V_{i}, AP, L)$ , i = 1, 2. A multi-valued bisimulation between $K_{1}$ and $K_{2}$ is a binary relation $R_{a} \subseteq S_{1} \times S_{2}$ for all s₁ ∈ S₁ and s₂ ∈ S₂, if $(s_{1}, s_{2}) \in R_{a}$ then:

V (s₁, p) = V (s₂, p) ⩾ a, p ∈ AP, a ∈ L.

If $\overset{´}{s_{1}} \in {Post}_{a} (s_{1})$ , then there exist $\overset{´}{s_{2}} \in {Post}_{a} (s_{2})$ and $(\overset{´}{s_{1}}, \overset{´}{s_{2}}) \in R_{a}$ .

If $\overset{´}{s_{2}} \in {Post}_{a} (s_{2})$ , then there exist $\overset{´}{s_{1}} \in {Post}_{a} (s_{1})$ and $(\overset{´}{s_{1}}, \overset{´}{s_{2}}) \in R_{a}$ .

Two states s₁ and s₂ are multi-valued bisimular, written s₁ ∼ _as₂, if there exists a multi-valued bisimulation

R_{a}

with

(s_{1}, s_{2}) \in R_{a}

K_{1}

and

K_{2}

are multi-valued bisimular, written

K_{1} \sim_{a} K_{2}

, if there exists a multi-valued bisimulation

R_{a}

such that for every s₁ ∈ S₁, there exists s₂ ∈ S₂ and

(s_{1}, s_{2}) \in R_{a}

. If a = 1, multi-valued bisimulation come down to classical bisimulation. Definition 2.5. A partition for S is a set Π = {B₁,. . . , B_k}, for 0 < i, j ≤ k, i ≠ j, if B_i≠ ∅, B_j≠ ∅, B_i∩ B_j = ∅ and S = ⋃ _0<i≤kB_i. B_i ∈ Π is called a block. C = B_i1 ∪ . . . ∪ B_ik ⊆ S is a super block of Π for some B_i1 . . . B_ik ∈ Π. let [s] _Π denote the unique block of partition Π containing s. For partitions Π₁ and Π₂ of S, Π₁ is called finer than Π₂ or Π₂ is called coarser than Π₁, if: ∀B₁ ∈ Π₁, ∃B₂ ∈ Π₂. B₁ ⊆ B₂. Π₁ is strictly finer than Π₂ or Π₂ is strictly coarse than Π₁, if Π₁ is finer than Π₂ and Π₁ ≠ Π₁.Definition 2.6. Let Π be a partition for S and C a super block of Π.

C is a splitter for Π if there exists a block B ∈ Π with B∩ Pre (c) ≠ ∅ and B∖ Pre (C) ≠ ∅.

Block B is stable with respect to C if B∩ Pre (c) = ∅ or B∖ Pre (C) = ∅.

Π is stable with respect to C if each block B ∈ Π is stable with respect to C.

3 Multi-valued bisimulation quotient

Follow the properties of bisimulation, some Kripke structures can construct a composition, if they fulfill some bisimulation relations. On the contrary, a Kripke structure also can be refined to a simplifying form(i.e., bisimulation quotient), if some states fulfill bisimulation. This section presents the definition of multi-valued bisimulation quotient and a specific application of it.

Definition 3.1. For a multi-valued Kripke structure $K = (S, I, R, V, AP, L)$ and multi-valued bisimulation $R_{aitsc}$ , the multi-valued bisimulation quotient is defined by $K / ~_{a} = (S / ~_{a}, I', R', V', A P, L)$

S/ ∼ _a = {[s] _{∼_a}|s ∈ S} denotes the multi-valued quotient space.

I' = {[s] _{∼_a}|s ∈ I} is the equivalent multi-valued initial states.

R' as the equivalent multi-valued relation.

V'([s]~_a, p)=V (s, p), as the equivalent labeling function.

$[s]_{\sim_{a}} = {s' \in S | (s, s') \in R}$ . I' in $K / \sim_{a}$ is the equivalent class of I in $K$ . $R' ([s_{1}] ~_{a}, [s_{2}] ~_{a}) \geq a$ , if R (s₁, s₂) ⩾ a. $V' ([s] ~_{a}, p) \geq a$ , if V (s, p) ⩾ a. Where a ∈ L.

According to multi-valued bisimulation quotient, multi-valued state space can be the greatest reduced.

Example 3.2. Consider a real-time traffic network of Los Angeles, the multi-valued bisimulation quotient can provide an insight to help console to make decision that how to dispatch ambulance isoptimally.

As shown as Fig. 1. s₀ is the current location of an ambulance, s₁, s₂, s₃ and s₄ are four patients in need of treatment, s₅ and s₉ are two gas stations, s₆, s₇, s₈, s₁₀, s₁₁ and s₁₂ are the hospitals distribution in current region. Red(dark) road represents the traffic flows are large. The car “may be” drive in the red roads and “must” drive in the normal roads. The car “may be” or “must” need to refuel, when driving in the red roads or long distance. Below are the options of the ambulance bring patients to hospitals.→1/2 represent current road jammed, maybe pass through it,→1 represent current road unimpeded, must pass through it.

{s₀} →1/2 {s₁} →1/2 {s₅} →1/2 {s₁₁}.

{s₀} →1/2 {s₁} →1/2 {s₆}.

{s₀} →1/2 {s₂} →1/2 {s₇}.

{s₀} →1 {s₃} →1 {s₈}.

{s₀} →1 {s₄} →1 {s₉} →1 {s₁₂}.

{s₀} →1 {s₄} →1 {s₁₀}.

Fig.1

Real-time traffic network of Los Angeles.

In Fig 2. (A) is a multi-valued Kripke structure(3-valued) of the original insight. S = {s₀, s₁,. . . , s₁₂}, AP = {p₁, p₂, p₃, p₄}, where p₁ labels states whether are ambulance, p₂ labels states whether are patients, p₃ labels states whether are gas stations, p₃ labels states whether are hospitals. Because s₁₁ is being constructed, V (s₁₁, p₄) ⩾1/2 represent s₁₁ “maybe” is a hospitals.

Fig.2

Multi-valued bisimulation quotient of insight.

(B) is the multi-valued bisimulation quotient of (A), it simplified the decision and provide an optimal insight as below.

{s₀} →1/2 {s₁, s₂} →1/2 {s₅} →1/2 {s₁₁}.

{s₀} →1/2 {s₁, s₂} →1/2 {s₆, s₇}.

{s₀} →1 {s₃, s₄} →1 {s₉} →1 {s₁₂}.

{s₀} →1 {s₄} →1 {s₈, s₁₀}.

4 Multi-valued bisimulation quotient algorithms

There are several algorithms for computing the multi-valued bisimulation quotient. Below sections will respectively explain the details of multi-valued AP partition algorithm, multi-valued pioneer refinement algorithm and multi-valued successor refinement algorithm.

4.1 Multi-valued AP partition algorithm

In the multi-valued AP partition algorithm, the states regroup to follow whether the label function values are equally. It determines the equivalent multi-valued initial states.

Definition 4.1. The AP partition Π_AP of a multi-valued Kripke structure $K$ is induced by R_AP = {(s₁, s₂) ∈ S × S|V (s₁, p) = V (s₂, p) ⩾ a, p ∈ AP, a ∈ L}.

Follow the definition, the procedure of multi-valued AP partition Π_AP is the procedure to generate a multi-valued decision tree.

As Fig. 3. The different branches of the multi-valued decision tree represent different label function memberships. The AP decides the height of the multi-valued decision tree, for AP = {p₁, p₂}, the height of the multi-valued decision tree is 2. The vertices at depth 1 represent the decision “V (s_i, p₁) ⩾ a”, the vertices at depth 2 represent the decision “V (s_i, p₂) ⩾ a”, s_i ∈ S, a ∈ L. Ultimately, according to different memberships, the states space will divide into some leafs, and the leafs represent the result of AP partition.

Fig.3

Multi-valued decision tree Π_AP.

Example 4.2. As shown as Fig. 4. (A) describes a 3-valued Kripke structure $K$ with AP = {p₁, p₂} and $L = {0, 1 / 2, 1}$ . The result of 3-valued AP partition Π_AP consists of 5 blocks of (B).

Block B₀ = {s₀}, because of V (s₀, p₁) =1 and V (s₀, p₂) =0.

Block B₁ = {s₁}, because of V (s₁, p₁) =1 and V (s₁, p₂) ⩾1/2.

Block B₂ = {s₂}, because of V (s₂, p₁) ⩾1/2 and V (s₂, p₂) =0.

Block B₃ = {s₃, s₄, s₅}, because of V (s₃, p₁) =0, V (s₄, p₁) =0, V (s₅, p₁) =0 and V (s₃, p₂) =0, V (s₄, p₂) =0, V (s₅, p₂) =0.

Block B₄ = {s₆}, because of V (s₆, p₁) ⩾1/2 and V (s₆, p₂) ⩾1/2.

Fig.4

A 3-valued AP partition.

After the 3-valued AP partition:

Π_AP = {(s₀) , (s₁) , (s₂) , (s₃, s₄, s₅) , (s₆)}.

The essential steps are outlined in Algorithm 1.

Algorithm 1

Computing the multi-valued AP partition

Input:

K

over AP = {p₁,. . . p_n}, a ∈ L.

Output: multi-valued AP partition Π_AP.

new(v₀); //create a root vertex

for alls ∈ S do

v = v₀; //start a top-down traversal

for alli = 1,. . . , n - 1 do

for alla ∈ Ldo

ifV (s, p_i) ⩾ a

then new(branch(v));

v:=branch(v); //create a branch of v

for alla ∈ Ldo

ifV (s, p_n) ⩾ a //v is a vertex at depth n

then new(branch(v));

states(branch(v)):=states(branch(v))∪s;

return states(branch(v)); //return a leaf

For each states s ∈ S, the multi-valued decision tree has to be traversed from root to leaf will take the time Θ (|AP| · |L|). So the time complexity of computing the multi-valued AP partition Θ (|S| · |AP| · |L|). When a = 1, the multi-valued decision tree comes down to the binary tree, and it is a binary tree traversal of classical bisimulation quotient with the time complexity Θ (|S| · |AP|).

4.2 Multi-valued refinement partition

Π_AP is guaranteed the states with the equal label function memberships. However, there are still existing some multi-valued partitions Π_i (i ≠ 0) finer than multi-valued AP partition Π_AP. This is taken care of in the successive multi-valued refinement steps. The multi-valued refinement procedure will be terminated till Π_i can not was further refined. This successive refinement partition steps called as multi-valued refinement partitions.

The multi-valued refinement partitions include multi-valued pioneer refinement and Multi-valued successor refinement.

4.2.1 Multi-valued pioneer refinement

Definition 4.3. C is a multi-valued pioneer splitter for Π if there exists a block B ∈ Π with B∩ Pre_a (C) ≠ ∅, a ∈ L.

Definition 4.4. Block B is multi-valued pioneer stable to C if and only if B∩ Pre_a (C) = ∅, a ∈ L.

Definition 4.5. Let Π is a multi-valued partition for S, C is a super block of Π. The multi-valued pioneer refinement:

Refine_pre (Π, C) = ⋃ _B∈ΠRefine_pre (B, C) = ⋃ _B∈Π (⋃ _a∈L (B ∩ Pre_a (C))).

Lemma 4.6. After multi-valued pioneer refinement, no further multi-valued pioneer refinements are possible, Π_pre is the pioneer quotient of the original multi-valued Kripke structure.

Example 4.7. Fig. 5 illustrate the multi-valued pioneer refinement by a 3-value Kripke structure.

Fig.5

3-value pioneer refinement.

After AP partition, Π₀ = Π_AP = {B₁, B₂, B₃, B₄}. Where B₁ = {s₀, s₁, s₂}, B₂ = {s₃, s₄, s₅, s₆}, B₃ = {s₇, s₈}, B₄ = {s₉, s₁₀, s₁₁, s₁₂}.

For multi-valued pioneer refinement, start from Π₀. In the first iteration, consider C₁ = B₂ as the first multi-valued pioneer splitter.

⋃_a∈L (B₁ ∩Pre_a (C₁))= (B₁ ∩ Pre₀ (C₁)) ∪ (B₁ ∩ Pre_1/2(C₁)) ∪ (B₁ ∩Pre₁ (C₁)) = {s₀} ∪{s₁,s₂} ∪ {s₁, s₂}={{s₀},{s₁,s₂}}.

B₁ divides into B₁₁ = {s₀}, B₁₂ = {s₁, s₂}. Then Π₁ = {B₁₁, B₁₂, B₂, B₃, B₄}

No further multi-valued pioneer refinements are possible in Π₁, thus Π_pre = Π₁ agrees with multi-valued pioneer stable, Π_pre is the multi-valued pioneer quotient.

4.2.2 Multi-valued successor refinement

Definition 4.8. C is a multi-valued successor splitter for Π if there exists a block B ∈ Π with B∩ Post_a (C) ≠ ∅, a ∈ L.

Definition 4.9. Block B is multi-valued successor stable to C if and only if B∩ Post_a (C) = ∅, a ∈ L.

Definition 4.10. Let Π is a multi-valued partition for S, C is a super block of Π. The multi-valued successor refinement:

$\begin{matrix} {Refine}_{post} (Π, C) = ⋃_{B \in Π} {Refine}_{post} (B, C) \\ = ⋃_{B \in Π} (⋃_{a \in L} (B \cap {Post}_{a} (C)) . \end{matrix}$

Lemma 4.11. After multi-valued successor refinements, no further multi-valued successor refinements are possible, Π_post is the successor quotient of the original multi-valued Kripke structure.

Example 4.12. Fig. 6 illustrates the principle of successor refinement.

Fig.6

3-value successor refinement.

For multi-valued successor refinement, start from Π₀ = Π_AP.

In the first iteration, consider C₁ = B₁ as the first multi-valued successor splitter.

⋃_a∈L (B₂ ∩ Post_a (C₁)) = (B₂ ∩ Post₀ (C₁)) ∪ (B₂ ∩ Post_1/2 (C₁)) ∪ (B₂ ∩ Post₁ (C₁)) = ∅ ∪ {s₃, s₅} ∪ {s₄, s₆} = {{s₃, s₅}, {s₄, s₆}}.

B₂ divides into B₂₁ = {s₃, s₅}, B₂₂ = {s₄, s₆}. Then Π₁ = {B₁, B₂₁, B₂₂, B₃, B₄}.

In the second iteration, consider C₂ = B₃ as the second multi-valued successor splitter.

$⋃_{a \in L}$ (B₄ ∩ Post_a (C₂)) = (B₄ ∩ Post₀ (C₂)) ∪ (B₄ ∩ Post_1/2 (C₂)) ∪ (B₄ ∩ Post₁ (C₂)) = ∅ ∪ {s₁₀, s₁₁} ∪ {s₉, s₁₂} = {{s₉, s₁₂}, {s₁₀, s₁₁}}.

B₄ divides into B₄₁ = {s₉, s₁₂}, B₄₂ = {s₁₀, s₁₁}. Then Π₂ = {B₁, B₂₁, B₂₂, B₃, B₄₁, B₄₂}.

No further multi-valued successor refinements in Π₂, thus Π_post = Π₂ agrees with multi-valued successor stable. And Π_post is the multi-valued successor quotient.

4.2.3 Multi-valued refinement

Definition 4.13. The multi-valued refinement: $\begin{matrix} Refine (Π, C) \\ = {Refine}_{pre} (Π, C) \cap {Refine}_{post} (Π, C) \end{matrix}$

Definition 4.14. Π is multi-valued stable to C if and only if each block B ∈ Π satisfies multi-valued pioneer stable and multi-valued successor stable.

Lemma 4.15. A multi-valued refinement result is multi-valued pioneer quotient when it fulfils multi-valued pioneer quotient and multi-valued successor quotient.

Example 4.16. As show as Fig. 7, multi-valued refinement.

Fig.7

3-value successor refinement.

Π_refinement = Π_pre ∩ Π_post = {{s₀} , {s₁, s₂} , {s₃, s₅} , {s₄, s₆} , {s₇, s₈} , {s₉, s₁₂} , {s₁₀, s₁₁}} is multi-valued stable.

After multi-valued AP partition, multi-valued pioneer refining partition and multi-valued successor refining partition, Π_refinement is the multi-valued bisimulation quotient.

Algorithm 2 outlines the main steps of multi-valued refinement partition. Both multi-valued pioneer refinement and multi-valued successor refinement start form multi-valued AP partition Π_AP. When Π_i is multi-valued pioneer stable and multi-valued successor stable, the iteratively multi-valued pioneer refinement and multi-valued successor refinement will be stop and Π_i is multi-valued stable. By means of above, every state s ∈ C for multi-valued pioneer refinement, the time costs $Θ (| Pre (s) | \cdot | L |)$ , for multi-valued successor refinement, the time costs $Θ (| Post (s) | \cdot | L |)$ . Hence for all states, the time costs of multi-valued pioneer refinement and multi-valued successor refinement are $Θ (\sum_{s \in S} | Pre (s) | \cdot | L |) = Θ (| Pre (S) | \cdot | L |)$ and $Θ (\sum_{s \in S} | Post (s) | \cdot | L |) = Θ (| Post (S) | \cdot | L |)$ . We obtain for the time complexity of the refinement operator: $Θ (| Pre (S) | \cdot | L | + | Post (S) | \cdot | L |)$ . When a = 1, the time complexity of the refinement operator is Θ (|Pre (S) |) for classical quotient.

Algorithm 2

Computing the multi-valued refinement partition

Input:

X

over AP = {a₁,. . . a_n},

d \in L

Output: multi-valued bisimulation quotient space

S / \sim_{B}

Π_pre : = Π_AP;

while there exists a multi-valued pioneer splitter for Πdo

choose a multi-valued pioneer splitter C for Π;

Π_pre : = Refine (Π, C) _pre;

Π_post : = Π_AP;

while there exists a multi-valued successor splitter for Πdo

choose a multi-valued successor splitter C for Π;

Π_post : = Refine (Π, C) _post;

returnΠ_refinement = Π_pre ∩ Π_post;

5 Conclusion

Bisimulation has been effectively applied to the analyses of systems, protocols and algorithms. Quotient has very important role in bisimulation and it provides a method to obtain the minimization of many systems. Multi-valued bisimulation extend truth values into De Morgen algebras, and it realises different multi-valued systems comparison. Thus, the definitions and algorithms of how to generate a quotient in multi-valued systems are also significant andessential.

In this paper, we have investigated quotient of multi-valued Kripke structures. Firstly of all, we have used an application of traffic to illustrate that how quotients to help to make decisions and insights in multi-value environments. Secondly, we have introduced some important definitions of the multi-value AP partition and the Multi-valued refinement partition. Finally, we have illustrated the processes of how to generate multi-value quotient by a series of examples and algorithms. And we also analysis every algorithm’s time complexity. Because of the properties between De Morgen algebras and Boolean algebras, all the algorithms and method can be used for classical model checking are obviously.

In future research, if using complete residuated lattices as truth values, it would be very interesting to discuss relevant quotient algorithms. And we also need to consider some improved algorithms to reduce the time complexity.

References

Peled

, Clarke

, Grumberg

, Model checking, The MIT Press, 1999.

Pan

, Zhang

, Wu

and Chen

, Quantitative analysis of lattice-valued kripke structures, Fundamenta Informaticae 135 (2014), 269–293.

Pan

, Zhang

and Chen

, Bisimulation For Latticevalued Transition Systems, 2012 IEEE Sixth International Symposium on Theoretical Aspects of Software Engineering.

Cao

Y.Z.

, Chen

G.Q.

and Kerre

, Bisimulations for Fuzzy-Transition Systems, IEEE Transactions on Fuzzy Systems 19(3) (2011), 540–552.

H.Y.

and Deng

Y.X.

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

Belohlavek

, Fuzzy Relational Systems, Foundations and Principles, Kluwer, 2012.

Jonnson

and Tarski

, Boolean algebras with operators, American Journal of Mathematics 74(1) (1952), 127–116.

Qiu

D.W.

, Automata theory based on complete residuated latticeąłvalued logic(I) and (II), Sci China, Ser F 44 (2001), 419–429; Sci China, Ser F 45 (2002), 442–452.

Kroupa

, States in Lukasiewicz logic correspond to probabilities of rational polyhedra, Int J Approx Reason 5 (2012), 435–446.

10.

Y.M.

, Droste

and Lei

L.H.

, Model checking of lineartime properties in multi-valued systems, Information Sciences 377 (2017), 51–74.

11.

, Li

and Ma

, Computation tree logic model checking based on possibility measures, Fuzzy Sets Syst 262 (2015), 44–59.

12.

and Ma

, Quantitative computation tree logic model checking based on generalized possibility measures, IEEE Trans Fuzzy Syst 23(6) (2015), 2034–2047.

13.

Feng

, Yu

N.K.

and Ying

M.S.

, Model checking quantum Markov chains, Journal of Computer and System Sciences 79 (2013), 1181–1198.

14.

Y.M.

and Li

L.J.

, Model checking of linear-time properties based on possibility measure, IEEE Trans Fuzzy Syst 21(5) (2013), 842–854.

15.

Baier

, Katoen

J.P.

, Principles of model checking, The MIT Press, 2007.

16.

Hart

and Sharir

, Probabilistic propositional temporal logics, Information and Control (1986), 97–155.

17.

Bloc

, Borowik

, Multi-Valued Logics, Springer-Verlag, Berlin, 1992.

18.

Chechik

, Easterbrook

, Petrovykh

, Model-checking over multi-valued logics, Lecture Notes in Computer Science, 2021, Springer Verlag, Berlin, 2001, pp. 72–98 .

19.

Chechik

, Devereux

, Gurfinkel

and Easterbrook

, Multivalued symbolic model-checking, on Software Engineering and Methodology 12(4) (2003), 371–408.

20.

Chechik

, Deverux

and Gurfinkel

, Model-checking infinite state-space systems with fine-grained abstractions using SPIN, Proceedings of the 8th SPIN Workshop on Model Checking Software, Lecture Notes in Computer Science, Toronto, Canada, vol. 2057, Springer, 2001, pp. 16–36.

21.

Paigef

and Tarjant

, Three partition refinement algorithms, Society for Industrial and Applied Mathematics 16(6) (1987), 973–989.