Quantitative reachability analysis of generalized possibilistic decision processes

Abstract

The verification of reachability properties of fuzzy systems is usually based on the fuzzy Kripke structure or possibilistic Kripke structure. However, fuzzy Kripke structure or possibilistic Kripke structure is not enough to describe nondeterministic and concurrent fuzzy systems in real life. In this paper, firstly, we propose the generalized possibilistic decision process as the model of nondeterministic and concurrent fuzzy systems, and deduce the possibilities of sets of paths of the generalized possibilistic decision process relying on defining of schedulers. Then, we give fuzzy matrices calculation methods of the maximal possibilities and the minimal possibilities of eventual reachability, always reachability, constrained reachability, repeated reachability and persistent reachability. Finally, we propose a model checking approach to convert the verification of safety property into the analysis of reachabilities.

Keywords

Generalized possibilistic decision processes scheduler fuzzy matrices reachability safety property

1 Introduction

Reachability is one of the central problems in model checking [1, 2], program analysis [3] and verification [3], which is about whether a system in one state can reach other states [4]. Reachability is widely applied in urban transportation planning [5], human geography [6], regional economics and computer science [7]. In computer science, the use of reachability decision algorithm can avoid the loop detection of useless state space, save the memory occupancy of the algorithm, and improve the efficiency of the algorithm. The use of reachability optimization algorithm can reduce the complexity of the algorithm [4].

Reachability problems based on classical model checking were proposed in [8]. Classical model checking is to verify the qualitative characteristics of systems. Qualitative reachability aims at obtaining exact values of certain events. However, in real life, there are some randomness, uncertainties and inconsistencies that classical model checking is unable to express those information, such as a 90 percent probability of system crashing during operation [12]. To embed uncertain information into the model, quantitative model checking methods are proposed, including probabilistic model checking [4], possibilistic model checking [17], multi-valued model checking [10, 11] and fuzzy model checking [2 , 18]. Quantitative reachability is to find the maximum probability [15] or the minimum probability [17].

This study extends the existing approach of the generalized possibilistic model checking to solve quantitative reachability problems. Li et al. [17 , 22] propose possibility model checking and generalized possibility model checking in combination with measure theory, providing a solution to the existing problems of fuzzy model checking. In [17], the reachability problem based on the possibility measure is given, and the reachability problem is studied by using a possibilistic Kripke structure as a model. In the existing generalized possibilistic model checking, the generalized possibilistic Kripke structure is the formal model of the representation system. However, in real life, a generalized possibilistic Kripke structure cannot describe nondeterministic and concurrent fuzzy systems. For example, suppose three experts want to formulate treatment schemes for a new bacterial infection. Because different experts have different understandings of the disease, each expert has a different scheme. We use a generalized possibilistic Kripke structure K = (S, P, I, AP, L) to model the patient’s treatment process respectively. It describes three treatment processes given by three experts(α, β and γ) in Fig. 1(a), (b), (c). However, the generalized possibilistic Kripke structure can only represent the treatment process of a scheme, cannot describe the joint consultation of three experts. To solve this problem, we propose a generalized possibilistic decision process to describe nondeterministic and concurrent fuzzy systems.

Fig. 1

The treatment processes by three experts.

In this paper, we mainly study the maximum possibility problem and the minimum possibility problem of eventual reachability, always reachability, constrained reachability, repeated reachability and persistent reachability under a generalized possibilistic decision process. First, we propose a generalized possibilistic decision process as the model of fuzzy systems, and deduce the possibilities of sets of paths of the generalized possibilistic decision process relying on defining of schedulers. Then, the fuzzy matrices calculation methods of reachability under a generalized possibilistic decision process are given, and the results show that the compositional operations of the fuzzy matrix is polynomial time, which is better than the exponential level of existing algorithms. Finally, we propose a model checking approach to convert the verification of safety property into the analysis of reachabilities.

The rest of this paper is organized as follows. Section 2 gives some preliminary knowledge. In Section 3, we define generalized possibilistic decision processes. In Section 4, we present the fuzzy matrix calculation methods of eventual reachability, always reachability, constrained reachability, repeated reachability and persistent reachability. In Section 5, we use good prefixes to analyze the possibilistic regular safety property. Section 6 is the conclusion. The proofs of some theorems of this paper can be found in the Appendix.

2 Preliminaries

To model and verify fuzzy systems, we provide some necessary knowledge including the fuzzy set, fuzzy set operation, fuzzy matrix operation, closure and others.

Definition 1. [23 , 28] Let X be a universal set. A fuzzy set A of X is an function which associates each element in X a value in the interval [0, 1], i.e., A : X ⟶ [0, 1]. For x ∈ X, A (x) is the membership of x in the fuzzy set A.

We use $F (X)$ to represent all fuzzy sets in X, i.e. $F (X) = {A ∣ A : X ⟶ [0, 1]}$ .

Definition 2. [26, 28] Let $A, B \in F (X)$ , we use A ∪ B, A ∩ B, A^c to represent the union, intersection and complement of A and B. The definition is as follows.

(A ∪ B) (x) = A (x) ∨B (x) = max {A (x) , B (x)},

(A ∩ B) (x) = A (x) ∧ B (x) = min {A (x) , B (x)},

A^c (x) =1 - A (x).

Definition 3. [26, 28] Let R and S be two fuzzy matrices with m rows and n columns, i.e., R = (r_ij) _m×n, S = (s_ij) _m×n. We introduce some set operators.

R = S if and only if r_ij = s_ij for all i, j.

R ⊆ S if and only if r_ij ≤ s_ij for all i, j.

R ∪ S = (r_ij∨s_ij) _m×n.

R ∩ S = (r_ij ∧ s_ij) _m×n.

R^c = (1 - r_ij) _m×n.

Definition 4. [26, 28] Let R be a fuzzy matrix with m rows and n columns, and S be a fuzzy matrix with n rows and l columns, i.e., R = (r_ij) _m×n and S = (s_ij) _n×l. The composition operation of R and S is R ∘ S = (t_ij) _m×l, where $t_{ij} = \lor_{k = 1}^{n} (r_{ik} \land s_{kj})$ , (i = 1, 2, . . . , m, j = 1, 2, . . . , l). For fuzzy matrices R, S, T, the composition operation has some operation laws.

(R ∘ S) ∘ T = R ∘ (S ∘ T);

(R ∪ S) ∘ T = (R ∘ T) ∪ (S ∘ T).

Let X be a universal set. For the fuzzy matrix R = (R (s, t)) _s,t∈X, we use R⁺ to denote its transitive closure. When X is finite, X has ∣X∣ elements, then R⁺ = R ∪ R² ∪ . . . ∪ R^∣X∣, where R^k+1 = R^k ∘ R for any positive integer number k. The Kleene closure R^* = R⁰ ∪ R⁺, for each 1≤ s, t ≤ ∣ S ∣, $R^{0} (s, t) = {\begin{matrix} 1 & s = t \\ 0 & s \neq t \end{matrix}$ . Possibility measure theory is a kind of uncertainty theory, which mainly deals with incomplete information and uncertain information. In addition, the possibility measure does not require additivity, which is more applicable to deal with practical application systems.

Definition 5. [21] Let X be a nonempty set,and Ω be a set composed of some subsets of X elements. We call Ω a σ- algebra, which is closed to countable and take complement set operations. The possibility measure on σ- algebra Ω is a mapping POS : Ω → [0, 1], which satisfies the following conditions:

POS (∅) =0;

POS (X) =1;

If E_i ∈ Ω, i ∈ I, then POS (⋃ _i∈IE_i) = ⋁ _i∈IPOS (E_i)

If only conditions(1) and (3), then POS is called a generalized possibility measure. If POS is a generalized possibility measure on the power set 2^X,for any A ⊆ X, there is POS (A) = ⋁ _a∈APOS ({ a }).

Definition 6. [18] A Generalized possibilistic Kripke structure(GPKS) is a tuple K = (S, P, I, AP, L), where

S is a countable, nonempty states set;

P : S × S → [0, 1] is the possibility transition distribution, for any states s, there is a state t, such that P (s, t) >0;

I : S → [0, 1] is the initial distribution of possibility and there exists a state s, such that I (s) >0;

AP is a set of atomic propositions;

L : S × AP → [0, 1] is a label function, L (s, a) represents the true value of atomic proposition a in state s.

For a GPKS K, its path is defined as an infinite sequence of states π = s₀s₁s₂ ⋯ ∈ s^ω, for any i so that P (s_i, s_i+1) > 0. Let Paths (s) and Paths_fin (s) represent the set of all infinite and finite paths starting from the state s in K. Paths (K) represents the set of all infinite paths in K, Paths_fin (K) represents the set of all finite paths in K, such as $\hat{π} = s_{0} s_{1} \dots s_{n}$ .

3 Generalized Possibilistic Decision Processes

In this section, first, we give the notion of the generalized possibilistic decision process. Then, the definition of the scheduler is proposed to solve the nondeterministic the generalized possibilistic decision process. Finally, we solve the generalized possibility measure problems.

Nondeterminism is absent in GPKS. The generalized possibilistic decision process can be viewed as a variant of GPKS that permits both possibility and nondeterministic choices.

Definition 7. A Generalized possibilistic decision process(GPDP) is a tuple M = (S, Act, P, I, AP, L), where

S is a countable, nonempty set of states;

Act is a set of actions;

P : S × Act × S ⟶ [0, 1] is a function, called possibilistic transition distribution function. For all states s ∈ S and actions α ∈ Act, there exits a state t ∈ S such that P (s, α, t) >0;

I : S ⟶ [0, 1] is a function, there exits states s such that I (s) >0;

AP is a set of atomic propositions;

L : S × AP ⟶ [0, 1] is a possibilistic labeling function, which can be viewed as function mapping a state s to the fuzzy set of atomic proposition, L (s, a) denotes the possibility or truth value of atomic proposition a which is hold in state s.

Furthermore, if the set S, Act and AP are finite sets, then M is a finite GPDP. In this paper, we always assume that GPDPs are finite. A GPDP has a unique initial distribution I. For all states s, t ∈ S and actions α ∈ Act, P (s, α, t) denotes the possibility from state s under action α to state t. An action α is enabled in state s if and only if P (s, α, t) >0. Let Act (s) denote the set of enabled actions in state s. For any states s ∈ S, it is required that Act (s)≠ ∅. Each state t for which P (s, α, t) >0 is called an α-successor of s. The set of direct α-successors of s is defined as:

Post (s, α) = {t ∈ S ∣ P (s, α, t) >0}.

The set of α-predecessors of s is defined by:

Pref (t) = {(s, α) ∈ S × Act (s) ∣ P (s, α, t) >0}.

We also use the P (s, α, T) to denote the possibility from the state s under the action α to the set T of states, that is, $P (s, α, T) = \underset{t \in T}{\lor} P (s, α, t)$ .

Paths in GPDP M are defined as infinite alternating sequences π = s₀ α₀s₁ α₁s₂ ⋯ ∈ (S × Act) ^ω such that P (s_i, α_i, s_i+1) >0 for all i ∈ I. Paths (s) denotes the set of all infinite paths in M that start in state s. Similarly, Paths_fin (s) denotes the set of all finite path fragment $\hat{π} = s_{0} α_{0} s_{1} α_{1} s_{2} \dots α_{n - 1} s_{n}$ such that s₀ = s. Paths (M) and Paths_fin (M) denote the set of all infinite paths and finite paths in M respectively. The trace of the infinite path fragment π = s₀s₁⋯ is defined as trace(π) = L (s₀) L (s₁)⋯. The trace of the finite path fragment $\hat{π}$ = s₀s₁ ⋯ s_n is defined as trace( $\hat{π}$ ) = L (s₀) L (s₁) ⋯ L (s_n).The trace of all infinite paths starting from state s is defined as Traces (s) = trace (Paths (s)).

Example 1. Let us consider the joint consult of three experts in Fig. 1(a),(b),(c). GPDP in Fig. 2, where states are represented by ovals and transitions by labeled edges, and state names are depicted outside the ovals, and labeling functions of the states are depicted inside the ovals.

Fig. 2

Treatment process by three experts’ consultation.

S = {s₀, s₁, s₂}, Act = {α, β, γ}, AP = {P, G, E}. P indicates that the patient is in “bad” health, G indicates that the patient is in “normal” health, E indicates that the patient is in “good” health.

For state s₀, the labeling functions are L (s₀, P) =0.85, L (s₀, G) =0.3, L (s₀, E) =0.2. L (s₀, P) =0.85 indicates that the degree of “bad” health in state s₀ is 0.85. L (s₀, G) =0.3 indicates that the degree of “normal” health in state s₀ is 0.3. L (s₀, E) =0.2 indicates that the degree of “good” health in state s₀ is 0.2.

Act (s₀) = {α, β, γ}, α, β, γ indicate three different treatment indicates. P (s₀, α, s₁) =0.8 indicates that the possibility of the patient’s health condition changing from state s₀ to state s₁ is 0.8 after the expert treats the patient with the α scheme. P (s₀, β, s₁) =0.6 indicates that the possibility of the patient’s health condition changing from state s₀ to state s₁ is 0.6 after the expert treats the patient with the β scheme. P (s₀, γ, s₁) =0.2 indicates that the possibility of the patient’s health condition changing from state s₀ to state s₁ is 0.2 after the expert treats the patient with the γ scheme.

Post (s₀, α) = {s₁, s₂},Post (s₀, α) indicates all α successor states of state s₀.

Pref (s₀) = {(s₀, α) , (s₀, β) , (s₀, γ) , (s₁, α) , (s₁, β) ,

(s₁, γ) , (s₂, α) , (s₂, β) , (s₂, γ)}, Pref (s₀) indicates all predecessor states of state s₀.

For the GPKS K, 2^Paths (K) is the algebra that is generated by ${Cyl (\hat{π}) ∣ \hat{π} \in Path s_{fin} (K)}$ on Paths (K), but the GPDPs are not augmented with a unique possibility measure. Instead, deducing possibilities of sets of paths of a GPDP rely on the resolution of nondeterminism. This resolution is performed by a scheduler. A scheduler chooses in any state s one of the actions set A ⊆ Act (s). It does not impose any constraint on the possibilistic choice that is resolved once α ∈ A has been chosen.

Definition 8. Let M = (S, Act, P, I, AP, L) be a GPDP, a scheduler for M is a function Adv : S → 2^Act so that Adv (s) ⊆ Act (s) for all s ∈ S.

Let Path_Adv (s) and ${Path}_{Adv}^{fin} (s)$ denote the set of paths and finite paths from state s under the decision of the scheduler Adv. Let Path_Adv (M) and ${Path}_{Adv}^{fin} (M)$ denote the set of paths and finite paths in the M under the decision of the scheduler Adv.

Given a GPDP M = (S, Act, P, I, AP, L), α ∈ Act, possibility distribution function P : S × α × S ⟶ [0, 1] can be represented by a fuzzy matrix. For convenience, the fuzzy matrix is written as P_α, so that P_α = (P (s, α, t)) _s,t∈S, called the fuzzy transition matrix of M corresponding to scheduler α. Using fuzzy matrix $P_{\max} = ⋁_{i = 0}^{n} P_{α_{i}}$ denotes the maximal possibility transition matrix, so that ${(P_{\max} (s, t))}_{s, t \in S} = {(⋁_{α \in Act (s)} P (s, α, t))}_{s, t \in S} .$

Using fuzzy matrix $P_{\min} = ⋀_{i = 0}^{n} P_{α_{i}}$ denotes the minimal possibility transition matrix, so that

${(P_{\min} (s, t))}_{s, t \in S} = {(⋀_{α \in Act (s)} P (s, α, t))}_{s, t \in S} .$

The GPKS K_max = (S, P_max, I, AP, L) and GPKS K_min = (S, P_min, I, AP, L) can be constructed from matrix P_max and matrix P_min respectively.

Example 2. As shown in the Example 1, the order of s₀→s₁→s₂ is used to give the fuzzy matrices P_max, P_min. $\begin{matrix} P_{\max} = (\begin{matrix} 0.8 & 0.8 & 0.3 \\ 0.5 & 0.9 & 0.9 \\ 0.3 & 0.8 & 1 \end{matrix}), P_{\min} = (\begin{matrix} 0.3 & 0.2 & 0.1 \\ 0.2 & 0.5 & 0.4 \\ 0.1 & 0.3 & 0.7 \end{matrix}), \end{matrix}$

Figure 3(a) shows the result of GPKS with respect to P_max, Fig. 3(b) shows the result of GPKS with respect to P_min.

Fig. 3

GPKS with respect to P_max and P_min.

Although GPDP can induce the GPKS under the consideration of some schedulers, reasoning about quantitative reachabilities requires a formalization of the possiblities for sets of paths. This formalization is based on possibility measure theory, in particular possibility spaces and generalized possibility measure theory.

Definition 9. Given a GPDP M = (S, Act, P, I, AP, L), let $\hat{π} = s_{0} α_{0} s_{1} α_{1} s_{2} \dots s_{n - 1} α_{n - 1} s_{n} \in {Paths}_{Adv}^{fin} (M)$ and Adv be the max or min scheduler, then the cylinder set of the finite path $\hat{π}$ is defined as $Cyl (\hat{π}) = {π \in Path s_{Adv} (M) ∣ \hat{π} \in Pref (π)},$ (1) where $Pref (π_{Adv}) = {π^{'} \in {Paths}_{Adv}^{fin} (M) ∣ π^{'}$ is a finite prefix of π_Adv }.

The cylinder set spanned by the finite adv-paths $\hat{π}$ consists of all infinite adv-paths that start with $\hat{π}$ . The cylinder sets serve as basis events of the measurable space 2^{Paths
_Adv} (M) associated with M. From classical concepts of possibility theory, it follows that there exists a unique possibility measure GPo on the measurable space 2^{Paths
_Adv} (M) associated with M are given by Definition 10.

Definition 10. Let M = (S, Act, P, I, AP, L) be a finite GPDP, the function GPo : Paths_Adv (M) → [0, 1] is defined:

$GPo (π) = I (s_{0}) \land \underset{i \geq 0}{\land} P_{Adv} (s_{i}, α_{i}, s_{i + 1})$ (2) where π = s₀ α₀s₁ α₁s₂ ⋯ ∈ Paths_Adv (M). Furthermore, we define GPo (E) = ∨ {GPo (π) ∣ π ∈ E}, for any E ⊆ Paths_Adv (M), then we have the function $GPo : 2^{Path s_{Adv} (M)} \to [0, 1]$ is called generalized possibility measure over Ω = 2^Paths_Adv(M).

Let M = (S, Act, P, I, AP, L) be a GPDP, s ∈ S, α_i ∈ Act, i ≥ 0, r_Adv : S → [0, 1] is defined as following, which denotes the maximal possibility measure of all Adv-paths from state s in M:

$\begin{matrix} r_{Adv} (s) = & ⋁ {⋀_{i \geq 0} P_{Adv} (s_{i}, α_{i}, s_{i + 1}) ∣ s_{1} \\ = s, s_{i} \in S, α_{i} \in Act} . \end{matrix}$ (3)

The role of the function r_Adv is to help us to calculate the possibility of Adv-paths in M. The Theorem 1 gives a fuzzy matrix calculation for r_Adv.

Theorem 1. Let M = (S, Act, P, I, AP, L) be a finite GPDP, for any s ∈ S, then we have

$r_{Adv} (s) = \underset{t \in S}{⋁} (P_{Adv}^{+} (s, t) \land P_{Adv}^{+} (t, t)) .$ (4)

In particular, P_Adv is normal iff r_Adv (s) =1 for any states s.

Proof. See the Appendix. ■

In the matrix notation, we have

$r_{Adv} = P_{Adv}^{+} \circ D_{Adv},$ (5) where $D_{Adv} = {(P_{Adv}^{+} (t, t))}_{t \in S}$ .

The computational complexity of r_Adv (s) mainly depends on the time of computational possibilistic transition closure. In [30], they gave an optimal algorithm to calculate D_Adv, then we get the time complexity is O (n² log n), where n =∣ S ∣.

Example 3. According to the GPDP in Example 1, for any s ∈ S,r_max and r_min corresponding to the maximal scheduler and the minimal scheduler are given,

$D_{\max} = {(P_{\max}^{+} (t, t))}_{t \in S} = (\begin{matrix} 0.8 \\ 0.9 \\ 1 \end{matrix}),$

$D_{\min} = {(P_{\min}^{+} (t, t))}_{t \in S} = (\begin{matrix} 0.3 \\ 0.5 \\ 0.7 \end{matrix}),$

$P_{\max}^{+} = (\begin{matrix} 0.8 & 0.8 & 0.8 \\ 0.5 & 0.9 & 0.9 \\ 0.5 & 0.8 & 1 \end{matrix}),$

$P_{\min}^{+} = (\begin{matrix} 0.3 & 0.2 & 0.1 \\ 0.2 & 0.5 & 0.4 \\ 0.2 & 0.3 & 0.7 \end{matrix}),$

$r_{\max} = P_{\max}^{+} \circ D_{\max} = (\begin{matrix} 0.8 \\ 0.9 \\ 1 \end{matrix}),$

$r_{\min} = P_{\min}^{+} \circ D_{\min} = (\begin{matrix} 0.3 \\ 0.5 \\ 0.7 \end{matrix}) .$

r_max (s₀) = 0.8 indicates that under the maximal possibilistic scheduler. That is, the maximal possibility of all paths from state s₀ is 0.8. r_min (s₀) = 0.3 indicates that under the minimal possibilistic scheduler. That is, the maximal possibility of all paths from state s₀ is 0.3.

Based on Theorem 1, we can get Theorem 2, which can convert the calculation of generalized possibility measure of infinite path into the calculation of possibility of finite path.

Theorem 2. Let M = (S, Act, P, I, AP, L) be a finite GPDP, then the generalized possibility measure of cylinder set $\hat{π} = s_{0} α_{0} s_{1} α_{1} \dots α_{n - 1} s_{n} \in {Paths}_{Adv}^{fin} (M)$ is: $\begin{matrix} GPo (Cyl (s_{0} α_{0} s_{1} α_{1} \dots α_{n - 1} s_{n})) \\ = I (s_{0}) \land \land_{i = 0}^{n - 1} P_{Adv} (s_{i}, α_{i}, s_{i + 1}) \land r_{Adv} (s_{n}), \end{matrix}$ where GPo (Cyl (s₀)) = I (s₀) ∧ r_Adv (s₀).

Proof. See the Appendix. ■

Example 4. According to the GPDP of Example 1, under the maximal possibilistic measure and the minimal possibilistic measure, the generalized possibility measure of cylinder set of the corresponding finite paths $\hat{π} = s_{0} α_{0} s_{1}$ are respectively,

GPo_max (Cyl (s₀ α₀s₁) ) = I (s₀) ∧ P (s₀, α₀, s₁) ∧ r_max (s₁) =0.8

GPo_min (Cyl (s₀ α₀s₁)) = I (s₀) ∧ P (s₀, α₀, s₁) ∧ r_min (s₁) =0.5 .

4 Reachability possibility

A typical task for the quantitative analysis of GPDPs is to compute the minimum or the maximum possibility for some reachabilities under consideration of the min or the max scheduler. This corresponds to the worst-case or best-case analysis possibility of GPDPs. Let M = (S, Act, P, I, AP, L) be a finite GPDP and B be a fuzzy set of target states. The fuzzy set B may represent a set of certain bad states that shall be visited with the minimum possibility, or dually, a set of good states that shall be visited with the maximum possibility. Some special reachabilities, such as eventual reachability, always reachability, constrained reachability, repeated reachability and persistent reachability are considered in this section.

4.1 Eventual reachability possibility

The event of eventual reachability is denoted ⋄B. We use the B : S ⟶ [0, 1] to represent the fuzzy set of states. For the given GPDP M, π = s₀ α₀s₁ … ∈ Paths_Adv (M), ∣∣ ⋄ B (π) ∣∣ = ⋁ _i≥0B (s_i). In the following, the quantitative analysis of eventual reachability is reduced to the computational range for all strategies of the minimum possibility or the maximum possibility of reaching a certain fuzzy set B of states.

Theorem 3. Let M = (S, Act, P, I, AP, L) be GPDP, max corresponds to the maximum possibility scheduler and min corresponds to the minimum possibility scheduler, then we have, $\begin{matrix} {GPo}_{\max} (⋄ B) & = ({GPo}_{\max} (s ⊨ ⋄ B))_{s \in S} \\ = P_{\max}^{*} \circ D_{B} \circ r_{\max} \end{matrix}$ (6) $\begin{matrix} {GPo}_{\min} (⋄ B) & = ({GPo}_{\min} (s ⊨ ⋄ B))_{s \in S} \\ = P_{\min}^{*} \circ D_{B} \circ r_{\min} . \end{matrix}$ (7)

Proof. See the Appendix. ■

Example 5. Based on Example 1, consider the generalized possibility of eventual reachability event ⋄B. Given the fuzzy state set B = (L (s, E)) _s∈S, only the reachability of the event is considered at this point, and the label function in GPDP is defined as L (s) = s.

Then the maximum possibility and minimum possibility of the event ◊^≤7B are respectively: $\begin{matrix} {GPo}_{\max} (◊^{\leq 7} B) = P_{\max}^{*} \circ D_{B} \circ r_{\max} \\ = {(\begin{matrix} 0.8 & 0.8 & 0.3 \\ 0.5 & 0.9 & 0.9 \\ 0.3 & 0.8 & 1 \end{matrix})}^{*} \circ (\begin{matrix} 0.2 & 0 & 0 \\ 0 & 0.7 & 0 \\ 0 & 0 & 0.9 \end{matrix}) \circ (\begin{matrix} 0.8 \\ 0.9 \\ 1 \end{matrix}) \\ = (\begin{matrix} 0.8 \\ 0.9 \\ 0.9 \end{matrix}), \end{matrix}$ $\begin{matrix} {GPo}_{\min} (◊^{\leq 7} B) = P_{\min}^{*} \circ D_{B} \circ r_{\min} \\ = {(\begin{matrix} 0.2 & 0.3 & 0.1 \\ 0.2 & 0.5 & 0.4 \\ 0.1 & 0.3 & 0.7 \end{matrix})}^{*} \circ (\begin{matrix} 0.2 & 0 & 0 \\ 0 & 0.7 & 0 \\ 0 & 0 & 0.9 \end{matrix}) \circ (\begin{matrix} 0.3 \\ 0.5 \\ 0.7 \end{matrix}) \\ = (\begin{matrix} 0.2 \\ 0.5 \\ 0.7 \end{matrix}) . \end{matrix}$

∥GPo (◊ ^≤7B) ∥ _max (s₀) =0.8, ∥GPo (◊ ^≤7B) ∥ _min (s₀) =0.2, describes the maximum possibility of the patient’s final state of health with the maximum possibility of “good” being 0.8 and the minimum possibility of “good” being 0.2 after 7 days treatment from state s₀.

4.2 Always reachability possibility

The event of always reachability is denoted B. We use the B : S ⟶ [0, 1] to represent the fuzzy set of states. For the given GPDPs M, π = s₀ α₀s₁ … ∈ Paths_Adv (M), B (π) = ⋀ _i≥0B (s_i). Under the maximum possibility scheduler and the minimum possibility scheduler, the methods of computing GPo_max (s ⊨ B) and GPo_min (s ⊨ B) are given. $\begin{matrix} {GPo}_{\max} (s ⊨ B) \\ = ⋁_{π \in {Paths}_{\max} (s)} ({GPo}_{\max} (π) \land ∥ B ∥ (π)) \\ = ⋁ ({GPo}_{\max} (π) \land ⋀_{i \geq 0} B (s_{i})) . \end{matrix}$

$\begin{matrix} {GPo}_{\min} (s ⊨ B) = ⋁ ({GPo}_{\min} (π) \land ∥ B ∥ (π)) \\ = ⋁ ({GPo}_{\min} (π) \land ⋀_{i \geq 0} B (s_{i})) . \end{matrix}$ From these results, we can get Theorem 4.

Theorem 4. Let M = (S, Act, P, I, AP, L) be GPDPs, max corresponds to the maximum possibility scheduler and min corresponds to the minimum possibility scheduler, then we have

$\begin{matrix} {GPo}_{\max} (B) & = ({GPo}_{\max} (s ⊨ B))_{s \in S} \\ = υ . f_{Bmax} (Z), \end{matrix}$ (8)

$\begin{matrix} {GPo}_{\min} (B) & = ({GPo}_{\min} (s ⊨ B))_{s \in S} \\ = υ . f_{Bmin} (Z), \end{matrix}$ (9) where f_Bmax (Z) = B ∧ P_max ∘ D_Z ∘ r_max, f_Bmin (Z) = B ∧ P_min ∘ D_Z ∘ r_min. υ . f_Bmax (Z) denotes the maximal fixed point of the operator f_Bmax (Z), υ . f_Bmin (Z) denotes the minimal fixed point of the operator f_Bmin (Z). We have given the solution to the maximal fixed point in [18].

Example 6. Based on Example 1, considering the generalized possibility of always reachability event ^≤7B, given the fuzzy state set B = (L (s, E)) _s∈S, the maximum possibility and the minimum possibility of all states in M satisfied event ^≤7B are respectively:

$\begin{matrix} f (z_{1}) = B \land (P_{\max}^{*} \circ D_{z} \circ r_{\max}) \\ = (\begin{matrix} 0.2 \\ 0.7 \\ 0.9 \end{matrix}) \land \\ ({(\begin{matrix} 0.8 & 0.8 & 0.3 \\ 0.5 & 0.9 & 0.9 \\ 0.3 & 0.8 & 1 \end{matrix})}^{*} \circ (\begin{matrix} 1 & 0 & 0 \\ 0 & 1 & 0 \\ 0 & 0 & 1 \end{matrix}) \circ (\begin{matrix} 0.8 \\ 0.9 \\ 1 \end{matrix})) \\ = (\begin{matrix} 0.2 \\ 0.7 \\ 0.9 \end{matrix}), \end{matrix}$

$\begin{matrix} f (z_{2}) = B \land (P_{\max}^{*} \circ D_{z_{1}} \circ r_{\max}) \\ = (\begin{matrix} 0.2 \\ 0.7 \\ 0.9 \end{matrix}) \land \\ ({(\begin{matrix} 0.8 & 0.8 & 0.3 \\ 0.5 & 0.9 & 0.9 \\ 0.3 & 0.8 & 1 \end{matrix})}^{*} \circ (\begin{matrix} 0.2 & 0 & 0 \\ 0 & 0.7 & 0 \\ 0 & 0 & 0.9 \end{matrix}) \circ (\begin{matrix} 0.8 \\ 0.9 \\ 1 \end{matrix})) \\ = (\begin{matrix} 0.2 \\ 0.7 \\ 0.9 \end{matrix}) . \end{matrix}$

fz₁ = fz₂, Therefore $\begin{matrix} {GPo}_{\max} (\leq 7 B) = (\begin{matrix} 0.2 \\ 0.7 \\ 0.9 \end{matrix}) . \end{matrix}$

Calculated by the same method $\begin{matrix} {GPo}_{\min} (\leq 7 B) = (\begin{matrix} 0.2 \\ 0.5 \\ 0.7 \end{matrix}) . \end{matrix}$

∥GPo ( E) ∥ _max (s₀) =0.2, ∥GPo ( E) ∥ _min (s₀) =0.2, it shows that from the state s₀, it is unlikely that the patient’s health always reach a “good” state after 7 days treatment.

4.3 Constrained reachability possibility

Given the GPDP M, and the fuzzy set of states B, C : S ⟶ [0, 1], consider the event of reaching B via a finite path fragment which ends in a fuzzy state s ∈ B, and visits only states in set of fuzzy states C prior to reaching fuzzy states s. This event is denoted by C ⊔ B. For n ≥ 0, the event C ⊔ ^≤nB has the same meaning as C ⊔ B, and it is required to reach B(via fuzzy state C) within n steps. Formally, C ⊔ ^≤nB is the union of the basic cylinders spanned by path fragments s₀ α₀s₁ α₁ … s_m so that m ≤ n with possibility C (s_i) for all 0 ≤ i ≤ m with possibility B (s_k).

Theorem 5. Let M = (S, Act, P, I, AP, L) be a GPDP, max corresponds to the maximum possibility scheduler and min corresponds to the minimum possibility scheduler, then we have

$\begin{matrix} {GPo}_{\max} (C ⊔^{\leq n} B) = {GPo}_{\max} (C ⊔ B) \\ = (D_{C} \circ P_{\max})^{*} \circ D_{B} \circ r_{\max}, \end{matrix}$ (10)

$\begin{matrix} {GPo}_{\min} (C ⊔^{\leq n} B) = {GPo}_{\min} (C ⊔ B) \\ = (D_{C} \circ P_{\min})^{*} \circ D_{B} \circ r_{\min} . \end{matrix}$ (11)

Proof. See the Appendix. ■

Example 7. Next, let’s continue to consider the generalized possibility of constrained reachability event C ⊔ ^≤7B. Given the fuzzy state set C = (L (s, P)) _s∈S, B = (L (s, E)) _s∈S, the maximum possibility and the minimum possibility of all states in M satisfying event C ⊔ ^≤7B are respectively:

$\begin{matrix} {GPo}_{\max} (C ⊔^{\leq 7} B) = (D_{C} \circ P_{\max})^{*} \circ D_{B} \circ r_{\max} \\ = {((\begin{matrix} 0.85 & 0 & 0 \\ 0 & 0.4 & 0 \\ 0 & 0 & 0.1 \end{matrix}) \circ (\begin{matrix} 0.8 & 0.8 & 0.3 \\ 0.5 & 0.9 & 0.9 \\ 0.3 & 0.8 & 1 \end{matrix}))}^{*} \\ \circ (\begin{matrix} 0.2 & 0 & 0 \\ 0 & 0.7 & 0 \\ 0 & 0 & 0.9 \end{matrix}) \circ (\begin{matrix} 0.8 \\ 0.9 \\ 1 \end{matrix}) \\ = (\begin{matrix} 0.7 \\ 0.7 \\ 0.9 \end{matrix}), \end{matrix}$ $\begin{matrix} {GPo}_{\min} (C ⊔^{\leq 7} B) = (D_{C} \circ P_{\min})^{*} \circ D_{B} \circ r_{\min} \\ = {((\begin{matrix} 0.85 & 0 & 0 \\ 0 & 0.4 & 0 \\ 0 & 0 & 0.1 \end{matrix}) \circ (\begin{matrix} 0.2 & 0.3 & 0.1 \\ 0.2 & 0.5 & 0.4 \\ 0.1 & 0.3 & 0.7 \end{matrix}))}^{*} \\ \circ (\begin{matrix} 0.2 & 0 & 0 \\ 0 & 0.7 & 0 \\ 0 & 0 & 0.9 \end{matrix}) \circ (\begin{matrix} 0.3 \\ 0.5 \\ 0.7 \end{matrix}) \\ = (\begin{matrix} 0.2 \\ 0.5 \\ 0.7 \end{matrix}) . \end{matrix}$

∥GPo (C ⊔ ^≤7B) ∥ _max (s₀) =0.7, ∥GPo (C ⊔ ^≤7B) ∥ _min (s₀) =0.2, which means that the patient’s health state is “bad” at state s₀. The expert adopts three treatment schemes after 7 days of treatment, the maximum possibility that a patient’s health states turn to a “good” state is 0.7 and the minimum possibility is 0.2.

4.4 Repeated reachability possibility

Let B : S ⟶ [0, 1] be a set of fuzzy states in GPDPs. For the event of repeated reachability, we use the ⋄ B to represent it. The set of all paths that visit B infinitely is often measurable. Let π = s₀ α₀s₁ α₁ … ∈ Paths_Adv (s₀), $∥ ⋄ B ∥ (π) = ⋁_{i \geq 0}^{\infty} ⋀_{j \geq i}^{\infty} B (s_{j})$ , we consider to calculate GPo_Adv (s ⊨ ⋄ B) under a scheduler Adv.

Theorem 6. Let M = (S, Act, P, I, AP, L) be a GPDP, B : S ⟶ [0, 1] is a fuzzy set of states, max corresponds to the maximum possibility scheduler and min corresponds to the minimum possibility scheduler. Then we have,

$\begin{matrix} {GPo}_{\max} (⋄ B) = P_{\max}^{+} \circ diag (P_{\max}^{+} (t, t))_{t \in S} \circ B, \end{matrix}$ (12)

$\begin{matrix} {GPo}_{\min} (⋄ B) = P_{\min}^{+} \circ diag (P_{\min}^{+} (t, t))_{t \in S} \circ B . \end{matrix}$ (13)

Proof. See the Appendix. ■

Example 8. Next, let’s continue to consider the generalized possibility of the repeated reachability event ⋄ B. Given the fuzzy state set B = (L (s, P)) _s∈S, the maximum possibility and the minimum possibility of all states in M satisfying event ⋄ B are respectively:

$\begin{matrix} {GPo}_{\max} (⋄ B) = P_{\max}^{+} \circ diag (P_{\max}^{+} (t, t))_{t \in S} \circ B \\ = {(\begin{matrix} 0.8 & 0.8 & 0.3 \\ 0.5 & 0.9 & 0.9 \\ 0.3 & 0.8 & 1 \end{matrix})}^{+} \circ (\begin{matrix} 0.8 & 0 & 0 \\ 0 & 0.9 & 0 \\ 0 & 0 & 1 \end{matrix}) \circ (\begin{matrix} 0.85 \\ 0.4 \\ 0.1 \end{matrix}) \\ = (\begin{matrix} 0.8 \\ 0.4 \\ 0.1 \end{matrix}), \end{matrix}$ $\begin{matrix} {GPo}_{\min} (⋄ B) = P_{\min}^{+} \circ diag (P_{\min}^{+} (t, t))_{t \in S} \circ B \\ = {(\begin{matrix} 0.2 & 0.3 & 0.1 \\ 0.2 & 0.5 & 0.4 \\ 0.1 & 0.3 & 0.7 \end{matrix})}^{+} \circ (\begin{matrix} 0.3 & 0 & 0 \\ 0 & 0.5 & 0 \\ 0 & 0 & 07 \end{matrix}) \circ (\begin{matrix} 0.85 \\ 0.4 \\ 0.1 \end{matrix}) \\ = (\begin{matrix} 0.3 \\ 0.4 \\ 0.1 \end{matrix}) . \end{matrix}$

When the state is s₀, ∥GPo ( ⋄ B) ∥ _max (s₀) =0.8, ∥GPo ( ⋄ B) ∥ _min (s₀) =0.3, indicates that the patients in this state are more likely to relapse. When the state is s₂, ∥GPo ( ⋄ B) ∥ _max (s₂) =0.1, ∥GPo ( ⋄ B) ∥ _min (s₀) =0.1, indicates that once the patient’s disease in this state is cured, and it basically will not recur.

4.5 Persistent reachability possibility

Let us consider persistent reachability properties events of the form ⋄ B. Let π = s₀ α₀s₁ α₁ … ∈ Paths_Adv (s₀) and B : S ⟶ [0, 1] be a fuzzy set of states in GPDPs. Thus, $∥ ⋄ B ∥ (π) = ⋀_{i \geq 0}^{\infty} ⋁_{j \geq i}^{\infty} B (s_{j})$ . Let us calculate GPo_Adv (s ⊨ ⋄ B) under the maximum possibility scheduler and the minimum possibility scheduler.

Theorem 7. Let M = (S, Act, P, I, AP, L) be a GPDP, B : S ⟶ [0, 1] is the fuzzy set of states, max corresponds to the maximum possibility scheduler and min corresponds to the minimum possibility scheduler. ${GPo}_{\max} (⋄ B) = P_{\max}^{*} \circ r_{D_{B} \circ P_{\max}},$ (14) ${GPo}_{\min} (⋄ B) = P_{\min}^{*} \circ r_{D_{B} \circ P_{\min}} .$ (15)

Proof. See the Appendix. ■

Example 9. Next, continue to consider the generalized possibility of persistent reachability event ⋄ B. Given the fuzzy state set B = (L (s, E)) _s∈S, the maximum possibility and the minimum possibility of all states in M satisfied event ⋄ B are respectively,

$\begin{matrix} D_{B} \circ P_{\max} = (\begin{matrix} 0.2 & 0 & 0 \\ 0 & 0.7 & 0 \\ 0 & 0 & 0.9 \end{matrix}) \circ (\begin{matrix} 0.8 & 0.8 & 0.3 \\ 0.5 & 0.9 & 0.9 \\ 0.3 & 0.8 & 1 \end{matrix}) \\ = (\begin{matrix} 0.2 & 0.2 & 0.2 \\ 0.5 & 0.7 & 0.7 \\ 0.3 & 0.8 & 0.9 \end{matrix}), \end{matrix}$ GPo_max (⋄ B) $= P_{\max}^{*} \circ r_{D_{B} \circ P_{\max}}$

$= {(\begin{matrix} 0.8 & 0.8 & 0.3 \\ 0.5 & 0.9 & 0.9 \\ 0.3 & 0.8 & 1 \end{matrix})}^{*} \circ (\begin{matrix} 0.2 \\ 0.7 \\ 0.9 \end{matrix}) = (\begin{matrix} 0.2 \\ 0.7 \\ 0.9 \end{matrix}),$

$\begin{matrix} D_{B} \circ P_{\min} = (\begin{matrix} 0.2 & 0 & 0 \\ 0 & 0.7 & 0 \\ 0 & 0 & 0.9 \end{matrix}) \circ (\begin{matrix} 0.2 & 0.3 & 0.1 \\ 0.2 & 0.5 & 0.4 \\ 0.1 & 0.3 & 0.7 \end{matrix}) \\ = (\begin{matrix} 0.2 & 0.2 & 0.1 \\ 0.2 & 0.5 & 0.4 \\ 0.1 & 0.3 & 0.7 \end{matrix}), \end{matrix}$ ${GPo}_{\min} (⋄ B) = P_{\min}^{*} \circ r_{D_{B} \circ P_{\max}}$

$= {(\begin{matrix} 0.2 & 0.3 & 0.1 \\ 0.2 & 0.5 & 0.4 \\ 0.1 & 0.3 & 0.7 \end{matrix})}^{*} \circ (\begin{matrix} 0.2 \\ 0.5 \\ 0.7 \end{matrix}) = (\begin{matrix} 0.2 \\ 0.5 \\ 0.7 \end{matrix}),$ where $D_{B} = {\begin{matrix} L (s, E) & s = t \\ 0 & otherwise \end{matrix}$ .

The possibility that the patient’s health continue to be “good” after the expert adopts the combination of three schemes. When the state is s₀, ∥GPo (⋄ B) ∥ _max (s₀) =0.2, ∥GPo (⋄ B) ∥ _min (s₀) =0.2, which indicates that the patient is in a bad state of health and is already in a state of illness. For state s₂, ∥GPo (⋄ B) ∥ _max (s₂) =0.9, ∥GPo (⋄ B) ∥ _min (s₂) =0.7, which indicates that the patient’s state health has been in a “good” state.

5 Reachability in the safety properties

The analysis of safety properties and the techniques for checking safety properties are closely related to reachability. Safety properties are often characterized as “nothing bad should happen”. In classic model checking, safety properties are defined as linear property which does not include a bad prefix, and analyses the eventual reachability and repeated reachability. Since it is difficult to define the notion of a bad prefix in fuzzy logic or possibility logic, Li [21] uses the good prefixes to define the fuzzy safety property, and computes the always reachability possibility and persistent reachability possibility. In the following section, we use the good prefixes to analyze the possibilistic of regular safety property.

For a GPDP M = (S, Act, P, I, AP, L), we assume the alphabet Σ = l^AP for some finite subset l ⊆ [0, 1] in the following.

Definition 11.c4:def1 For the safety property P_safe, we define a possibilistic language Gref (P_safe) : Σ^* ⟶ [0, 1] as Gpref (P_safe) (θ) = ⋁ {P_safe (θσ) ∣ σ ∈ Σ^ω}. For all θ ∈ Σ^*, Gpref (P_safe) is called the good prefixes of P_safe.

P_safe is called possibilistic regular safety property if P_safe (σ) = ⋀ {Gpref (P_safe) (θ) ∣ θ ∈ Gpref (σ) }, for all σ ∈ Σ^ω, Pref (σ) = {θ ∈ Σ^* ∣ σ = θσ′, σ′ ∈ Σ^ω} is called the set of prefixes of σ.

We call P_safe a generalized possibilistic regular safety property if P_safe is a generalized possibilistic safety property and Gpref (P_safe) is a fuzzy regular language over Σ.

Definition 12. [22] A fuzzy finite automata is a five tuple A = (Q, Σ, δ, Q₀, F), where

Q is a finite nonempty set of states;

Σ a finite nonempty set of input symbols;

δ : Q × Σ × Q ⟶ [0, 1] is a fuzzy transition function. For any p, q ∈ Q, a ∈ Σ, δ (p, a, q) denotes the possibility of state p reaching state Q under the action of input letter a;

Q₀ : Q ⟶ [0, 1] represent the fuzzy initial state of fuzzy automata A,for q ∈ Q,Q₀ (q) denotes q is the possibility of the initial state;

F : Q ⟶ [0, 1] represent the fuzzy acceptance state of fuzzy automata A,F (q) denotes q is the possibility of the acceptance state;

For a GPDP M = (S, Act, P, I, AP, L) and a fuzzy finite automata A = (Q, Σ, δ, Q₀, F), the product of M and A is defined as follows.

Definition 13. Let M = (S, P, Act, I, AP, L) be a GPDP, A = (Q, Σ, δ, Q₀, F) be a fuzzy finite automata, M ⊗ A = (S × Q, P′, Act′, I′, AP′, L′), where P′ (< s, q > , α, < s′, q′ >) = P (s, α, s′) ∧ δ (q, L (s′) , q′); Act′ (< s, q >) = Act (s); I′ (< s, q >) = I (s) ∧ ⋁ _q₀∈QQ₀ (q₀) ∧ δ (q₀, L (s) , q); for all <s, q > ∈ S × Q, AP′ = S × Q; L′ (< s, q >) = < s, q >.

For each path π = s₀ α₀s₁ α₁s₂ α₂ … ∈ Paths_Adv (M) in M, Trace_Adv (π) = L (s₀) L (s₁) L (s₂)…, the fuzzy automata A has a unique run q₀q₁q₂… and in M ⊗ A there exists π⁺ =< s₀, q₁ > α₀ < s₁, q₂ > α₁ … corresponding to them.Similarly, the path in M ⊗ A with state <s₀, δ (q₀, L (s))> also corresponds to the path in M and the run in A.

Theorem 8.Let M = (S, Act, P, I, AP, L) be a GPDP, P_safe is the generalized possibilistic regular safety property accepted by a deterministic fuzzy finite automata A = (Q, Σ, δ, Q₀, F), and Adv is the set of all strategies begin state s. We have:

${GPo}_{Adv}^{M} (s ⊨ P_{safe}) = {GPo}_{Adv}^{M \otimes A} (< s, q_{s} > ⊨ B),$ (16) where q_s = δ (q₀, L (s)), B = S× F = ∑_s∈S,q∈QF (q)/< s, q >, which means that B (< s, q >) = F (q), for all <s, q > ∈ S × Q.

Proof. See the Appendix. ■

Let GPo_Adv ( B) = GPo_Adv (s ⊨ B) _s∈S, then

GPo_Adv ( B) can be solved by the maximum fixed point, where the maximum fixed point of the operator is f_B (Z) = B ∧ P_Adv ∘ D_Z ∘ r_Adv. For the scheduler Adv taking the maximum possibility scheduler max and the minimum possibility scheduler min, the maximum possibility and the minimum possibility that the state s satisfies the generalized possibilistic regular safety property P are respectively: $\begin{matrix} {GPo}_{\max} (B) = ({GPo}_{\max} (s ⊨ B))_{s \in S} \\ = υ Z . f_{Bmax} (Z), \end{matrix}$ (17) $\begin{matrix} {GPo}_{\min} (B) = ({GPo}_{\min} (s ⊨ B))_{s \in S} \\ = υ Z . f_{Bmin} (Z), \end{matrix}$ (18) where $\begin{matrix} f_{Bmax} (Z) = B \land P_{\max} \circ D_{Z} \circ r_{\max}, \\ f_{Bmin} (Z) = B \land P_{\min} \circ D_{Z} \circ r_{\min} . \end{matrix}$

Example 10. We use Example 1 as a sample. To discuss the generalized possibility measure of generalized possibilistic regular safety property in the alphabet Σ = l^AP, in which $l = {0, 0.1, 0.2, 0.3, 0.4, 0.5, 0.6, 0.7, 0.8, 0.9, 1} .$ Generalized possibilistic regular safety property P_safe = {A₀, A₁, … ∈ Σ^ω ∣ ∀ i ≥ 0, A_i (E) >0} a describes the patient’s health states is good (E). Because the safety property P_safe has a good prefix Gref (P_safe) = {A₀, A₁, …, A_n ∈ Σ^* ∣ n ≥ 0, ∀ i ≥ 0, A_i (E) >0}, and for any infinite words δ ∈ Σ^ω, if w ∈ Pref (δ), w ∈ Gref (P_safe), then δ ∈ P_safe. Gref (P_safe) can be accepted by the definite finite fuzzy automata shown in the Fig. 4. Therefore, P_safe is generalized possibilistic regular safety property, where the letter E in the automata A denotes the atomic proposition for any A ∈ Σ such that A (E) >0 is an atomic proposition.

Fig. 4

Finite automata A corresponding to Gref (P_safe).

Given a GPDP M and generalized possibilistic regular safety property P_safe = {A₀, A₁, … ∈ Σ^ω ∣ ∀ i ≥ 0, A_i (E) >0}, Adv is the scheduler defined in M. The solution processes of GPo_max (s₀ ⊨ P_safe) and GPo_min (s₀ ⊨ P_safe) corresponding to Adv is the maximum scheduler and the minimum scheduler are given.

The product M ⊗ A of a GPDP M and P_safe good prefix Gref (P_safe) corresponding to a finite automata A is shown in Fig. 5. According to formulas 17 and 18, there B = S × {q₁} = {1, 1, 1} is

Fig. 5

Product GPDPs M ⊗ A.

$\begin{matrix} f (z_{1}) = B \land (P_{\max}^{*} \circ D_{z} \circ r_{\max}) \\ = (\begin{matrix} 1 \\ 1 \\ 1 \end{matrix}) \land \\ ({(\begin{matrix} 0.8 & 0.8 & 0.3 \\ 0.5 & 0.9 & 0.9 \\ 0.3 & 0.8 & 1 \end{matrix})}^{*} \circ (\begin{matrix} 1 & 0 & 0 \\ 0 & 1 & 0 \\ 0 & 0 & 1 \end{matrix}) \circ (\begin{matrix} 0.8 \\ 0.9 \\ 1 \end{matrix})) \\ = (\begin{matrix} 0.8 \\ 0.9 \\ 1 \end{matrix}), \end{matrix}$ $\begin{matrix} f (z_{2}) = B \land (P_{\max}^{*} \circ D_{z_{1}} \circ r_{\max}) \\ = (\begin{matrix} 1 \\ 1 \\ 1 \end{matrix}) \land \\ ({(\begin{matrix} 0.8 & 0.8 & 0.3 \\ 0.5 & 0.9 & 0.9 \\ 0.3 & 0.8 & 1 \end{matrix})}^{*} \circ (\begin{matrix} 0.8 & 0 & 0 \\ 0 & 0.9 & 0 \\ 0 & 0 & 1 \end{matrix}) \circ (\begin{matrix} 0.8 \\ 0.9 \\ 1 \end{matrix})) \\ = (\begin{matrix} 0.8 \\ 0.9 \\ 1 \end{matrix}), \end{matrix}$

fz₁ = fz₂, Therefore $\begin{matrix} {GPo}_{\max} (B) = (\begin{matrix} 0.8 \\ 0.9 \\ 1 \end{matrix}) . \end{matrix}$

Calculated by the same method $\begin{matrix} {GPo}_{\min} (B) = (\begin{matrix} 0.3 \\ 0.5 \\ 0.7 \end{matrix}) . \end{matrix}$

GPo_max (s₀ ⊨ P_safe) =0.8,GPo_min (s₀ ⊨ P_safe) =0.3 are obtained, which shows that the maximum possibility and minimum possibility of generalized possibilistic regular safety property P_safe in GPDPs M are 0.8 and 0.3.

6 Conclusion

In this paper, firstly, we propose GPDPs as the models of nondeterministic and concurrent fuzzy systems. Then, we give fuzzy matrices calculation methods of the maximal possibilities and the minimal possibilities of reachabilities. Finally, we propose a model checking approach to convert the verification of safety property into the analysis of reachabilities. We have given the method of optimization algorithm for reachability. In the future, we will investigate the optimization algorithm for reachability to solve the verification of other properties, such as liveness and fairness in fuzzy systems.

Acknowledgments

The work is partially supported by National Natural Science Foundation of China(Grant No. 61962001), Graduate Innovation Project of North Minzu University(Grant No. YCX22184 and No. YCX22196).

Appendix

Proof. [Proof of Theorem 1]

Since S and Act is finite, given the scheduler Adv, the possibility transition matrix P_Adv is also finite. Obviously, the fuzzy meet operator ∧ does not generate new element,so the set ${\underset{i \geq 0}{\land} P_{Adv} (s_{i}, α_{i}, s_{i + 1}) ∣ s_{i} \in S, α_{i} \in Act}$ is finite.Since S and Act is finite, for any states s ∈ S under consideration of the scheduler Adv, there exits t ∈ S and i < j so that s_i = s_j = t.

In this case, P_Adv (s, α₀, s₁)∧ P_Adv (s₁, α₁, s₂) ∧ ⋯

= P_Adv (s, α₀, s₁) ∧ ⋯ ∧ P_Adv (s_i-1, α_i-1, t) ∧ (P_Adv (t, α_i, s_i+1)

∧⋯ P_Adv (s_j-1, α_j, t)) ∧ ⋯

≤P_Adv (s, α₀, s₁) ∧ ⋯ ∧ P_Adv (s_i-1, α_i-1, t) ∧ (P_Adv (t, α_i, s_i+1)

∧ ⋯ ∧ P_Adv (s_j-1, α_j, t))

$\leq P_{Adv}^{+} (s, Act (s), t) \land P_{Adv}^{+} (t, Act (t), t)$ .

Hence, $r_{Adv} (s) \leq P_{Adv}^{+} (s, Act (s), t) \land P_{Adv}^{+} (t, Act (t), t)$ .

Conversely, for any t ∈ S and schedulers Adv, by the definition of $P_{Adv}^{+}$ , there exists ss₁ ⋯ s_i = t ∈ S and s_i+1 ⋯ s_j such that

$P_{Adv}^{+} (s, t) = P_{Adv} (s, s_{1}) \land \dots \land P_{Adv} (s_{i - 1}, t)$

$P_{Adv}^{+} (t, t) = P_{Adv} (t, s_{1}) \land \dots \land P_{Adv} (s_{j}, t)$ .

Let π_Adv = s₀ α₀s₁ α₁ ⋯ s_i-1 α_i-1tα_i (s_i+1 ⋯ s_j α_jt) ^ω,then $P_{Adv}^{+} (s, t) \land P_{Adv}^{+} (t, t) = P_{Adv} (s, s_{1}) \land P_{Adv} (s_{1}, s_{2}) \land \dots .$

Hence, $P_{Adv}^{+} (s, t) \land P_{Adv}^{+} (t, t) \leq r_{Adv} (s)$ , $⋁ {P_{Adv}^{+} (s, t) \land P_{Adv}^{+} (t, t) ∣ t \in S} \leq r_{Adv} (s) .$

Therefore, $r_{Adv} (s) = \lor {P_{Adv}^{+} (s, t) \land P_{Adv}^{+} (t, t) ∣ t \in S}$ .

Proof. [Proof of Theorem 2]

From $Cyl (\hat{π}) = {π \in Path s_{Adv} (M) ∣ \hat{π} \in Pref (π)}$ , we have Cyl (s₀ α₀s₁ α₁ ⋯ α_n-1s_n) = ⋃ {π_Adv ∈ Paths_Adv (M) ∣ s₀ α₀ ⋯ α_n-1s_n ∈ Pref (π_Adv)} .

Therefore, GPo (Cyl (s₀ α₀ ⋯ α_n-1s_n) )

= ⋁ {GPo (π_Adv) ∣ s₀ α₀ ⋯ α_n-1s_n ∈ Pref (π_Adv)}

$= ⋁ {I (s_{0}) \land \underset{i \geq 0}{⋀} P_{Adv} (s_{i}, α_{i}, s_{i + 1}) ∣ s_{0} α_{0} s_{1} \dots α_{n - 1} s_{n} \in Pref (π_{Adv})} = {I (s_{0}) \land ⋀_{i = 0}^{n - 1} P_{Adv} (s_{i}, α_{i}, s_{i + 1})} \land ⋀ {\underset{j \geq n}{⋀} P_{Adv} (s_{j}, α_{j}, s_{j + 1})}$

$= I (s_{0}) \land ⋀_{i = 0}^{n - 1} P_{Adv} (s_{i}, α_{i}, s_{i + 1})} \land r_{Adv} (s_{n}) .$

Proof. [Proof of Theorem 3]

GPo_max (s ⊨ ⋄ B)

= ⋁ _{π∈Paths_max(s)} (GPo_max (π) ∧ ∥ ⋄ B ∥ (π) )

$= ⋁ (⋀_{i = 0}^{\infty} ⋁_{α_{i} \in Act} P (s_{i}, α_{i}, s_{i + 1}) \land ⋁_{j = 0}^{\infty} B (s_{j}))$

$= ⋁ ⋁_{i = 0}^{\infty} (P_{\max} (s, s_{1}) \land \dots \land P_{\max} (s_{i - 1}, s_{i}) \land B (s_{i})) \land ⋁ ⋀_{j = i}^{\infty} P_{\max} (s_{j}, s_{j + 1})$

$= ⋁_{i = 0}^{\infty} ⋁ (P_{\max} (s, s_{1}) \land \dots \land P_{\max} (s_{i - 1}, s_{i}) \land B (s_{i}) \land r_{\max} (s_{i}))$

$= ⋁_{i = 0}^{\infty} (P_{\max}^{i} \circ D_{B} \circ r_{\max}) (s)$

$= ((⋁_{i = 0}^{\infty} P_{\max}^{i}) \circ D_{B} \circ r_{\max}) (s)$

$= (P_{\max}^{*} \circ D_{B} \circ r_{\max}) (s)$

where P_maxis the maximum possibility transition matrix under the max scheduler, Kleene closure of P_max is $P_{\max}^{*}$ , D_B is the diagonal matrix diag (B (s)) _s∈S, $r_{\max} = P_{\max}^{+} \circ D$ , $P_{\max}^{+} = P_{\max} \lor P_{\max}^{*}$ , $D = (P_{\max}^{+} (t, t))_{t \in S}$ .

GPo_min (s ⊨ ⋄ B)

= ⋁ _{π∈Paths_min(s)} (GPo_min (π) ∧ ∥ ⋄ B ∥ (π) )

$= ⋁ (⋀_{i = 0}^{\infty} ⋀_{α_{i} \in Act} P (s_{i}, α_{i}, s_{i + 1}) \land ⋁_{j = 0}^{\infty} B (s_{j}))$

$= ⋁ ⋁_{i = 0}^{\infty} (P_{\min} (s, s_{1}) \land \dots \land P_{\min} (s_{i - 1}, s_{i}) \land B (s_{i})) \land ⋁ ⋀_{j = i}^{\infty} P_{\min} (s_{j}, s_{j + 1})$

$= ⋁_{i = 0}^{\infty} ⋁ (P_{\min} (s, s_{1}) \land \dots \land P_{\min} (s_{i - 1}, s_{i}) \land B (s_{i}) \land r_{\min} (s_{i}))$

$= ⋁_{i = 0}^{\infty} (P_{\min}^{i} \circ D_{B} \circ r_{\min}) (s)$

$= ((⋁_{i = 0}^{\infty} P_{\min}^{i}) \circ D_{B} \circ r_{\min}) (s)$

$= (P_{\min}^{*} \circ D_{B} \circ r_{\min}) (s),$

where P_min is the minimum possibility transition matrix under the min scheduler.

Proof. [Proof of Theorem 5]

GPo_max (s ⊨ C ⊔ ^≤nB) = ⋁ _{π∈Paths_max(s)} (GPo_max (π) ∧ ∥ C ⊔ ^≤nB ∥ (π) )

= ⋁ (⋁ _{α₀∈Act(s₀)}P (s₀, α₀, s₁) ∧ ⋁ _{α₁∈Act(s₁)}P (s₁, α₁, s₂)

$\land \dots \land (⋁_{j \geq 0}^{n} B (s_{j}) \land ⋀_{i \leq j} C (s_{i})))$

$= ⋁ (P_{\max} (s_{0}, s_{1}) \land P_{\max} (s_{1}, s_{2}) \land \dots \land (⋁_{j \geq 0}^{n} B (s_{j}) \land ⋀_{i \leq j} C (s_{i})))$

$= (B (s_{0}) \land r_{\max} (s_{0})) \lor (⋁_{j \geq 0}^{n} C (s_{j}) \land ⋀_{i \leq j} P_{\max} (s_{i - 1}, s_{i}) \land C (s_{i}) \land P_{\max} (s_{j - 1}, s_{j}) \land B (s_{j}) \land r_{\max} (s_{j}))$

$= (⋁_{i = 0}^{n} (D_{C} \circ P_{\max})_{i} \circ D_{B} \circ r_{\max}) (s) .$

GPo_min (s ⊨ C ⊔ ^≤nB)

= ⋁ _{π∈Paths_min(s)} (GPo_min (π) ∧ ∥ C ⊔ ^≤nB ∥ (π) )

$= ⋁ (⋀_{α_{0} \in Act (s_{0})} P (s_{0}, α_{0}, s_{1}) \land ⋀_{α_{1} \in Act (s_{1})} P (s_{1}, α_{1}, s_{2}) \land \dots \land (⋁_{j \geq 0}^{n} B (s_{j}) \land ⋀_{i \leq j} C (s_{i})))$

$= ⋁ (P_{\min} (s_{0}, s_{1}) \land P_{\min} (s_{1}, s_{2}) \land \dots \land (⋁_{j \geq 0}^{n} B (s_{j}) \land ⋀_{i \leq j} C (s_{i})))$

$= (B (s_{0}) \land r_{\min} (s_{0})) \lor (⋁_{j \geq 0}^{n} C (s_{j}) \land ⋀_{i \leq j} P_{\min} (s_{i - 1}, s_{i}) \land C (s_{i}) \land P_{\min} (s_{j - 1}, s_{j}) \land B (s_{j}) \land r_{\min} (s_{j}))$

$= (⋁_{i = 0}^{n} (D_{C} \circ P_{\min})_{i} \circ D_{B} \circ r_{\min}) (s) .$

Proof. [Proof of Theorem 6]

GPo_Adv (s ⊨ ⋄ B) = ⋁ _{π∈Paths_Adv(s)} (GPo (π) ∧ ∥ ⋄ B ∥ (π) ). Let π = s₀ α₀s₁ α₁ … ∈ Paths_Adv (s₀), inf (π) denotes the set of states that occur infinitely many times on the path π, then ∥ ⋄ B ∥ (π) ≤ ⋁ _t∈inf(π)B (t). Furthermore, for any t ∈ inf (π), π ⊨ ⋄ t, we can get GPo_Adv (π) ≤ GPo_Adv ({π ∈ Paths_fin (s) ∣ π ⊨ ⋄ t} ) , thus GPo_Adv (π) ∧ ∥ ⋄ B ∥ (π) ≤ ⋁ _t∈inf(π) > (B (t) ∧ GPo_Adv (s ⊨ ⋄ t) ) ≤ ⋁ _t∈S (B (t) ∧ GPo_Adv (s ⊨ ⋄ t) ) . Therefore, GPo_Adv (s ⊨ ⋄ B) ≤ ⋁ _t∈S (B (t) ∧ GPo_Adv (s ⊨ ⋄ t) ) .

Conversely, for any state t ∈ S, and any path π ∈ Paths_Adv (s) that satisfies the event ⋄ t,we have B (s) ≤ ∥ ⋄ B ∥ (π). It follows that ⋁_t∈S (B (t) ∧ GPo_Adv (s ⊨ ⋄ t) ) ≤ ⋁ _t∈S (B (t) ∧ GPo_Adv (s ⊨ ⋄ t) ), therefore, ⋁_t∈S (B (t) ∧ GPo_Adv (s ⊨ ⋄ t) ) ≤ GPo_Adv (s ⊨ ⋄ B).

In conclusion, GPo_Adv (s⊨ ⋄ B) = ⋁ _t∈SB (t) ∧

GPo_Adv (s ⊨ ⋄ t) .

We can get the method to calculate GPo_Adv (s ⊨ ⋄ t) from these results, that is ${GPo}_{Adv} (s ⊨ ⋄ t) = P_{Adv}^{+} (s, t) \land P_{Adv}^{+} (t, t)$ . Then we obtain ${GPo}_{Adv} (s ⊨ ⋄ B) = ⋁_{t \in S} B (t) \land P_{Adv}^{+} (s, t) \land P_{Adv}^{+} (t, t) .$

When the Adv is the maximum possibility scheduler and the minimum possibility scheduler, we can get Theorem 6.

Proof. [Proof of Theorem 7]

GPo_max (s ⊨ ⋄ B)

= ⋁ _{π∈Paths_max(s)} (GPo_max (π) ∧ ∥ ⋄ B ∥ (π) )

$= ⋁ ({GPo}_{\max} (π) \land ⋁_{i = 0}^{\infty} ⋀_{j = i}^{\infty} B (s_{j}))$

$= ⋁ ⋁_{i = 0}^{\infty} (⋁_{α_{0} \in Act} P (s, α_{0}, s_{1}) \land ⋁_{α_{1} \in Act} P (s_{1}, α_{1}, s_{2}) \land \dots \land ⋁_{α_{i - 1} \in Act} P (s_{i - 1}, α_{i - 1}, s_{i}) \land B (s_{i}) \land ⋁_{α_{i} \in Act} P (s_{i}, α_{i}, s_{i + 1})$

∧B (s_i+1) ∧ ⋁ _{α_i+1∈Act}P (s_i+1, α_i+1, s_i+2) ∧ B (s_i+2) ∧ … )

$= ⋁ ⋁_{i = 0}^{\infty} (P_{\max} (s, s_{1}) \land P_{\max} (s_{1}, s_{2}) \land \dots \land P_{\max} (s_{i - 1} s_{i}) \land B (s_{i}) \land P_{\max} (s_{i}, s_{i + 1}) \land B (s_{i + 1}) \land P_{\max} (s_{i + 1}, s_{i + 2}) \land$

B (s_i+2) ∧ … )

$= ⋁ ⋁_{i = 0}^{\infty} (P_{\max} (s, s_{1}) \land P_{\max} (s_{1}, s_{2}) \land \dots \land P_{\max} (s_{i - 1} s_{i})$

∧ (D_max ∘ P_max) (s_i, s_i+1) ∧ (D_max ∘ P_max) (s_i+1, s_i+2)

∧ … )

$= ⋁ ⋁_{i = 0}^{\infty} (P_{\max} (s, s_{1}) \land P_{\max} (s_{1}, s_{2}) \land \dots \land P_{\max} (s_{i - 1} s_{i})$

∧r_{D_B∘P_max} (s_i) )

$= ⋁_{i = 0}^{\infty} (⋁_{s_{i} \in S} (P_{\max} (s, s_{1}) \land P_{\max} (s_{1}, s_{2}) \land \dots) \land$

P_max (s_i-1s_i) ∧ r_{D_B∘P_max} (s_i) )

$= ⋁_{i = 0}^{\infty} (P_{\max}^{i} \circ r_{D_{B} \circ P_{\max}} (s)) = (⋁_{i = 0}^{\infty} P_{\max}^{i}) \circ r_{D_{B} \circ P_{\max}} (s)$

$= P_{\max}^{*} \circ r_{D_{B} \circ P_{\max}} (s),$

GPo_min (s ⊨ ⋄ B)

= ⋁ _{π∈Paths_min(s)} (GPo_min (π) ∧ ∥ ⋄ B ∥ (π) )

$= ⋁ ({GPo}_{\min} (π) \land ⋁_{i = 0}^{\infty} ⋀_{j = i}^{\infty} B (s_{j}))$

$= ⋁ ⋁_{i = 0}^{\infty} (⋀_{α_{0} \in Act} P (s, α_{0}, s_{1}) \land ⋀_{α_{1} \in Act} P (s_{1}, α_{1}, s_{2}) \land \dots \land ⋀_{α_{i - 1} \in Act} P (s_{i - 1}, α_{i - 1}, s_{i}) \land B (s_{i}) \land ⋀_{α_{i} \in Act} P (s_{i}, α_{i}, s_{i + 1}) \land B (s_{i + 1}) \land ⋀_{α_{i + 1} \in Act} P (s_{i + 1}, α_{i + 1}, s_{i + 2}) \land B (s_{i + 2}) \land \dots)$

$= ⋁ ⋁_{i = 0}^{\infty} (P_{\min} (s, s_{1}) \land P_{\min} (s_{1}, s_{2}) \land \dots \land P_{\min} (s_{i - 1} s_{i}) \land B (s_{i}) \land P_{\min} (s_{i}, s_{i + 1}) \land B (s_{i + 1}) \land P_{\min} (s_{i + 1}, s_{i + 2}) \land B (s_{i + 2}) \land \dots)$

$= ⋁ ⋁_{i = 0}^{\infty} (P_{\min} (s, s_{1}) \land P_{\min} (s_{1}, s_{2}) \land \dots \land P_{\min} (s_{i - 1} s_{i}) \land (D_{\min} \circ P_{\min}) (s_{i}, s_{i + 1}) \land (D_{\min} \circ P_{\min}) (s_{i + 1}, s_{i + 2}) \land \dots)$

$= ⋁ ⋁_{i = 0}^{\infty} (P_{\min} (s, s_{1}) \land P_{\min} (s_{1}, s_{2}) \land \dots \land P_{\min} (s_{i - 1} s_{i}) \land r_{D_{B} \circ P_{\min}} (s_{i})) = ⋁_{i = 0}^{\infty} (⋁_{s_{i} \in S} (P_{\min} (s, s_{1}) \land P_{\min} (s_{1}, s_{2}) \land \dots) \land P_{\min} (s_{i - 1} s_{i}) \land r_{D_{B} \circ P_{\min}} (s_{i}))$

$= ⋁_{i = 0}^{\infty} (P_{\min}^{i} \circ r_{D_{B} \circ P_{\min}} (s)) = (⋁_{i = 0}^{\infty} P_{\min}^{i}) \circ r_{D_{B} \circ P_{\min}} (s) = P_{\min}^{*} \circ r_{D_{B} \circ P_{\min}} (s) .$

Proof. [Proof of Theorem 8]

${GPo}_{Adv}^{M} (s ⊨ P_{safe})$

= ⋁ _{π∈Paths_Adv(s)} (GPo_Adv (π) ∧ P_safe (Trace_Adv (π)) )

= ⋁ (GPo_Adv (π) ∧ ⋀ _j≥0 {L (A) (θ) ∣ θ ∈ Pref (Trace_Adv (π)) } )

= ⋁ (GPo_Adv (π) ∧ ⋀ _j≥0 {F (q_j) ∣ q_jδ^* (q₀, L (s) L (s₁) … L (s_j)) } ) ⋁ (GPo_Adv (π) ∧ ⋀ _i≥0F (q_i) ) .

For π = sα₀s₁ α₁ … ∈ Paths_Adv (s), we define the run sequence q₀q₁q₂… of the deterministic fuzzy finite automata by q_i+1 = δ (q_i, L (s_i)). Vice versa, for the same run sequence q₀q₁q₂… of the deterministic fuzzy finite automata, we have

${GPo}_{Adv}^{M \otimes A} (< a, q_{s} > ⊨ B)$

= ⋁ _{π⁺∈Paths_Adv(<s,q_s>)} (GPo_Adv (π⁺) ∧ ⋀ _i≥0B (π⁺ [i]) )

= ⋁ _{π∈Paths_Adv(s)} (GPo_Adv (π) ∧ ⋀ _i≥0F (q_i) ) ,

References

Mahmood

A Verification Framework for ComponentBased Modeling and Simulation Putting the pieces together[J], arXiv preprint arXiv:2301.03088, 2023.

Pan

, Li

, Cao

et al. Model checking fuzzy computation tree logic[J]. Fuzzy sets and Systems 262 (2015), 60–77.

Laroussinie

et al. Principles of Model Checking[J]. The Computer Journal 53(5) (2010), 615–616.

Hansen

H.A.

, Schneider

and Steffen

, Reachability analysis of complex planar hybrid systems[J]. Science of Computer Programming 78(12) (2013), 2511–2536.

Herbert

S.L.

, Bansal

, Ghosh

et al. Reachability-based safety guarantees using efficient initializations[C], 2019 IEEE 58th Conference on Decision and Control (CDC), IEEE, 2019, 4810–4816.

Wang

, Deng

and Xu

, Reachability analysis of real-time systems using time Petri nets. IEEE Trans Syst Man Cybern B Cybern 30(5) (2000), 725–736. doi: 10.1109/3477.875448. PMID: 18252405

Bouyer

, Markey

, Randour

et al. Reachability in networks of register protocols under stochastic schedulers[J], arXiv preprint arXiv:1602.05928, 2016.

Xie

, Xiong

, Bu

et al. Deriving unbounded reachability proof of linear hybrid automata during bounded checking procedure[J]. IEEE Transactions on Computers 66(3) (2016), 416–430.

Ganguli

, Iyer

C.V.K.

, Pandey

Reachability Embeddings: Scalable Self-Supervised Representation Learning from MobilityTrajectories for Multimodal Geospatial Computer Vision[C], 2022 23rd IEEE International Conference on Mobile Data Management (MDM), IEEE, 2022, 44–53.

10.

Song

Y.H.

, Shahid

and Chung

E.S.

, Differences in multi-model ensembles of CMIP5 and CMIP6 projections for future droughts in South Korea[J]. International Journal of Climatology 42(5) (2022), 2688–2716.

11.

, Droste

and Lei

, Model checking of linear-time properties in multi-valued systems[J]. Information Sciences 377 (2017), 51–74.

12.

, Li

et al. Model Checking Fuzzy Computation Tree Logic Based on Fuzzy Decision Processes with Cost[J]. Entropy 24(9) (2022), 1183.

13.

Lee

, Kim

et al. Directed Model Checking for Fast Abstract Reachability Analysis[J]. IEEE Access 9 (2021), 158738–158750.

14.

Wang

, Yuan

, Zhang

et al. Reachability-Driven Influence Maximization in Time-dependent Road-social Networks[C], 2022 IEEE 38th International Conference on Data Engineering (ICDE), IEEE, 2022, 367–379.

15.

and Koutsoukos

, Reachability analysis of uncertain systems using bounded-parameter Markov decision processes[J]. Artificial Intelligence 172(8-9) (2008), 945–954.

16.

and Koutsoukos

, Reachability analysis of uncertain systems using bounded-parameter Markov decision processes[J]. Artificial Intelligence 172(8-9) (2008), 945–954.

17.

and Li

, Model checking of linear-time properties based on possibility measure[J]. IEEE Transactions on Fuzzy Systems 21(5) (2012), 842–854.

18.

and Wei

, Possibilistic fuzzy linear temporal logic and itsmodel checking[J]. IEEE Transactions on Fuzzy Systems 29(7) (2020), 1899–1913.

19.

Jiang

, Zhang

and Ma

, The μ-calculus model-checkingalgorithm for generalized possibilistic decision process[J]. Applied Sciences 10(7) (2020), 2594.

20.

, Mp

, Sr

et al. Model-checking graded computation-tree logic with finite path semantics[J]. Theoretical Computer Science 806 (2020), 577–586.

21.

, Quantitative model checking of linear-time properties based on generalized possibility measures[J]. Fuzzy sets and Systems 320 (2017), 17–39.

22.

and Ma

, Quantitative computation tree logic model checking based on generalized possibility measures[J]. IEEE Transactions on Fuzzy Systems 23(6) (2015), 2034–2047.

23.

Ying

and Ying

, Reachability analysis of quantum Markov decision processes[J], . Information and Computation 263 (2018), 31–51.

24.

Huang

and Cleaveland

, A tableau construction for finite linear-time temporal logic[J]. Journal of Logical and Algebraic Methods in Programming 125 (2022), 100743.

25.

Quatmann

, Junges

, Katoen

J.P.

Markov automata with multiple objectives[C], International Conference on Computer Aided Verification, Springer, Cham, 2017, 140–159.

26.

Shojafar

, Javanmardi

, Abolfazli

et al. FUGE: A joint meta-heuristic approach to cloud job scheduling algorithm using fuzzy theory and a genetic method[J]. Cluster Computing 18(2) (2015), 829–844.

27.

Wei

and Li

, Fuzzy alternating automata over distributive lattices[J]. Information Sciences 425 (2018), 34–47.

28.

Madhumangal Pal Fuzzy Matrices with Fuzzy Rows and Columns, 1 Jan. 2016, 561–573.

29.

Wang

, Li

, Ying

Equivalence Checking of Sequential Quantum Circuits[J], IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2021. doi: 10.1109/TCAD.2021.3117506.

30.

Garmendia

, Salvador , Gonzĺćlez del

, Campo , Lĺöpez et al. An algorithm to compute the transitive closure, a transitive approximation and a transitive opening of a fuzzy proximity[J]. Mathware and Soft Computing 16(2) (2009), 175–191.

31.

Hartmanns

, Junges

, Katoen

J.P.

et al. Multi-cost bounded reachability in MDP[C], International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, Cham, 2018, 320–339.

32.

Chondrogiannis

, Nascimento

M.A.

, Bouros

Relative reachability analysis as a tool for urban mobility planning: Position paper[C], Proceedings of the 12th ACM SIGSPATIAL International Workshop on Computational Transportation Science, 2019, 1–4.