images
Computers, Materials & Continua
images

DOI: 10.32604/cmc.2024.047168

ARTICLE

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

Xia Li1, Zhanyou Ma1,*, Zhibao Mian2, Ziyuan Liu1, Ruiqi Huang1 and Nana He1

1School of Computer Science and Engineering, North Minzu University, Yinchuan, 750000, China
2School of Computer Science, FoSE, The University of Hull, Hull, UK
*Corresponding Author: Zhanyou Ma. Email: mazhany@nmu.edu.cn
Received: 27 October 2023; Accepted: 05 February 2024; Published: 26 March 2024

Abstract: Model checking is an automated formal verification method to verify whether epistemic multi-agent systems adhere to property specifications. Although there is an extensive literature on qualitative properties such as safety and liveness, there is still a lack of quantitative and uncertain property verifications for these systems. In uncertain environments, agents must make judicious decisions based on subjective epistemic. To verify epistemic and measurable properties in multi-agent systems, this paper extends fuzzy computation tree logic by introducing epistemic modalities and proposing a new Fuzzy Computation Tree Logic of Knowledge (FCTLK). We represent fuzzy multi-agent systems as distributed knowledge bases with fuzzy epistemic interpreted systems. In addition, we provide a transformation algorithm from fuzzy epistemic interpreted systems to fuzzy Kripke structures, as well as transformation rules from FCTLK formulas to Fuzzy Computation Tree Logic (FCTL) formulas. Accordingly, we transform the FCTLK model checking problem into the FCTL model checking. This enables the verification of FCTLK formulas by using the fuzzy model checking algorithm of FCTL without additional computational overheads. Finally, we present correctness proofs and complexity analyses of the proposed algorithms. Additionally, we further illustrate the practical application of our approach through an example of a train control system.

Keywords: Model checking; multi-agent systems; fuzzy epistemic interpreted systems; fuzzy computation tree logic; transformation algorithm

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

Therefore, it can be concluded that ‖EΩφ‖(g)=‖FM(◯φ)σΩE‖(g)=PσΩE∘Dφ∘rσΩE holds, meaning that the epistemic formula EΩφ can be simplified into the state formula FM(◯φ)σΩE in FCTL. Furthermore, based on the proof results of Theorem 1, we have the equality ‖EΩφ‖(g)=∧i∈Ω‖Kiφ‖(g) holds. Therefore, formula EΩφ can also be simplified to ∧i∈ΩFM(◯φ)σi in FCTL.

Proof of the third equation in Theorem 3.

‖CΩφ‖(g) represents the possibility value that everyone in group Ω knows the common knowledge φ.

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

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

Proof of the fourth equation in Theorem 3.

‖DΩφ‖(g) represents the possibility value of distributed knowledge φ at state g.

‖DGφ‖(g)=FMg{π∈Paths(g)|g≈DΩg′ and π=g⋯g′ and ‖φ‖g′}=∨π=g0βΩDg1βΩDg2⋯∈Paths(g)(P(g,βΩD,g1)∧P(g1,βΩD,g2)∧⋯∧P(g,βΩD,g1)∧‖φ‖(g1))

=∨π=g0βΩDg1βΩDg2⋯∈Paths(g)(PσΩD(g,g1)∧PσΩD(g1,g2)∧⋯∧PσΩD(g,g1)∧‖φ‖(g1))=PσΩD∘Dφ∘rσΩD

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

Algorithm 3 describes the FCTL model checking algorithm based on the FKS model.

After model transformation and formula simplification, the model checking algorithm for FCTLK is converted into the model checking algorithm for FCTL, and Algorithm 3 is invoked for computation. The model checking algorithm for FCTLK based on the FEIS model is presented in Algorithm 4.

Example 4. Following the simplification rules of the formula, Next, we will provide the calculation of the possibility that everyone in the group knows content q.

PσΩE+=(0.300.70.40.300.60.40.300.30.40000)rσΩE=(0.300.70.40.300.60.40.300.30.40000)∘(0.300.30)=(0.30.30.30)

‖EΩq‖(g)=‖FM(◯q)σΩE‖(g)=PσΩE∘Dq∘rσΩE=(000.70000.600.3000.40000)∘(0.600000.800000.800000.7)∘(0.30.30.30)=(0.30.30.30)

6  Time Complexity of Model Checking FCTLK

In this section, we will analyze the time complexity of the fuzzy model checking algorithm proposed in Section five. The algorithm comprises the following three primary computational steps.

Lemma 1. The time complexity of the model transformation is linear concerning the size of the input model M, i.e., 𝒪(|M|).

Proof of Lemma 1. The problem of model transformation is tackled using a deterministic one-tape Turing machine (DTM) [40]. The DTM sequentially reads all the states, temporal transition relations, and epistemic accessibility relation within the input FEIS model, using distinct markers to signify these relations, and converting them into transition actions. The transformed states and actions are recorded onto an output tape. Through DTM’s examination, model transformation can be accomplished within polynomial time, demonstrating a linear relationship between the time complexity of transformation and the size of the input model.

Lemma 2. The translation from FCTLK formulae to FCTL formulae is linear in time in the size of the input formula φ, i.e., 𝒪(|φ|).

Proof of Lemma 2.

(1) We divide the FCTLK formula φ input into n sub-formulas. The nth formula is a state formula with epistemic operator, and this step can be executed in linear time, proportional to the size of formula |φ|, i.e., 𝒪|φ|.

(2) Apply the relevant reduction rule to the nth formula based on the form of its state sub-formula to generate an FCTL formula. This process involves straightforwardly applying the rules to each sub-formula, resulting in a constant time complexity, i.e., 𝒪(1).

(3) Replace the nth sub-formula with the translated state formula. This step can also be executed in constant time.

(4) The preceding process is repeated until no more FCTLK sub-formulas exist in the formula.

(5) Therefore, since each sub-formula needs to be converted according to steps 2 and 3, the process needs to be iterated n times, where n is the number of sub-formulas. Since the number of sub-formulas is linearly related to the size of the formula, the time complexity of this step is 𝒪(|φ|).

Theorem 4. A model checking algorithm exists for FCTLK formulae, which runs in time 𝒪(|M|×|φ|).

Proof of Theorem 4.

For a given FKS model and FCTL formula, Pan et al. [30] determined that the time complexity of the model checking algorithm is 𝒪(|MFKS|×|φFKS|). We can conclude that the total time complexity of the algorithm is based on Lemma 1 and Lemma 2 𝒪(|MFKS|×|φFKS|)+𝒪(|M|)+𝒪(|φ|). Due to the linear relationship between the size of the fuzzy interpreted system model and formula and the size of the transformed model and formula, the algorithm’s total time complexity can be reduced.

From Theorem 4, we know that the model checking problem exhibits a polynomial relationship with both the model size and formula length, indicating an upper bound of P. Through an investigation of [30], we discover that the FCTL model checking problem based on the FKS model is P-complete, suggesting a lower bound of P as well. In summary, the FCTLK model checking problem is P-complete.

7  Illustrative Examples

The train control system consists of two trains, a controller, and a tunnel on a circular track. On the track, there are two trains moving clockwise and counterclockwise. The tunnel can only accommodate one train, and traffic lights are installed at both ends of the tunnel. These traffic lights can be either red or green. Each train carries a signal generator used to send signals to the controller when they approach the tunnel. The controller is responsible for receiving signals from both of two trains and controlling the traffic lights at both ends of the tunnel to ensure that the two trains never enter the tunnel simultaneously.

In the real world, controllers perceive their surrounding environment through sensors, but these sensors may be influenced by various interfering factors such as noise, errors, and communication delays. These factors introduce randomness and uncertainty, causing fluctuations and errors in sensor data, which in turn result in biases in the controller’s environmental perception and subsequently impact its decision-making process. Therefore, modeling with a fuzzy system can better capture the actual status of the trains, enabling the controller to make more flexible decisions and controls.

Let the set of agents be Agt={i1,i2,j}, where i1,i2,j corresponds to Train1, Train2, and Controller in Fig. 4. The following transforms this instance into a FEIS model, as shown in Fig. 5.

Figure 4: Train control system

Figure 5: The FEIS model of the train control system

(1) The local state set of agents i1,i2,j are Li1={away1,wait1,tunnel1}, Li2={away2,wait2,tunnel2} and Lj={light1light2}.

(2) G={s0,s1,s2,s3,s4} is the global state set of the system, including s0={away1,r1r2,away2}, s1={tunnel1,g1r2,wait2}, s2={tunnel1,g1r2,wait2}, s3={away1,r1g2,tunnel2} and s4={wait1,r1g2,tunnel2}.

(3) The initial state is s0.

(4) The set of atomic propositions for agents i1,i2,j is APi1={away1(pi11),wait1(pi12),tunnel1(pi13)}, APi2={away2(pi21),wait2(pi22),tunnel2(pi23)}, and APj={pj1,pj2,pj3}, respectively, where

• The atomic propositions constituting “away” are pi11 and pi21, representing the trains moving away from the tunnel.

• The atomic propositions constituting “wait” are pi12 and pi22, indicating longer waiting times for the trains.

• The atomic propositions constituting “tunnel” are pi13 and pi23, signifying the trains approaching the tunnel entrance.

• The atomic propositions constituting “light1light2” are pj1, pj2, and pj3, respectively, representing the controller changing traffic signal lights based on the perception of train information as r1r2, r1g2, and g1r2.

(5) Joint actions are defined as Act={∂1,⋯,∂14}, where for an action ∂∈Act, its preconditions pre(∂) and postconditions post(∂) are both local state sets, representing the prerequisites before and the state after the execution of action ∂. Agent(∂) denotes the set of agents that may alter local states when performing action ∂. For example, pre(∂1)={away1,r1r2}, post(∂1)={tunnel1,g1r2} Agent(∂1)={i1,j}.

(6) The fuzzy values of atomic propositions under specific states are assumed as follows:

s0={T1(pi11=0.8,pi12=0.4,pi13=0.5),C(pj1=0.95,pj2=0.3,pj3=0.9),T2(pi21=0.9,pi22=0.7,pi23=0.3)}s1={T1(pi11=0.6,pi12=0.4,pi13=0.7),C(pj1=0.5,pj2=0.3,pj3=0.9),T2(pi21=0.4,pi22=0.8,pi23=0.2)}s2={T1(pi11=0.1,pi12=0.2,pi13=0.5),C(pj1=0.4,pj2=0.3,pj3=0.9),T2(pi21=0.5,pi22=0.7,pi23=0.6)}s3={T1(pi11=0.9,pi12=0.2,pi13=0.7),C(pj1=0.4,pj2=0.8,pj3=0.3),T2(pi21=0.4,pi22=0.3,pi23=0.6)}s4={T1(pi11=0.1,pi12=0.9,pi13=0.7),C(pj1=0.4,pj2=0.7,pj3=0.3),T2(pi21=0.4,pi22=0.7,pi23=0.8)}

Because there is an epistemic accessibility relationship between states, the setting of fuzzy values needs to satisfy ℓ(i,g,p)=ℓ(i,g′,p). For example, between s0 and s1, there exists epistemic relationships s0≈i1s1 and s0≈js1, so there must be at least one set of fuzzy label function values that are equal, i.e., ℓi1(s0,pi12)=ℓi1(s1,pi12)=0.4, ℓj(s0,pj3)=ℓj(s1,pj3)=0.9.

(7) The arrowed lines in Fig. 5 represent fuzzy transitions. For example, s0∂1,0.2→s1 indicates that in state s0, the possibility of transitioning to state s1 by executing joint action ∂1 is 0.2. Dashed lines represent transitions through epistemic accessibility relationships.

Remark 2. In this instance, the degree of satisfaction of atomic propositions and the possibility of transitions under specific states are both represented as fuzzy values subjectively acquired through expert experience.

According to the model transformation rules and the definition of group epistemic accessibility relationships, the FEIS model in Fig. 5 is transformed into the FDP model in Fig. 6, which includes group epistemic actions, as follows.

Figure 6: The FDP model of the train control system

‖Ki1(tunnel2)‖(s2)=0.2 represents that T1 predicts the possibility of T2 passing through the tunnel to be 0.2. This anticipation arises because in state s2, it is highly likely that the Controller, by perceiving the states of T1 and T2, adjusts the traffic signal to g1r2. At this moment, T1 is passing through the tunnel, and T2 should be in a waiting state. T1, with its awareness of traffic safety, understands that if T2 receives the traffic signal, it should also realize the presence of other trains inside the tunnel. Therefore, for safety reasons, the prudent decision is to wait rather than trying to enter the tunnel.

‖Ei1i2(r1r2)‖(s0)=0.6 indicates that each train knows the possibility of the traffic signal being r1r2 is 0.6. This is because in s0, both T1 and T2 are far away from the tunnel, and the Controller perceives that there is no train information in the vicinity. Therefore, it determines that it is safe to set the traffic signal to r1r2.

‖Ci1i2j(¬(tunnel1∧tunnel2))‖(s1)=0.8 represents that everyone is cognizant of a traffic common sense fact that two trains cannot enter the tunnel simultaneously, and the credibility of this epistemic is 0.8. This indicates that in state s1, both the trains and the Controller have a very clear understanding of this traffic rule and are committed to strictly adhering to it to ensure traffic safety.

‖Di2j(wait2)‖(s0)=‖Kj(r1r2)∧Ki2([r1r2]wait2)‖(s0)=0.9 indicates that in state s0, the Controller adjusts the traffic signal to r1r2 by perceiving the external environment. T2 perceives this change and, based on the state of the traffic signal, deduces that there may be other trains inside the tunnel at this time. Therefore, it chooses a probability of 0.9 to wait at the entrance.

8  Conclusions

This paper addresses the verification of attributes in fuzzy epistemic multi-agent systems using an indirect fuzzy model checking algorithm, which transforms the FCTLK model checking problem based on FEIS into the FCTL model checking problem based on FKS. It calculates the formulas of FCTLK through the synthesis operation of fuzzy matrices and proposes a polynomial-time fuzzy model-checking algorithm. An example of a train control system is presented as an illustration of the practical application of this algorithm.

In the future, we plan to explore the application of direct fuzzy model checking methods for verification. Simultaneously, we intend to utilize the decision framework of the FP-SVNSS method [41] and apply it to the verification of multi-agent systems based on fuzzy epistemic. The core idea of this method is to enrich the verification process through control processes, addressing the issue of fuzzy epistemic attributes influencing collaborative behavior among agents in multi-agent systems. In the application of the decision framework, we need to consider how to verify fuzzy factors in collaborative behavior to ensure the overall collaborative performance of the system.

Acknowledgement: We would like to thank the anonymous reviewers and editors for their suggestions. We would also like to thank for the support and help in scientific research offered by the Key Laboratory of Images & Graphics Intelligent Processing of State Ethnic Affairs Commission, North Minzu University (IGIPLab).

Funding Statement: The work is partially supported by Natural Science Foundation of Ningxia (Grant No. AAC03300), National Natural Science Foundation of China (Grant No. 61962001), Graduate Innovation Project of North Minzu University (Grant No. YCX23152).

Author Contributions: Conceptualization and Methodology, Z.M. and X.L.; Formal analysis, Y.G. and Z.L. All authors have read and agreed to the published version of the manuscript.

Availability of Data and Materials: Not applicable.

Conflicts of Interest: The authors declare that they have no conflicts of interest to report regarding the present study.

References

1. L. Ding, H. Wan, L. Hu, and Y. Chen, “Identifying counterexamples without variability in software product line model checking,” Comput. Mater. Contin., vol. 75, no. 2, pp. 2655–2670, 2023.

2. R. Jhala and R. Majumdar, “Software model checking,” ACM Comput. Surv. (CSUR), vol. 41, no. 4, pp. 1–54, 2009. doi: 10.1145/1592434.1592438.

3. F. Huang, Z. Liu, T. Wang, H. Zhang, and T. Yip, “The optimization study about fault self-healing restoration of power distribution network based on multi-agent technology,” Comput. Mater. Contin., vol. 65, no. 1, pp. 865–878, 2020.

4. F. Belardinelli, A. Ferrando, and V. Malvone, “An abstraction-refinement framework for verifying strategic properties in multi-agent systems with imperfect information,” Artif. Intell., vol. 316, no. 5, pp. 103847, 2023. doi: 10.1016/j.artint.2022.103847.

5. C. Baier and J. P. Katoen, Principles of Model Checking. Cambridge, MA, USA: MIT Press, 2008.

6. Y. Shoham and S. B. Cousins, “Logics of mental attitudes in AI: A very preliminary survey,” Foundations of Knowledge Representation and Reasoning, vol. 810, pp. 296–309, 2005.

7. V. D. Ron, “Axioms for knowledge and time in distributed systems with perfect recall,” in Proc. Ninth Annual IEEE Symp. on Logic in Computer Science, Paris, France, IEEE, 1994, pp. 448–457.

8. G. Lakemeyer, “Limited reasoning in first-order knowledge bases,” Artif. Intell., vol. 71, no. 2, pp. 213–255, 1994. doi: 10.1016/0004-3702(94)90044-2.

9. G. M. Bodner, “Bodner constructivism: A theory of knowledge,” J. Chem. Educ., vol. 63, no. 10, pp. 837, 1986.

10. J. Skorupski, “Automatic verification of a knowledge base by using a multi-criteria group evaluation with application to security screening at an airport,” Knowl. Based Syst., vol. 85, no. 16, pp. 170–180, 2015. doi: 10.1016/j.knosys.2015.05.004.

11. W. Penczek and A. Lomuscio, “Verifying epistemic properties of multi-agent systems via bounded model checking,” in Proc. Second Int. Joint Conf. on Auton. Agents and Multiagent Syst., Melbourne, Australia, 2003, pp. 209–216.

12. D. Xie, W. Xiong, L. Bu, and X. Li, “Deriving unbounded reachability proof of linear hybrid automata during bounded checking procedure,” IEEE Trans. Comput., vol. 66, no. 3, pp. 416–430, 2016. doi: 10.1109/TC.2016.2604308.

13. G. B. Rossi, F. Crenna, and M. Berardengo, “Probability theory as a logic for modelling the measurement process,” Acta IMEKO, vol. 12, no. 2, pp. 1–5, 2023. doi: 10.21014/actaimeko.v12i2.1313.

14. F. Pourpanah et al., “An improved fuzzy ARTMAP and Q-learning agent model for pattern classification,” Neurocomput., vol. 359, no. 10, pp. 139–152, 2019. doi: 10.1016/j.neucom.2019.06.002.

15. A. K. Adak, M. K. Gunjan, and N. K. Agarwal, “Picture fuzzy semi-prime ideals,” J. Fuzzy Ext. Appl., vol. 4, no. 2, pp. 115–124, 2023.

16. A. Termine, A. Antonucci, G. Primiero, and A. Facchini, “Imprecise probabilistic model checking for stochastic multi-agent systems,” SN Comp. Sci., vol. 4, no. 5, pp. 443, 2023. doi: 10.1007/s42979-023-01817-x.

17. C. Fu, A. Turrini, X. Huang, L. Song, Y. Feng and L. Zhang, “Model checking probabilistic epistemic logic for probabilistic multiagent systems,” in Proc. Twenty-Seventh Int. Joint Conf. on Artif. Intell., Stockholm Sweden, 2018, pp. 4757–4763.

18. F. Ronald and J. Y. Halpern, “Reasoning about knowledge and probability,” J. ACM, vol. 41, no. 2, pp. 340–367, 1994. doi: 10.1145/174652.174658.

19. Y. H. Fan, Y. M. Li, and H. Y. Pan, “Computation tree logic model checking for nondeterminisitc fuzzy Kripke structure,” Acta Electon. Sin., vol. 46, no. 1, pp. 152–159, 2018 (In Chinese).

20. N. L. Anh, “Computing the fuzzy partition corresponding to the greatest fuzzy auto-bisimulation of a fuzzy graph-based structure under the Gödel semantics,” Inf. Sci., vol. 630, pp. 482–506, 2023. doi: 10.1016/j.ins.2023.02.029.

21. Z. Ma, Z. Li, W. Li, Y. Gao, and X. Li, “Model checking fuzzy computation tree logic based on fuzzy decision processes with cost,” Entropy, vol. 24, no. 9, pp. 1183, 2022. doi: 10.3390/e24091183.

22. P. Yannick and A. Subias, “Diagnosability of event patterns in safe labeled time Petri nets: A model-checking approach,” IEEE Trans. Autom. Sci. Eng., vol. 19, no. 2, pp. 1151–1162, 2021.

23. P. A. Abdulla, M. F. Atig, A. Godbole, S. Krishna, and M. Vahanwala, “Overcoming memory weakness with unified fairness,” arXiv:2305.17605, 2023.

24. Z. Ma, Y. Gao, Z. Li, X. Li, and Z. Liu, “Quantitative reachability analysis of generalized possibilistic decision processes,” J. Intell. Fuzzy Syst., vol. 44, no. 5, pp. 8357–8373, 2023. doi: 10.3233/JIFS-222803.

25. A. Souri, A. M. Rahmani, N. J. Navimipour, and R. Rezaei, “Rezaei A symbolic model checking approach in formal verification of distributed systems,” Hum. Cent. Comput. Inf. Sci., vol. 9, no. 1, pp. 1–27, 2019.

26. B. Mário, A. Madeira, and M. A. Martins, “Graded epistemic logic with public announcement,” J. Log. Algebr. Methods Prog., vol. 125, pp. 100732, 2022.

27. H. Enhua, “Fuzzy epistemic logic,” Noesis XVIII, vol. 18, no. 1, pp. 19–32, 2017.

28. Y. M. Li and Z. Y. Ma, “Quantitative computation tree logic model checking based on generalized possibility measures,” IEEE Trans. Fuzzy Syst., vol. 23, no. 6, pp. 2034–2047, 2015. doi: 10.1109/TFUZZ.2015.2396537.

29. Y. M. Li, W. Liu, J. Wang, X. Yu, and C. Li, “Model checking of possibilistic linear-time properties based on generalized possibilistic decision processes,” IEEE Trans. Fuzzy Syst., vol. 31, no. 10, pp. 3495–3506, 2023. doi: 10.1109/TFUZZ.2023.3260446.

30. H. Y. Pan, Y. Li, Y. Cao, and Z. Ma, “Model checking fuzzy computation tree logic,” Fuzzy Sets Syst., vol. 262, no. 23, pp. 60–77, 2015. doi: 10.1016/j.fss.2014.07.008.

31. S. A. El-Morsy, “Optimization of fuzzy zero-base budgeting,” Comput. Algorithms Num. Dimens., vol. 1, no. 4, pp. 147–154, 2022.

32. E. Elham, M. R. Fathi, and S. M. Sobhani, “A modification of technique for order preference by similarity to ideal solution (TOPSIS) through fuzzy similarity method (a numerical example of the personnel selection),” J. Appl. Res. Ind. Eng., vol. 10, no. 2, pp. 203–217, 2023.

33. B. Darko, D. Tesic, D. Marinkovic, and A. Milic, “Modeling of neuro-fuzzy system as a support in decision-making processes,” J. Mech. Eng., vol. 2, no. 1, pp. 222–234, 2021. doi: 10.31181/rme2001021222b.

34. E. Ali, H. Mehrmanesh, and M. Mohammadi, “Identifying and prioritizing technology capability drivers in the supply chain using the fuzzy hierarchical analysis process (case study: Iran khodro and saipa automotive company),” Int. J. Res. Ind. Eng., vol. 12, no. 1, pp. 2783, 2023.

35. R. Abolfazl and M. Hemati, “Providing a hybrid fuzzy approach to explain managers’ mental paradigms to prioritize employee needs,” J. Fuzzy Ext. Appl., vol. 4, no. 3, pp. 155–172, 2023.

36. A. Z. Lotfi, “Fuzzy sets,” Inform. Comput., vol. 8, no. 3, pp. 338–353, 1965.

37. Y. G. Xue and Y. Deng, “Decision making under measure-based granular uncertainty with intuitionistic fuzzy sets,” Appl. Intell., vol. 51, no. 8, pp. 6224–6233, 2021. doi: 10.1007/s10489-021-02216-6.

38. W. Wei, J. Bentahar, and A. B. Hamza, “Model checking epistemic-probabilistic logic using probabilistic interpreted systems,” Knowl. Based Syst., vol. 50, no. 9–10, pp. 279–295, 2013. doi: 10.1016/j.knosys.2013.06.017.

39. V. Botti et al., “A temporal blackboard for a multi-agent environment,” Data Knowl. Eng., vol. 15, no. 3, pp. 189–211, 1995. doi: 10.1016/0169-023X(95)00007-F.

40. B. Guillon, G. Pighizzini, L. Priginoiero, and D. Prusa, “Prusa weight-reducing turing machines,” Inf. Comput., vol. 292, no. 2, pp. 105030, 2023. doi: 10.1016/j.ic.2023.105030.

41. M. Ihsan, M. Saeed, and A. U. Rahman, “Optimizing hard disk selection via a fuzzy parameterized single-valued neutrosophic soft set approach,” J. Oper. Strateg. Anal., vol. 1, no. 2, pp. 62–69, 2023. doi: 10.56578/josa010203.

images
This work is licensed under a Creative Commons Attribution 4.0 International License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.