An MDE Approach for Modelling and Reasoning About Multi-agent Systems

Abstract

Epistemic logic plays an important role in artificial intelligence for reasoning about multi-agent systems. Current approaches for modelling multi-agent systems with epistemic logic use Kripke semantics where the knowledge base of an agent is represented as atomic propositions, but intelligent agents need to be equipped with formulas to derive implicit information. In this paper, we propose a metamodelling approach where agents’ state of affairs are separated in different scopes, and the knowledge base of an agent is represented by a propositional logic language restricted to Horn clauses. We propose to use a model driven approach for the diagrammatic representation of multi-agent systems knowledge (and nested knowledge). We use a message passing for updating the state of affairs of agents and use belief revision to update the knowledge base of agents.

1 Introduction

Our approach for modelling multi-agent system is based on combining metamodelling and epistemic logic with diagrammatic specifications and logic statements. We use the basic modal system K [5] for epistemic logic and enhance the modelling with the use of model-driven engineering techniques. Traditionally, Kripke structures have been used to give the semantics of epistemic logic by representing the information state of several agents [5]. Although Kripke structures can be used to model the cognitive states of other agents but the knowledge representation of different agents in a Kripke model are not structured. In our approach, agents’ information states are modularized into scopes. Scopes include states where the knowledge base of a state is represented by horn clauses making agents capable of deducing new information. We propose to use metamodels for specifying the information state of agents. Using metamodels for defining domain specific modelling languages has potential as languages can be easily customized. However, model-driven engineering using metamodels has not been explored for modelling multi-agent systems.

Our work is closely related to the deductive model of belief proposed by Konolige [8] where agents’ beliefs are described as a set of sentences in a formal language together with a deductive process for deriving consequences of those beliefs. Deductive model of belief provides a model for agents’ problem solving ability based on the reasoning about other agents’ problem solving ability. Konolige introduced the concept of belief subsystem which can model fairly complicated and confusing situations where agents believe that other agents have belief subsystems of varying capabilities. Some of these scenarios would be useful in representing situations where agents have different beliefs. In real-life, different sources will expose agents to different information, which can naturally lead to disagreement. In our approach, we use several distinct elements to represent and to reason about knowledge in a MAS setting. We use Diagram Predicate Framework [11] for the diagrammatic representation of agents’ state of affairs where the knowledge base is represented using Horn clauses. We apply category theory for structuring the knowledge of different agents and combine our approach with Delgrande’s inconsistency-based contraction [3] for knowledge base revision. Our proposed approach of modular information states can be used to represent different knowledge of agents, and leads to a simple mechanism to update the knowledge base of agents. We introduce the application of category theoretical operations for extracting the local and global knowledge base of agents which opens up a new formal way of modelling multi-agent systems.

The paper is organized as follows. In Sect. 2, we present a language for representing the knowledge base of agents. Section 3 presents the modelling artifacts for specifying multi-agent systems. Section 4 provides details of how agents communicate information and update their knowledge base, Sect. 5 concludes the paper with a direction for future work.

2 Knowledge Representation of Multi-agent Systems

Unlike Kripke models, states in our multi-agent model are associated with knowledge bases (KB). The knowledge base is given by a restricted form of the propositional logic language $\mathcal {L_{HC}}$ based on a finite set of atoms (atomic propositions) $\mathbf P = \{\bot , p,q,r, \ldots \}$, where P includes the distinguished atom $\bot$ (false). The language $\mathcal {L_{HC}}$ over P is given by a set of horn clauses as defined in [3]. A horn clause can be written as a rule in the form $\alpha _1 \wedge \alpha _2 \wedge \ldots \wedge \alpha _n \rightarrow \alpha$, where $n \ge 0$, and $\alpha$, $\alpha _i$ $(1 \le i \le n)$ are distinct atoms and $\rightarrow$ represents implication. Let $\varphi$ be a horn clause in $\mathcal {L_{HC}}$, if $n = 0$ then $\varphi$ represents a ground atom and $\rightarrow \alpha$ is written as $\alpha$. We will use $body(\varphi )$ to refer to the set of atomic propositions to the left of $\rightarrow$ and $head(\varphi )$ to refer to the consequence of $\varphi$. We use $\bot$ in the consequence of a clause to represent an integrity constraint [3]. In other words, a clause with $\bot$ in the consequence represents an impossible situation. A horn clause $\varphi$ can be derived from a set of horn clauses $\varPhi$, written $\varPhi \vdash \varphi$ if $\varphi$ can be obtained by the inference relation given in [3]. A set of horn clauses $\varPhi$ is inconsistent if $\varPhi \vdash \bot$. We use the notation $\varPhi ^* =\texttt {Cn} (\varPhi ) = \{ \varphi : \varPhi \vdash \varphi \}$ to represent the set of all logical consequences of $\varPhi$. A scope of an agent consists of one or more states representing epistemic alternatives. To express what an agent know in its states or about other agents, we need a language of epistemic logic $\mathcal {L}_k$ which is defined as: $\varphi \, {:}{:}{=} \, p | \lnot \varphi | (\varphi \wedge \varphi ) | (\varphi \vee \varphi ) | (\varphi \rightarrow \varphi ) | K_a \varphi$. Here p is an atomic proposition and $K_a$ is a knowledge operator. For an agent a, $K_a \varphi$ is interpreted as “agent a knows $\varphi$”.

Fig. 1.

An example model of an agent a and its scopes

Figure 1(left) shows an example where the knowledge of an agent a is represented diagrammatically. The example illustrates a scope A of agent a consisting of two states $a_0$ and $a_1$. These two states are representing two epistemic alternatives of agent a. We use KB($a_0$) and KB($a_1$) to refer to the knowledge bases of states $a_0$ and $a_1$, respectively. In scope A, agent a knows that it is cloudy (represented by the ground atom c) and rain implies cloudy (represented by horn clause: $r \rightarrow c$), but agent a does not know if it is raining or not. Therefore, he cannot distinguish between states $a_0$ and $a_1$ where $r \in ~$ KB $(a_0)$ and $r \notin ~$ KB $(a_1)$ (i.e., uncertain about r). What agent a knows about agent b’s epistemic alternatives are represented in the internal scope B. The internal scope B represents the information state of agent b where agent b knows that it is windy (represented by the ground atom w) but he cannot distinguish between $b_0$ and $b_1$ where $c \in ~$ KB $(b_0), r \in ~$ KB $(b_0)$ and $c \notin ~$ KB $(b_1), r \notin ~\texttt {KB}(b_1)$. Figure 1(right) illustrates this model with hierarchically structured information. Distinguished clauses that are true only in a particular state are represented inside the rectangular box representing the state. Horn clauses that are commonly known among all the agents are represented in a global knowledge base $\varTheta$. Horn clauses that are commonly known among all the states in a scope are visualized in a local knowledge base (e.g., $\varGamma _A$, $\varGamma _B$ in Fig. 1). For brevity we will not display all the logical consequences inside the boxes. Note that local knowledge bases implicitly include the global knowledge base. Therefore in Fig. 1(right), $\varGamma _{A}^*$ = Cn $(\{ r \rightarrow c , c \})$ and $\varGamma _{B}^*$ = Cn $(\{ r \rightarrow c , w \})$. We apply a pullback operation for extracting the local and global knowledge bases of agents which is a very common construction in category theory [1]. Below we formalize the notion of local and global knowledge base of agents. In order to apply category theory, we need to constitute a category for knowledge base where the objects are sets of horn clauses and morphisms are given by the inclusion mapping of horn clauses.

Definition 1

(Inclusion mapping of horn clauses). Let $\varPhi$ and $\varPsi$ be two sets of horn clauses. An inclusion mapping $f: \varPhi \rightarrow \varPsi$ exists if $\forall \varphi \in \varPhi ,$ $\varPsi \vdash \varphi$.

Definition 2

(Local knowledge base). Let $s_0$, $s_1$, ...$s_n$ be states of agent a in scope $A_1$ and $\varPhi _0=$ KB($s_0$), $\varPhi _1=$ KB $(s_1), \ldots$ knowledge bases comprised of horn clauses. The local knowledge base $\varGamma _{A_1}$ of scope $A_1$ is the information commonly known by agent a in scope $A_1$ and is obtained by the limit of the inclusion mappings $\varPhi _0 \rightarrow \varPhi _\mathcal {C}, \varPhi _1 \rightarrow \varPhi _\mathcal {C},\ldots \varPhi _m \rightarrow \varPhi _\mathcal {C}$ where $\varPhi _\mathcal {C}$ is the combined knowledge base of $\varPhi _0, \varPhi _1,\ldots \varPhi _m$.

Definition 3

(Global knowledge base). Let $\varGamma _{A_1}, \varGamma _{A_2}, \ldots \varGamma _{An}$ be the local knowledge bases of scopes $A_1, A_2,\ldots A_n$. The global knowledge base $\varTheta$ is the information commonly known in scopes $A_1$, $A_2$, ...$A_n$ and is obtained by the limit of the inclusion mappings $\varGamma _{A_1} \rightarrow \varGamma _\mathcal {C}, \varGamma _{A_2} \rightarrow \varGamma _\mathcal {C},\ldots \varGamma _{A_n} \rightarrow \varGamma _\mathcal {C}$ where $\varGamma _\mathcal {C}$ is the combined knowledge base of all the local knowledge bases.

Fig. 2.

Local and global knowledge base

Figure 2 shows the knowledge bases of different agents and their local and global knowledge bases. All the arrows in the figure represent inclusion mappings of horn clauses.

Theorem 1

The limit of a set of inclusion mappings of horn clauses $\{\varPhi _0 \rightarrow \varPsi , \varPhi _1 \rightarrow \varPsi ,\ldots \varPhi _m \rightarrow \varPsi \}$ is a consistent knowledge base if at least one of $\varPhi _0, \varPhi _1,\ldots \varPhi _m$ are consistent.

Proof:

Let $\varGamma$ be the limit of the inclusion mappings and $\varPhi _i (0\le i \le m)$ be a consistent knowledge base. Since $\forall \gamma \in \varGamma$, $\varPhi _i \vdash \gamma$, it is not possible that $\varGamma$ is an inconsistent knowledge base while $\varPhi _i$ is a consistent knowledge base.    $\square$

In Fig. 2 the colimit $\varTheta _\mathcal {C}$ represents the combined knowledge base of all the agents and the colimit $\varGamma _\mathcal {C}$ represents the distributed knowledge of a set of agents. There exists an inclusion mapping from $\varTheta _\mathcal {C}$ to the language $\mathcal {L_{HC}}$. It is possible that the colimits might be inconsistent. However, a consistent $\varGamma _\mathcal {C}$ supports collaboration of the agents’ knowledge.

3 Metamodelling with DPF

We use Diagrammatic Logic [4] and the Diagram Predicate Framework (DPF) [11] for the formal development of metamodel specifications. A metamodel specifies the abstract syntax of a modelling language that often includes a set of modelling concepts, their attributes and their relationships, as well as the rules for combining these concepts to specify valid models. In the context of this paper we develop a metamodel for hierarchical representation of agents’ knowledge. In DPF, a (meta)model is represented by a diagrammatic specification $\mathfrak {S}$ $= (S, C^\mathfrak {S}:\varSigma )$ consisting of an underlying graph S together with a set of atomic constraints $C^\mathfrak {S}$ specified by a predicate signature $\varSigma$. A predicate is used to specify constraints in a model by means of graph homomorphisms. DPF provides a formalization of multi-level metamodelling by defining the conformance relation between models at adjacent levels of a metamodelling hierarchy [10].

The graph in Fig. 3(b) represents the specification of a multi-agent model $\mathfrak {S}_1$ $= (S_1, C^{\mathfrak {S}_1}:\varSigma )$. Constraints are added into the structure by predicates. Figure 3(a) shows the predicates used for constraining the model $\mathfrak {S}_1$. Each predicate has a name p, a shape graph (arity) $\alpha$(p), a visualization, and a semantic interpretation. For instance, the intended semantics of is that for each instance of X, f must have at least n and at most m instances. The predicates are constraining the model $\mathfrak {S}_1$ by means of a graph homomorphism $\delta : \alpha (p) \rightarrow S_1$ from the arity of the predicate p to the graph of the model $\mathfrak {S}_1$. The model $\mathfrak {S}_1$ specifies that an agent may have a scope consisting of a number of states. An agent’s scope may have internal scopes of other agents. An instance ($I, \iota$) of $\mathfrak {S}_1$ is shown (represented in abstract syntax) in Fig. 3(c). The instance ($I, \iota$) of $\mathfrak {S}_1$ is given by a graph I together with a typing graph homomorphism $\iota : I \rightarrow S_1$ that satisfies the constraints $C^{\mathfrak {S}_1}$. The diagram shown earlier in Fig. 1 is the concrete syntax of this instance. The semantics of the predicates are provided in a fibred manner [4]. That is, the semantics of a predicate p is given by the set of its instances. The multiplicity predicate is used to add an atomic constraint on edge ‘contains’ in Fig. 3. This atomic constraint specifies that every Scope instance must contain at least one State instance. The irreflexive predicate is used to add an atomic constraint on edge ‘internal’. The atomic constraint specifies that a Scope instance cannot have reflexive reference of type ‘internal’.

Fig. 3.

A DPF specification $\mathfrak {S}_1$ for multi-agent model

We use the concept of a single ‘State’ in the multi-agent model to represent the condition of an agent and use the word ‘information state’ to represent an instance of a multi-agent model. An instance of an agent’s state is valid if the associated knowledge base is consistent. Let ($M,\iota$) be a multi-agent model instance consisting of a set of agents $\mathcal {A}$ (instances of Agent) and $\varPhi =$ KB($s_a$) be a set of horn clauses representing the knowledge base of a state $s_a$ in scope A of an agent $a \in \mathcal {A}$. The state $s_a$ is consistent or satisfiable if $\varPhi \nvdash \bot$. We define that a propositional logic formula $\varphi$ is true in $s_a$, written as $(M,\iota ), s_a \models \varphi$, as follows:

• $(M,\iota ), s_a \models p$ iff $p \in \varPhi ^*$ ($\varPhi ^*$ is the set of all logical consequences of $\varPhi$)

• $(M,\iota ), s_a \models \lnot p$ iff $p \notin \varPhi ^*$

• $(M,\iota ), s_a \models (\varphi \wedge \psi )$ iff $(M,\iota ), s \models \varphi$ and $(M,\iota ), s \models \psi$

• $(M,\iota ), s_a \models (\varphi \vee \psi )$ iff $(M,\iota ), s \models \varphi$ or $(M,\iota ), s \models \psi$

Let us consider that a scope A contains a set of states, S. Any formula $\varphi$ generated by the language of epistemic logic $\mathcal {L}_k$ is true in scope A (written as $(M,\iota ), \mathbf A \models \varphi$) or in a state $s_a \in \mathbf S$ (also written as $(M,\iota ), s_a \models \varphi$) as defined below:

• $(M,\iota )$, A $\models p$ iff $\forall s \in \mathbf S ~ (M,\iota ), s \models p$

• $(M,\iota )$, A $\models \lnot p$ iff $\exists s \in \mathbf S ~ (M,\iota ), s \nvDash p$

• $(M,\iota )$, A $\models (\varphi \wedge \psi )$ iff $\forall s \in \mathbf S ~ (M,\iota ), s \models \varphi$ and $(M,\iota ), s \models \psi$

• $(M,\iota )$, A $\models (\varphi \vee \psi )$ iff $\forall s \in \mathbf S ~ (M,\iota ), s \models \varphi$ or $(M,\iota ), s \models \psi$

• $(M,\iota )$, A $\models K_a \varphi$ iff $\forall s \in \mathbf S ~ (M,\iota ), s \models \varphi$

• $(M,\iota )$, A $\models K_b \varphi$ ($b \in \mathcal {A}~ \wedge ~ b \ne a$) iff $(M,\iota )$, B $\models \varphi$ where agent b’s scope B is an internal scope of A

• $(M,\iota ), s_a \models K_a \varphi$ iff $(M,\iota )$, A $\models K_a \varphi$

• $(M,\iota ), s_a \models K_b \varphi$ ($b \in \mathcal {A}~ \wedge ~ b \ne a$) iff $(M,\iota )$, A $\models K_b \varphi$

An instance of a multi-agent model (i.e., an information state of an agent) is valid if it satisfies all the domain constraints specified in the DPF specification and contains only valid states for agents.

4 Message Passing Communication

We envision a system where agents collaborate with each other by exchanging messages which include epistemic information. These messages are used to update the knowledge bases of agents and their information states. The agents have their own knowledge base, and in addition they are aware of other agents’ knowledge bases.

Fig. 4.

Predicates for annotating message instance

A message is an instance of the multi-agent model where the agents are annotated with [S] and [R] ( and predicates). Figure 4 shows the predicates and the abstract and concrete syntax of a message. A message contains a scope of an agent with a set of states. The states have an associated knowledge base which contains a set of propositional horn clauses. An incoming message from the sender agent is used to update the internal scope of the receiver agent. Two kinds of update operations are performed in order to update the internal scope of the receiver agent: (i) product of states (in the category of sets), and (ii) knowledge base revision. The product operation deals with the higher order information and the revision operation updates the knowledge base of states. Figure 5 illustrates an agent b sending a message to agent a. Agent b informs agent a that he does not know if it is foggy (represented by f) or not. The figure shows the effect of an update operation where a product is formed to update the information states of the internal scope B. After performing the product operation, the knowledge base of the states are revised based on the knowledge base from the message.

Fig. 5.

Example effect of an update

We consider Delgrande’s inconsistency based contraction [3] for knowledge base revision. The purpose of this type of revision is to modify the knowledge base in such a way that adding new horn clauses from the message does not result in an inconsistent knowledge base. While modifying the knowledge base we want to retain as much as possible from the old knowledge base. We use Delgrande’s definition of i-reminder set for the horn language:

Definition 4

(Horn i -Reminder Sets). Given a knowledge base $\varPhi$ in $\mathcal {L_{HC}}$ and a set of new horn clauses $\varPsi$, Horn i-reminder sets of $\varPhi$ w.r.t. $\varPsi$, written $\varPhi \downarrow _i \varPsi$ is the set such that $K \in \varPhi \downarrow _i \varPsi$ iff (i) $K \subseteq \varPhi$, (ii) $K \cup \varPsi \nvdash \bot$, (iii) $\not \exists K'$ such that $K \subset K' \subseteq \varPhi$, $K' \cup \varPsi \nvdash \bot$.

While updating the knowledge base $\varPhi$ of a state s of an agent a due to the new information $\varPsi$ of a message, we propose to use Horn i-reminder sets. If there are more than one element in $\varPhi \downarrow _i \varPsi$, multiple states are produced by replacing s containing different possibilities of revised knowledge base. However other strategies may be followed to revise $\varPhi$ such as Horn i-Contraction [2].

5 Conclusion and Future Work

Epistemic logic was first introduced by Hintikka in [7] and later on used by numerous researchers for modelling multi-agent systems where the information state of multi-agent systems are given by Kripke semantics [5, 6]. One issue with this approach is that models become very big in size as the number of epistemic alternatives increases. In this paper, we presented a model driven approach where the states are modularized in scopes which clearly represents agents dimension of epistemic alternatives. To extract the local and global knowledge base of agents, we use pullback, limit and colimit operations.

In future, we will investigate reasoning algorithms to rule out uncertainty. Reasoning about uncertainty may play an important role in optimizing resources via strategies. In [9], we introduced a categorical approach for metamodelling epistemic game theory. As part of the future work, we will investigate how game theoretic concepts can be applied in a multi–agent system environment using model driven engineering approaches.