Computation Tree Logic Model Checking of Multi-Agent Systems Based on Fuzzy Epistemic Interpreted Systems

1  Introduction

Model checking [1,2] is a formal method employed for the automatic verification of whether a model satisfies specific properties. This approach finds extensive application in multi-agent systems [3,4]. Property specifications for finite state systems are typically formalized using temporal logics like Computation Tree Logic (CTL) and Linear Temporal Logic (LTL) [5]. In contrast, multi-agent systems comprise interacting agents and place greater emphasis on the formalization of agents’ mental attitudes, such as knowledge, beliefs, and desires [6]. As a result, multi-agent system verification focuses on broadening the scope of classical model checking techniques by incorporating epistemic modalities that characterize agents’ knowledge and motivational attitudes.

Previous research has mainly demonstrated meta-logical outcomes across various temporal and epistemic combinations, with a particular emphasis on completeness and computational complexity. To enhance expressive capabilities, epistemic logic has undergone multi-directional expansion. In one research domain, scholars have adopted axiomatic approaches to extend temporal epistemic logic, with a focus on the meta-logical properties of the resultant logic, all without specific validation algorithms [7]. In another line of inquiry, a separate group of researchers have studied epistemic logic at the predicate level [8,9]. Recent years have seen a notable shift in research orientation towards the development of model checking techniques integrated with these formal languages, implying that researchers are moving away from traditional theorem-proving methods to the utilization of model checking methods for system verification. The knowledge in multi-agent systems has been widely modeled through the extension of temporal logic [10,11]. Despite the success of these methods in specifying and verifying multi-agent systems from different domains, current approaches overlook the uncertainty in multi-agent systems and tend to assume ideal behavior [12].

Real-world scenarios are uncertain, particularly when it comes to open systems that interact with complex environment. Uncertainties within such systems arise due to the ambiguity and limited knowledge of the environment. In such complex contexts, tools for uncertainty solving, such as probability theory [13] and fuzzy logic [14,15], become indispensable. Probability logic has been widely researched in epistemic multi-agent systems [16,17]. Epistemic itself is a complex and multifaceted concept involving numerous sources of uncertainty, including individual subjective judgments and emotions [18]. Since epistemic is often considered fuzzy, using precise probability logic for accurate description becomes nearly impossible. For instance, an individual’s perception of weather conditions could be described as ‘somewhat hot’ or ‘a bit cold,’ both expressions laden with ambiguity. It is difficult to represent such epistemic with precise probability values. Fuzzy logic is an approach for handling these situations, where fuzzy sets could be defined to capture the probabilistic uncertainty of epistemic. A fundamental model for tackling probabilistic uncertainty is by defining interpreted systems [18]. However, there is still a lack of sufficient exploration on how to effectively resolve fuzziness in epistemic multi-agent systems. Furthermore, there is currently a lack of logical language that can describe fuzzy epistemic attributes. This accentuates the importance of model checking in the context of fuzzy epistemic multi-agent systems and how to represent and verify quantified epistemic properties. Therefore, the purpose of this research is to address the verification issues of properties in fuzzy epistemic multi-agent systems.

The contributions of this paper can be divided into three major aspects: (i) the Fuzzy Computation Tree Logic of Knowledge (FCTLK) has been defined. This logical framework not only accommodates path fuzziness but also represents knowledge regarding quantification and uncertainty. Fuzzy Kripke structures (FKS) [19,20] have been combined with an interpreted system [18] for S5 epistemic logic to model fuzzy multi-agent systems. Fuzzy Kripke structures are widely applied in modeling systems with fuzziness. They serve as the formal model for Fuzzy Computation Tree Logic (FCTL); (ii) a method has been proposed to address epistemic property verification in fuzzy multi-agent systems. It employs an indirect fuzzy model checking algorithm that transforms the FCTLK model checking problem into the FCTL model checking. During this process, the fuzzy epistemic interpreted system (FEIS) is transformed into a Fuzzy Decision Process (FDP) [21] model. In addition, a scheduler is applied to eliminate the non-determinism of actions. Subsequently, the FDP model is transformed into an FKS model; (iii) the equivalence between the satisfiability of formulas in the FCTLK model and the FCTL model has been theoretically demonstrated using matrix synthesis operations. The algorithm time complexity analysis results show that formulas in FCTLK can be verified using the synthesis operations of fuzzy matrices without additional computational overheads. Furthermore, this computational process exhibits greater conciseness with improved readability.

1.1 Related Work

As an automated formal verification technique, model checking has been widely employed for the verification of various critical properties, including security [22], fairness [23], and reachability [24]. In recent years, this technique has found extensive application in the verification of multi-agent systems. Skorupski [10] proposed an efficient model checking technique that reduces the problem of Computation Tree Logic of Knowledge (CTLK) model checking in multi-modal logic to the problem of model checking Action-Restricted CTL (ARCTL) [25]. In [11], Penczek et al. introduced group knowledge and applied verification techniques using bounded model checking to validate group knowledge attributes. However, this approach solely focuses on the absolute accuracy of properties in the model and ignores the influence of stochastic phenomena on the system. Additionally, it did not consider the relationships among the three types of group knowledge. In contrast, the work presented in this paper not only considers the uncertainty of the system but also extends the scope of the study from individual agents to the entire group.

Termine et al. [16] introduced an uncertain probabilistic interpreted system model for the modelling of epistemic multi-agent systems. They proposed an iterative process-based model checking algorithm to verify multi-agent systems with non-stationary characteristics. In [17], a different approach is employed to study the model checking problem of Probabilistic Epistemic Temporal Logic (PETL) logic and propose a symbolic model checking algorithm designed for in-memory schedulers. This algorithm simplifies the model checking problem into a mixed-integer nonlinear programming problem. It demonstrates particular advantages, especially in addressing cyclic aspects within the state space. Probability model checking primarily addresses model checking problems caused by uncertainty in stochastic processes to determine the accuracy of probabilistic systems under quantitative probability specifications.

While in fuzzy systems where data is uncertain, traditional probability logic might not always work effectively. Therefore, fuzzy logic has become a specialized tool for dealing with factual imprecision, particularly demonstrating excellent performance in situations where it is difficult to describe using precious true/false values. Many scholars have suggested a type of fuzzy epistemic logic that allows evaluating the robustness of knowledge without strictly relying on probability. They have chosen possible world models as semantic models, utilizing t-norms to tackle the ambiguity of logical connectors [26,27]. In this research, interpreted system were adopted as semantic models, and fuzzy interpretations of epistemic attributes were conducted within the framework of Zadeh’s fuzzy logic.

Li et al. [28] had previously proposed a model checking approach Generalized Possibilistic Computational Tree Logic (GPoCTL) based on Generalized Possibilistic Kripke Structures (GPKS), it overlooked non-deterministic choices in fuzzy systems. Addressing this gap, Li et al. [29] employed Possibility Decision Processes (PDPs), facilitating the modeling of unpredictability in fuzzy systems, and introduced Possibility Strategy Computational Tree Logic (PoSCTL) to handle attributes with non-deterministic choices, aiming to calculate the probability of model satisfaction. In a different approach, Pan et al. [30] suggested another model checking method based on FCTL with fuzzy Kripke structures. This method emphasis the actual values of attributes, addressing a distinct form of uncertainty caused by the vagueness in conceptual expansion. Consequently, this study proposes a simplified method for fuzzy model checking by transforming fuzzy-epistemic attributes into quantifiable ones that are easier to measure and analyze. This approach aims to facilitate the verification process of epistemic attributes in intricate, fuzzy multi-agent systems.

Furthermore, Fuzzy logic is widely used across various disciplines such as budget management [31], decision-making processes [32,33], and organizational management [34,35]. For instance, it has been integrated into TOPSIS method to better handle uncertain and complex decisions, enhancing the method’s effectiveness [32,33]. In budget management, El-Morsy [31] demonstrated the application of fuzzy logic in innovating zero-based budgeting (ZBB) within ambiguous environments. This approach involved the use of triangular fuzzy numbers to depict uncertain budget data, presenting an alternative method for those seeking more precise outcomes. In organizational management, Abolfazl et al. [35] applied the fuzzy Delphi method for eliciting expert opinions on requirements, which were then organized using Kano’s model and the Alpha-cut technique, with fuzzy AHP deployed for prioritizing them. The adaptability of fuzzy logic stems from its unique ability to quantify and manage ambiguity, making it a valuable tool in numerous fields.

Table 1 provides an overview of the comparison between this study and previous research in terms of formalization, uncertainty, complexity analysis, knowledge, group knowledge, and verification. It highlights the limitations of earlier works [7–9,16,17,22,25–31] in addressing the validation issues of attributes in fuzzy epistemic multi-agent systems.

2  Preliminaries

To model and validate fuzzy epistemic multi-agent systems, we offer essential knowledge, including fuzzy sets, fuzzy set operations, fuzzy matrix operations, and group epistemic accessibility relations.

Definition 1 ([36]). Let X be a universal set. A fuzzy set A of X is a function that associates each element in X with 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 ℱ(X) to represent all fuzzy sets in X, i.e., ℱ(X)={A|A:X→[0,1]}

Definition 2 ([36]). Let A,B∈ℱ(X), we use A∪B, A∩B, 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)}

Definition 3 ([37]). Let R be a fuzzy matrix with m rows and n columns, S be a fuzzy matrix with n rows and l columns, i.e., R=(rij)m×n,S=(sij)n×l. The composition operation of R and S is R∘S=(tij)m×l, where tij=∨k=1n(rik∧skj),(i=1,2,⋯,m,j=1,2,⋯,l). For fuzzy matrixes R, S, T the composition operation has some laws.

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

Definition 4 ([38]). Group Epistemic Accessibility Relations.

(1) ≈EΩ =∪i∈Ω≈i is the union of epistemic accessibility relation for each agent in the group Ω.

(2) ≈CΩ is the transitive closure of ≈EΩ.

(3) ≈DΩ =∩i∈Ω≈i is the intersection of epistemic accessibility relation for each agent in the group Ω.

3  Models Description

3.1 Interpreted System

The interpreted system is a framework used to model the interactions among multiple autonomous agents, with the aim of describing the temporal evolution process among these agents. The specific formal definition is as follows:

Definition 5([18]). An interpreted system (IS) is composed of n agents Agt={1,…,n} that can interact with each other. The IS can be formally defined as IS=((Li,acti,Pi)i∈Agt,G,g0,Act,τ), where

(1) Each agent i∈Agt is characterized by countable sets Li and acti of local states and actions, respectively, in which the set acti is mainly used to account for the temporal evolution of the system. Also, a given local state, li∈Li represents the state of agent i at a certain moment. In addition, based on a local protocol Pi:Li→2Acti, each agent assigns a set of enabled local actions to each local state,

(2) G⊆L1×L2×⋅⋅⋅×Ln, where a state g=(l1,l2,⋯ln)∈G can be seen as the instant state of all agents in the system at a given time,

(3) g0 is the initial state,

(4) Act=act1×act2×…×actn is the set of joint actions that all agents in the system, where can execute, ∂=(∂1,∂2,∂3,⋯∂n)∈Act,

(5) τ:G×Act×G→{0,1} is the transition function of the time evolution process. For each g∈G, ∂∈Act there exists g′∈G such that τ(g,∂,g′)=1.

3.2 Fuzzy Kripke Structures

Kripke structures are fundamental models commonly used in model checking. When conducting fuzzy model checking, we extend the concept of fuzzy Kripke structures, defined as follows:

Definition 6 ([19,20]) A fuzzy Kripke structure (FKS) is a tuple K=(S,P,s0,AP,L), where

(1) S is a countable, non-empty set of states,

(2) P:S×S→[0,1] is the fuzzy transition. For each s∈S, there exist t∈S such that P(s,t)>0,

(3) s0 is the initial state,

(4) AP is the set of atomic propositions,

(5) L:S×AP→[0,1] is a fuzzy labeling function. L(s,p) is the truth value to the atomic proposition p in state s.

3.3 Fuzzy Epistemic Interpreted System

We will integrate fuzzy Kripke structures with an interpreted system to construct a fuzzy epistemic interpreted system (FEIS) for modeling fuzzy epistemic multi-agent systems. The formal definition of the FEIS model is as follows:

Definition 7. FEIS is a six-tuple consisting of a set of n agents Agt={1,…,n} that can interact. The FEIS can be formally defined as M=(G,g0,δ,AP,ℓ,≈i), where the definitions of G, and g0 are the same as before defined in IS (see Definition 5). The main distinction between IS and FEIS lies in the fact that in FEIS, three new tuples, AP, ℓ, and δ, are introduced by extending the corresponding tuples from the fuzzy Kripke structure with the inclusion of agent characteristics. Additionally, we incorporate epistemic accessibility relation ≈i to describe the knowledge of agents.

(1) δ:G×G→[0,1] is the fuzzy transition function. For each g∈G there exists g′∈G, such that δ(g,g′)>0 if and only if there exists a joint action ∂=(∂1,∂2,∂3,⋯∂n)∈Act such that δ(g,g′)=τ(g,∂,g′) in fuzzy interpreted systems,

(2) AP: Is the set of atomic propositions for n agents, where {APi}i∈Agt represents the set of atomic propositions for agent i,

(3) ℓ:Agt×G×AP→[0,1], is a fuzzy labeling function. ℓ(i,g,p) is the truth value of the atomic proposition of agent i in state s,

(4) ≈i ⊆G×G represents the epistemic accessibility relation for the agent i, p∈APi such that for two global states g0=(l1,⋯,ln) and g′=(l1‘,⋯,ln‘), we have g0≈ig′ iff ℓ(i,g,p)=ℓ(i,g′,p). The possibility value of transition between g and g′ through epistemic accessibility relations is δ(g,≈i,g′).

The fuzzy transition function δ:G×G→[0,1] can also be represented by a family of fuzzy matrixes (δ(g,g′))g,g′∈G. The possibility of moving from state g to its successors is shown on the rows δ(g,⋅) of the matrix, while the possibility of entering state g from other states is shown on the columns δ(⋅,g) of the matrix.

Computation paths: If G, ≈i and AP are finite, then it is guaranteed that M are also finite. For each g∈G there exists a state g′∈G such that δ(g,g′)>0. π^=g0g1⋯gn−1gn denotes a finite path of M. π=g0g1⋯ denotes an infinite path of M. Paths(g) denotes the set of the infinite paths which begin from state g. Paths(M) denotes the set of finite paths which begin from all states of M.

Fuzzy measure: If M=(G,g0,δ,AP,ℓ,≈i) is a finite FEIS, π=g0g1⋯∈Paths(M), ℑ⊆Paths(M), the definition of FM:2Path(M)→[0,1] is as follows:

FM(ℑ)=∨π∈ℑ(∧e≥0δ(ge,ge+1))

This function is referred to as a fuzzy measure on K=2Path(M), with K representing a sample set.

For finite M=(G,g0,δ,AP,ℓ,≈i), define r:G→[0,1] as

r(g)=∨{∧e≥0δ(ge,ge+1)|g1=g,ge∈G}

For each g∈G there exists r(g)=∨{∧e≥0δ(ge,ge+1)|g1=g,ge∈G,} represent the maximum fuzzy measure of the path starting from state g. Below is the calculation method for r.

Let M=(G,g0,δ,AP,ℓ,≈i) be a finite FEIS, for any g∈G,

r(g)=∨t∈G(δ+(g,t)∧δ+(t,t))

Using the fuzzy matrix calculation form r=δ+∘C, where C=(δ+(t,t))t∈G.

The fuzzy matrix δ induces a fuzzy space on the set of infinite paths, which start in the state g, using the cylinder construction as follows. An observation of a finite path determines a basic event (cylinder). Suppose g=g0 for π^=g0g1⋯gn, we define the fuzzy measure FMg{π^} for the π^-cylinder as follows:

FM{π^}={r(g0)if π^ consists of a  single state∧e=0n−1δ(ge,ge+1)∧r(gn)otherwise

Example 1. Fig. 1 represents a FEIS model containing two agents. G={g0,g1,g2,g3} is the set of reachable global states. APi={p},APj={q} consists of atomic propositions for agents i and j. ℓ is a fuzzy label function such that for state g0, ℓ(i,g0,p)=0.4, ℓ(j,g0,q)=0.6. For the epistemic accessibility relations, we have {(g0,g2),(g1,g2)}⊆ ≈i and {(g1,g2),(g2,g0),(g2,g3)}⊆ ≈j.

Figure 1: FEIS model M

Based on the epistemic accessibility relations of individual agents i and j, we can derive the group epistemic accessibility relations as follows:

{(g0,g2),(g1,g2),(g2,g0),(g2,g3)}⊆ ≈EΩ{(g0,g0),(g0,g2),(g0,g3),(g1,g0),(g1,g2),(g1,g3),(g2,g0),(g2,g2),(g2,g3)}⊆ ≈CΩ{(g1,g2)}⊆ ≈DΩ

The numerical values on the arrows in the diagram represent the possibility of a state transitioning to another state through epistemic accessibility relationships or joint actions. The resulting fuzzy transition function can be represented as a 4×4 matrix, as shown below:

δ=(00000.800.900.6000.30000)δ≈i=(000.70000.8000000000)δ≈j=(0000000.600.3000.40000)

4  Fuzzy Computation Tree Logic of Knowledge

To describe the specification of FEIS, we introduce FCTLK. Here we present the syntax of FCTLK and its semantic interpretation in FEIS.

Definition 8. (FCTLK syntax). Let Agt={1,…,n} be a set of agents and Ω⊆Agt be a group of agents. The FCTLK state formula is defined inductively as follows:

φ::=true|p|φ1∧φ2|¬φ|[℘]φ|FM(ψ)|𝒦

where φ and ℘ denote the state formulas, [℘]φ represents formula φ will hold true after event ℘ is announced, ψ denotes the path formulas, while 𝒦 stands for epistemic formulas. they are special state formulas within FCTLK capable of describing epistemic properties.

The following is the FCTLK path formula:

ψ::=◯φ|φ1∪φ2

where φ,φ1 and φ2 are state formulas.

• ◯φ denotes the second state on the path where φ holds.

• φ1∪φ2 denotes the existence of a state satisfying φ2 on a path, and all the states before it on the path satisfy φ1.

The following are the FCTLK social formula and epistemic formula:

𝒦::=Kiφ|EΩφ|CΩφ|DΩφ

• Kiφ, EΩφ, CΩφ and DΩφ that represent respectively “agent i knows”, “every agent in the group Ω knows”, “common knowledge”, and “distributed knowledge”.

Definition 9. (FCTLK semantics). Let M=(G,g0,δ,AP,ℓ,≈i) be a finite FIS, ‖φ‖:G→[0,1] be a function. For the FCTLK state formula φ, the semantic is defined as follows:

‖true‖(g)=1‖p‖i(g)=ℓ(i,g,p)‖φ1∧φ2‖(g)=‖φ1‖(g)∧‖φ2‖(g)

‖¬φ‖(g)=1−‖φ‖(g)‖[℘]φ‖(g)=‖℘∧φ‖(g)‖FM(ψ)‖(g)=FM(g|=ψ)‖Kiφ‖(g)=FMg{π∈Paths(g)|g≈ig′ and π=g⋯g′ and ‖φ‖g′}‖EΩφ‖(g)=FMg{π∈Paths(g)|g≈EΩg′ and π=g⋯g′ and ‖φ‖g′}‖CΩφ‖(g)=FMg{π∈Paths(g)|g≈CΩg′ and π=g⋯g′ and ‖φ‖g′}‖DΩφ‖(g)=FMg{π∈Paths(g)|g≈DΩg′ and π=g⋯g′ and ‖φ‖g′}

Given a fuzzy interpreted system model, ‖ψ‖:Paths(M)→[0,1] indicates the possibility that the path π satisfies ψ. The semantics of path formula ψ is defined below:

‖◯φ‖(π)=δ(g0,g1)∧‖φ‖(g1)‖φ1∪φ2‖(π)=‖φ2‖(g1)∨∨e>0(‖φ1‖(g0)∧∧k<e(δ(gk−1,gk)∧‖φ1‖(gk)∧δ(ge−1,ge)∧‖φ2‖(ge))

FM(g|=ψ) represents the probability of satisfying the path formula ψ starting from state g. It is defined as follows:

FM(g|=ψ)=∨π∈Paths(g)(FM(π)∧‖ψ‖(π))

5  Model Checking FCTLK Based on FEIS

Given a fuzzy multi-agent system represented as a FEIS M and a specification φ in FCTLK describing a desirable property, the problem of fuzzy model checking FCTLK is to compute the value of state g satisfying the state formula φ. Building upon the works shown in [38], this section presents an indirect fuzzy model checking method. The method consists of two main processes: Model conversion and formula simplification.

5.1 Model Conversion

During the process of model transformation, FEIS is converted into FDP. FDP is a formal model employed to depict the fuzzy and uncertain behaviors of a system, wherein there is at least one enabled action in each state. To address the issue of action uncertainty in FDP, the introduction of scheduler transforms FDP into FKS.

Before showing how to transform FEIS into an FDP, we recall the definition of the FDP model as follows:

Definition 10 ([21]). A fuzzy decision process (FDP) is a tuple F=(S,s0,AP,υ,ACT,P), where:

(1) S is a countable, non-empty set of states.

(2) s0 is the initial state.

(3) AP is the set of atomic propositions.

(4) υ:S×AP→[0,1] is a fuzzy labeling function. υ(s,p) is the truth value of the atomic proposition p in state s.

(5) ACT is the set of actions.

(6) P:S×ACT×S→[0,1] is the fuzzy transition. For each s∈S and θ∈ACT there exist t∈S which let P(s,θ,t)>0.

We say that action ACT is enabled in state s if there exists a state s‘∈S such that P(s,θ,s‘)>0. ACT(s) denotes the set of actions that can be enabled in state s.

It is evident from Definition 10 that the FDP model possesses a set of actions, ACT, which does not have an equivalent in the FEIS model. Therefore, one of the key steps in the FEIS-to-FDP transformation process is defining the set ACT. The specific approach involves transforming the transition relation and epistemic accessibility relation from M into distinct actions in F. Assuming there are n agents, 1≤i≤n and 1≤j≤n, the transition relation is marked as action ∂, and the four epistemic accessibility relations are marked as four different actions: βi, βΩE, βΩC and βΩD. The fuzzy transition P is jointly defined by transitions labeled as action ∂ and transitions labeled as actions βi, βΩE, βΩC and βΩD. The specific definition is as follows:

P:S×ACT×S→[0,1] is a fuzzy transition function for all s,s‘∈S,

P(s,θ,s‘)={τ(g,∂,g′),ifθ=∂δ(g,≈i,g′),ifθ=βiδ(g,≈EΩ,g′),ifθ=βΩEδ(g,≈CΩ,g′),ifθ=βΩCδ(g,≈DΩ,g′),ifθ=βΩD

In addition, In the process of being transformed into FDP, the states, atomic propositions, and label functions remain unchanged. Algorithm 1 describes the specific process of transforming FEIS into FDP.

Example 2. Following the model transformation rules, we convert the FEIS model in Fig. 1 into the FDP model in Fig. 2.

Figure 2: FDP model

The fuzzy transition matrix under group epistemic actions is as follows:

PβΩE=(000.70000.600.3000.40000)PβΩC=(0.300.70.40.300.60.40.300.30.40000)PβΩD=(0000000.6000000000)

To address the uncertainty of actions in FDP. We defined five different schedulers to convert FDP to FKS. The specific definition of the scheduler functions is provided below.

Definition 11. Let F=(S,s0,AP,υ,ACT,P) be a finite FDP. σ:S→ACT is a function of F. For each s∈S, there is σ(s)⊆ACT(s). We have defined σ into five different schedules. σt to be used for interpreting temporal formulae, σi, σΩE, σΩC, and σΩD are used to capture different epistemic formulas.

(1) σt:S→Act. For any state s∈Q, and given a scheduler function σt. We select the operation in the joint action set Act, i.e., σt(s)=∂. For the scheduler function σt, its fuzzy transition matrix can be defined as Pσt such that

Pσt(s,t)=P(s,σt(s),t)s,t∈S

(2) σi:S→β. For any state s∈S, and given a scheduler function σi. We select action βi i.e., σi(s)=βi. For the scheduler function σi, its fuzzy transition matrix can be defined as Pσi such that

Pσi(s,t)=P(s,σi(s),t)s,t∈S

(3) σΩE:S→βΩE. For any state s∈S, and given a scheduler function σΩE. We select action βΩE i.e., σΩE(s)=βΩE. For the scheduler function σΩE, its fuzzy transition matrix can be defined as PσΩE such that

PσΩE(s,t)=P(s,σΩE(s),t)s,t∈S

(4) σΩC:S→βΩC. For any state s∈S, and given a scheduler function σΩC. We select action βΩC i.e., σΩC(s)=βΩC. For the scheduler function σΩC, its fuzzy transition matrix can be defined as PσΩC such that

PσΩC(s,t)=P(s,σΩC(s),t)s,t∈S

(5) σΩD:S→βΩD. For any state s∈S, and given a scheduler function σΩD. We select action βΩD i.e., σΩD(s)=βΩD. For the scheduler function σΩD, its fuzzy transition matrix can be defined as PσΩD such that

PσΩD(s,t)=P(s,σΩD(s),t)s,t∈S

Under the scheduler σ, Pathsσ(s) denotes the set of paths which start from the state s, Pathsσ(F) denotes the set of paths which start from all initial states in F. By selecting different actions based on the schedule, we can obtain the FKS model of FCTL.

The FDP can be transformed into an action-determined FKS, with the transformation algorithm as follows:

Remark 1: As epistemic attributes are challenging to directly quantify and calculate, we utilize a conversion algorithm to transform fuzzy-epistemic attributes into computable quantitative attributes. Thereby transforming the model checking problem of FCTLK into the model checking problem of FCTL. Subsequently, it is essential to adapt the models and logical formulas describing system properties accordingly.

Example 3. For the FDP in Fig. 3, the scheduler functions are defined as σΩE(g0)=βΩE, σΩD(g1)=βΩD, σΩC(g2)=βΩC, and σt(g3)=∂. Fig. 3 represents the action-deterministic FKS.

Figure 3: FKS model

5.2 Formula Simplification

This section presents proofs for the equivalence relationships among three epistemic formulas and simplifies FCTLK formulas through a scheduler function. Before the formula simplification, we briefly reviewed the syntax definition of FCTL logic [30].

φ::=true|p|φ1∧φ2|¬φ|FM(ψ)ψ::=◯φ|φ1∪φ2

The state formulas and path formulas are similar to FCTLK, excluding the knowledge operator. However, the FCTL logic we are transforming differs slightly from what is presented in the literature. We have introduced the fuzzy operator FM as a replacement for the path universal quantifier and path existential quantifier in FCTL.

Before simplifying the formulas, we can establish equivalence relationships between knowledge based on the semantics and epistemic accessibility relationship of the four knowledge types, and then prove them.

Theorem 1. Equivalence among epistemic logics:

EΩφ=∧i∈ΩKiφ(1)

CΩφ=EΩφ∨EΩ2φ∨⋯∨EΩkφ(2)

DΩφ=∧i∈ΩKi([℘]φ)(3)

Proof of the first equation in Theorem 1.

Consider a set of Agt, where Ω is a subset of the Agt set and i1,i2⋯ are elements in the subset Ω. The possibility value of epistemic formula EΩφ on state g.

Therefore, the calculation of EΩφ can be done as follows:

‖EΩφ‖(g)=FMg{π∈Paths(g)|g≈EΩg′ and π=g⋯g′ and ‖φ‖g′}=FMg{π∈Paths(g)|g∪i∈Ω≈ig′ and π=g⋯g′ and ‖φ‖g′}=∨t∈G(∧h≥0P(th,βΩE,th+1)∧P(g,βΩE,t1)∧‖φ‖(t1))=∨t∈G(∧h≥0(P(th,βi1,th+1)∧P(th,βi2,th+1)∧⋯)∧(P(g,βi1,t1)∧P(g,βi2,t1)∧⋯)∧‖φ‖(t1))=∧i∈Ω∨t∈G(∧h≥0(Pσi(th,th+1))∧(Pσi(g,t1))∧‖φ‖(t1))=∧i∈Ω‖Kiφ‖(g)

In conclusion, it can be concluded that EΩφ=∧i∈ΩKiφ holds true.

Proof of the second equation in Theorem 1.

CΩφ represents common knowledge, where every agent in the group knows content φ, and everyone knows that everyone knows φ, etc., ≈CΩ is the transitive closure of ≈EΩ.

The possibility value of epistemic formula CΩφ on state g.

‖CΩφ‖(g)=FMg{π∈Paths(g)|g≈CΩg′ and π=g⋯g′ and ‖φ‖g′}

For finite M=(G,g0,δ,AP,ℓ,≈i), define η:G→[0,1] as

η(g)=∨{∧e≥0δ(ge,≈CΩ,ge+1)|g1=g,ge∈G,≈CΩ⊆G×G}

For each g∈G there exists η(g)=∨{∧e≥0δ(ge,≈CΩ,ge+1)|g1=g,ge∈G,≈CΩ⊆G×G} represent the maximum likelihood of the sequence starting from state g.

Therefore, the calculation of CΩφ can be done as follows:

‖CΩφ‖(g)=FMg{π∈Paths(g)|g≈CΩg′ and π=g⋯g′ and ‖φ‖g′}=∨t1∈G(P(g,βΩC,t1)∧‖φ‖(t1))∧∨t2,t3⋯∈G(P(t1,βΩC,t2)∧P(t2,βΩC,t3)∧⋯)=∨t1∈G(PσΩC(g,t1)∧‖φ‖(t1))∧ησΩC(t1)=∨t1∈G((PσΩE(g,t1)∨PσΩE2(g,t1)⋯∨PσΩEk(g,t1))∧‖φ‖(t1))∧(ησΩE(t1)∨ησΩE2(t1)⋯∨ησΩEk(t1))=‖EΩφ∨EΩ2φ∨⋯∨EΩkφ‖(g)

In conclusion, it can be concluded that CΩφ=EΩφ∨EΩ2φ∨⋯∨EΩkφ holds true.

Proof of the third equation in Theorem 1.

DΩφ represents distributed knowledge, where members of the group Ω publicly declare their knowledge as announcements in language [℘] to achieve sharing. As a result, each member in the group can know content φ based on announcement [℘]. This announcement mechanism is akin to the blackboard structure in multi-agent systems, enabling individual agents to store local information in an accessible shared space, thus facilitating the sharing of local data [39].

It indicates that on all paths reached through group epistemic accessibility relationship ≈DΩ, the next state satisfies content φ. Therefore, the calculation of DΩφ can be done as follows:

‖DΩφ‖(g)=FMg{π∈Paths(g)|g≈DΩg′ and π=g⋯g′ and ‖φ‖g′}=∨t∈G(∧h≥0P(th,βΩD,th+1)∧P(g,βΩD,t1)∧‖φ‖(t1))=∨t∈G(∧h≥0(P(th,βi1,th+1)∧P(th,βi2,th+1)∧⋯)∧(P(g,βi1,t1)∧P(g,βi1,t1)∧⋯)∧‖[℘]φ‖(t1))=∧i∈Ω‖Ki[℘]φ‖(g)

In conclusion, it can be concluded that DΩφ=∧i∈ΩKi[℘]φ holds true.

Hereafter, based on different scheduler functions σ, we will apply corresponding simplification rules to transform FCTLK formulas into FCTL formulas. The correctness and completeness of this transformation will be proven.

Theorem 2. Given the scheduler σt, let ℱ:φ→φFKS be a function. The FCTLK temporal formulae can be transformed into FCTL as follows:

ℱ(p)=p(4)

ℱ(¬φ)=¬φ(5)

ℱ(φ1∧φ2)=φ1∧φ2(6)

ℱ(FM(φ1∪φ1))=(FM(φ1∪φ1))(7)

ℱ(FM(◯φ))=(FM(◯φ))(8)

Proof of Theorem 2.

When the scheduler function is σt, it only captures the temporal transitions for each state in the model. This FKS model only interprets FCTL formulas. It cannot be used to capture the transformed formulas of knowledge because it ignores all relations except those labeled by ∂. Therefore, FCTLK formulas can be directly converted into FCTL formulas without the need for simplification.

Theorem 3. Given the scheduler σi, σΩE, σΩC, and σΩD, let ℱ:φ→φFKS be a function. The FCTLK epistemic formulas can be transformed into FCTL as follows:

ℱ(Kiφ)=FM(◯φ)σi(9)

ℱ(EΩφ)=FM(◯φ)σΩE(10)

ℱ(CΩφ)=FM(◯φ)σΩC(11)

ℱ(DΩφ)=FM(◯φ)σΩD(12)

When the scheduler functions are σi, σΩE, σΩC, and σΩD, the FKS model exclusively captures the transformed formulas related to knowledge, specifically the transitions labeled as β actions. Intuitively, transitions labeled as β represent epistemic accessibility relations, and according to epistemic semantics, all next states reached through epistemic accessibility relations satisfy content φ. In other words, all next states reached through transitions labeled as β satisfy ℱ(φ). This explains why the knowledge formula is transformed into the next operator in all paths emanating from the knowledge state, followed by the transformation of the knowledge content, i.e., the conversion to ℱ(φ). Finally, it is proven that the truth value of the formulas remains unchanged after simplification.

Let F=(S,s0,AP,υ,ACT,P) be a finite FDP, Dφ be a |S|×|S| fuzzy diagonal matrix for state formula φ. For each s,t∈S,

Dφ(s,t)={‖φ‖(s)s=t0otherwise

Pφ is a |S|×1 fuzzy matrix. E is a |S|×1 fuzzy matrix with all elements equal to 1.

In the following, simplify the four epistemic formulas and express them in matrix form.

Proof of the first equation in Theorem 3.

‖Kiφ‖(g) represents the possibility value that agent i knows content φ at state g.

‖Kiφ‖(g)=FMg{π∈Paths(g)|g≈ig′ and π=g⋯g′ and ‖φ‖g′}=∨π=g0βig1βig2⋯∈Paths(g)(P(g,βi,g1)∧P(g1,βi,g2)∧⋯∧P(g,βi,g1)∧‖φ‖(g1))=∨π=g0βig1βig2⋯∈Paths(g)(Pσi(g,g1)∧Pσi(g1,g2)∧⋯∧Pσi(g,g1)∧‖φ‖(g1))=∨g1∈G(Pσi(g,g1)∧‖φ‖(g1))∧∨g2,g3⋯∈G(Pσi(g1,g2)∧Pσi(g2,g3)∧⋯)=∨g1∈G(Pσi(g,g1)∧‖φ‖(g1)∧rσi(g1))=Pσi∘Dφ∘rσi

Therefore, it can be proven that ‖Kiφ‖(g)=‖FM(◯φ)σi‖(g)=Pσi∘Dφ∘rσi holds. This implies that the epistemic formula Kiφ can be reduced to the state formula FM(◯φ)σi in FCTL.

Proof of the second equation in Theorem 3.

‖EΩφ‖(g) represents the possibility value that each agent in group Ω satisfies content φ at state g.

‖EΩφ‖(g)=FMg{π∈Paths(g)|g≈EΩg′ and π=g⋯g′ and ‖φ‖g′}=∨π=g0βΩEg1βΩEg2⋯∈Paths(g)(P(g,βΩE,g1)∧P(g1,βΩE,g2)∧⋯∧P(g,βΩE,g1)∧‖φ‖(g1))=∨π=g0βΩEg1βΩEg2⋯∈Paths(g)(PσΩE(g,g1)∧PσΩE(g1,g2)∧⋯∧PσΩE(g,g1)∧‖φ‖(g1))=PσΩE∘Dφ∘rσΩE