Quantitative reachability analysis of generalized possibilistic decision processes

1Introduction

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, 12, 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, 18, 21, 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.

2Preliminaries

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, 26, 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∈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 tij=∨k=1n(rik∧skj) , (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 ∣, R0(s,t)={1s=t0s≠t . 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:

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

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 πˆ=s0s1⋯sn .

3Generalized 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

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)=∨t∈TP(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 πˆ=s0α0s1α1s2⋯αn-1sn 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 πˆ = s₀s₁ ⋯ s_n is defined as trace( πˆ ) = 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(πˆ)∣πˆ∈Pathsfin(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 PathAdvfin(s) denote the set of paths and finite paths from state s under the decision of the scheduler Adv. Let Path_Adv (M) and PathAdvfin(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 Pmax=⋁i=0nPαi denotes the maximal possibility transition matrix, so that

Using fuzzy matrix Pmin=⋀i=0nPαi denotes the minimal possibility transition matrix, so that

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.

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 πˆ=s0α0s1α1s2⋯sn-1αn-1sn∈PathsAdvfin(M) and Adv be the max or min scheduler, then the cylinder set of the finite path πˆ is defined as

The cylinder set spanned by the finite adv-paths πˆ consists of all infinite adv-paths that start with πˆ . 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:

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:

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

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

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,

Dmax=(Pmax+(t,t))t∈S=(0.80.91),

Dmin=(Pmin+(t,t))t∈S=(0.30.50.7),

Pmax+=(0.80.80.80.50.90.90.50.81),

Pmin+=(0.30.20.10.20.50.40.20.30.7),

rmax=Pmax+∘Dmax=(0.80.91),

rmin=Pmin+∘Dmin=(0.30.50.7).

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 πˆ=s0α0s1α1⋯αn-1sn∈PathsAdvfin(M) is:

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 πˆ=s0α0s1 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 .

4Reachability 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.

5Reachability 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

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) ∧ ⋁ _q0∈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:

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:

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

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.

fz₁ = fz₂, Therefore

Calculated by the same method

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.

6Conclusion

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 {∧i≥0PAdv(si,αi,si+1)∣si∈S,αi∈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))

≤PAdv+(s,Act(s),t)∧PAdv+(t,Act(t),t) .

Hence, rAdv(s)≤PAdv+(s,Act(s),t)∧PAdv+(t,Act(t),t) .

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

PAdv+(s,t)=PAdv(s,s1)∧⋯∧PAdv(si-1,t)

PAdv+(t,t)=PAdv(t,s1)∧⋯∧PAdv(sj,t) .

Let π_Adv = s₀ α₀s₁ α₁ ⋯ s_i-1 α_i-1tα_i (s_i+1 ⋯ s_j  α_jt)  ^ω,then PAdv+(s,t)∧PAdv+(t,t)=PAdv(s,s1)∧PAdv(s1,s2)∧⋯.

Hence, PAdv+(s,t)∧PAdv+(t,t)≤rAdv(s) , ⋁{PAdv+(s,t)∧PAdv+(t,t)∣t∈S}≤rAdv(s).

Therefore, rAdv(s)=∨{PAdv+(s,t)∧PAdv+(t,t)∣t∈S} .

Proof. [Proof of Theorem 2]

From Cyl(πˆ)={π∈PathsAdv (M)∣πˆ∈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(s0)∧⋀i≥0PAdv(si,αi,si+1)∣s0α0s1⋯αn-1sn∈Pref(πAdv)}={I(s0)∧⋀i=0n-1PAdv(si,αi,si+1)}∧⋀{⋀j≥nPAdv(sj,αj,sj+1)}

=I(s0)∧⋀i=0n-1PAdv(si,αi,si+1)}∧rAdv(sn).

Proof. [Proof of Theorem 3]

GPo_max (s ⊨ ⋄ B)

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

=⋁(⋀i=0∞⋁αi∈ActP(si,αi,si+1)∧⋁j=0∞B(sj))

=⋁⋁i=0∞(Pmax(s,s1)∧…∧Pmax(si-1,si)∧B(si))∧⋁⋀j=i∞Pmax(sj,sj+1)

=⋁i=0∞⋁(Pmax(s,s1)∧…∧Pmax(si-1,si)∧B(si)∧rmax(si))

=⋁i=0∞(Pmaxi∘DB∘rmax)(s)

=((⋁i=0∞Pmaxi)∘DB∘rmax)(s)

=(Pmax*∘DB∘rmax)(s)

where P_maxis the maximum possibility transition matrix under the max scheduler, Kleene closure of P_max is Pmax* , D_B is the diagonal matrix diag (B (s)) _s∈S, rmax=Pmax+∘D , Pmax+=Pmax∨Pmax* , D=(Pmax+(t,t))t∈S .

GPo_min (s ⊨ ⋄ B)

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

=⋁(⋀i=0∞⋀αi∈ActP(si,αi,si+1)∧⋁j=0∞B(sj))

=⋁⋁i=0∞(Pmin(s,s1)∧…∧Pmin(si-1,si)∧B(si))∧⋁⋀j=i∞Pmin(sj,sj+1)

=⋁i=0∞⋁(Pmin(s,s1)∧…∧Pmin(si-1,si)∧B(si)∧rmin(si))

=⋁i=0∞(Pmini∘DB∘rmin)(s)

=((⋁i=0∞Pmini)∘DB∘rmin)(s)

=(Pmin*∘DB∘rmin)(s),

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

Proof. [Proof of Theorem 5]

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

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