-What happens when distributed sources of information (agents) hold and acquire information locally, and have to communicate with neighbouring agents in order to refine their hypothesis regarding the actual global state of this environment? This question occurs when it is not be possible (e. g. for practical or privacy concerns) to collect observations and knowledge, and centrally compute the resulting theory. In this paper, we assume that agents are equipped with full clausal theories and individually face abductive tasks, in a globally consistent environment. We adopt a learner/critic approach. We present the Multi-agent Abductive Reasoning System (MARS), a protocol guaranteeing convergence to a situation “sufficiently” satisfying as far as consistency of the system is concerned. Abduction in a full clausal theory has however already a high computational cost in centralized settings, which can become much worse with arbitrary distributions. We thus discuss ways to use knowledge about each agent's theory language to improve efficiency. We then present some first experimental results to assess the impact of those refinements.
In multi-agent systems, the inherent distribution of
autonomous entities, perceiving and acting locally, is the source
of many challenging questions. To overcome the limitation
of their own knowledge, usually local and incomplete, agents
are driven to form some hypotheses and share information
with other agents. Especially, abductive reasoning is a form of
hypothetical reasoning deriving the possible causes of an
observation. It can be used to complete an agent’s understanding
of its environment by explaining its observations, or, more
proactively, for planning, as one can try to find the possible actions
that might cause the completion of a goal. However reasoning
in a sound manner with distributed knowledge rises interesting
problems, as one cannot ensure locally the consistency of an
information. Moreover, the system often comes with severe
communication restrictions, due to physical (e. g. the limited
scope of a communication device) or reasoning (e. g. the mere
impossibility to consider all the potential communications)
limitations of agents populating it. For such situations, we
presented in [
Distributed abduction has been considered in recent years
in the ALIAS system [
The rest of this paper is as follows. Section II gives the necessary background on abduction and consequence finding. Then, Section III describe formally a multi-agent abduction problem, and present the MARS protocol, giving details about the communications exchanged over its execution. Efficiency is then discussed, and we describe two improvement on the previous protocol. These variants are then experimentally tested in Section IV, and we conclude in Section V.
First, we review some notions and terminology to represent our problem in a logical setting. A literal is an atom or the negation of an atom. A clause is a disjunction of literals, and is often denoted by the set of literals. A clause {A1, . . . , Am, ¬B1, . . . , ¬Bn}, where Ai and ¬Bj are respectively positive and negative atoms is also written as A1 ∨ . . . ∨ Am ← B1 ∧ . . . ∧ Bn. Any variable in a clause is assumed to be universally quantified at the front. A clausal theory is a finite set of clauses which can be identified with the conjunction of the clauses. Let S and T be clausal theories. S logically implies T , denoted as S |= T , if and only if for every interpretation I such that S is true under I, T is also true under I. |= is called the entailment relation. For a clausal theory T , a consequence of T is a clause entailed by T . We denote by T h(T ) the set of all consequences of T . Let C and D be two clauses. C subsumes D, denoted C D, if there is a substitution θ such that Cθ ⊆ D. C properly subsumes D if C D but D 6 C. For a clausal theory T , μT denotes the set of clauses in T not properly subsumed by any clause in T .
We can now introduce the notion of characteristic clauses,
which represents “interesting” consequences of a given
problem [
The logical framework of hypothesis generation in abduction for the centralized case can be expressed as follows. Let T be a clausal theory, which represents the background theory, and O be a set of literals, which represents observations. Also let A be a set of literals representing the set of abducibles, which are candidate assumptions to be added to T for explaining O. Given T , O and A, the abduction problem is to find a hypothesis H such that: (i) T ∪ H |= O (accountability), (ii) T ∪ H 6|= ⊥ (consistency), and (iii) H is a set of instances of literals from A (bias). In this case, H is also called an explanation of O (with respects to T and A). A hypothesis is minimal if no proposer subset of H satisfies the above three conditions (which is equivalent to subsumption minimality for ground clauses). A hypothesis is ground if it is a set of ground literals (literals containing no variable). This restriction is often employed in applications whose observations are also given as ground literals. In the following, we shall indeed assume that observations are grounded, and that we are only searching for minimal ground hypotheses.
Given the observations O, each hypothesis H of O can
be computed by the principle of inverse intailment [
SOLAR [
Once possible hypotheses have been computed, a ranking
process can be applied to select a preferred hypothesis (e.g.
hypothesis ranking such as in [
We propose here a new formalization of our problem as a multi-agent abductive system, which is defined as a tuple hS, {Γt}, A, ≥pi, where: • S = {a0, . . . , an−1} is a set of agents. Each agent ai has its own individual theory Ti and its own observations Oi. It will also form its own preferred hypothesis Hi, though it can also adopt it from other agents. In fact, in the end of the process, all agents will share the same hypothesis. • Γt = hS, Eti is the communicational constraint graph at time t, an undirected unlabeled graph whose nodes are the agents in S and whose edges Et represent the communicational links between the agent. An agent ai can only communicate with another agent aj at time t if (ai, aj ) ∈ Et. • A is the common set of abducibles that represents the langage bias of the abductive process. • ≥p is the common preference relation, a total order over hypotheses.
Theories and observations are considered to be certain knowledge. As such, they are assumed to be consistent, meaning that Si<n Ti ∪ Si<n Oi 6|= ⊥. To ensure termination, it will also be assumed that Carc(Si<n Ti, hLi) is finite, and that both hypotheses and observations are ground (i.e. contain no variable). Moreover, the system will be assumed to be temporally connected, meaning that at any time t, the graph Γt+ = hS, St′≥t Et′ i is a connected graph.
Our aim is then to ensure the formation of an abductive explanation of Si<n Oi with respects to Si<n Ti and A. Given a group of agents G = {ai, i ∈ J } ⊂ S, we shall say that a hypothesis H is group-consistent with G iff it is consistent with the union of all the individual theory of the agents of the group, that is, iff Si∈J Ti∪H 6|= ⊥. Likewise, we shall say that H ensures group-accountability for G iff it can explains all observations of the agents of the group when it is associated with the union of their theories, that is iff Si∈J Ti ∪ H |= Si∈J Oi. If G = S, we shall say that the hypothesis is masconsistent or that it ensures mas-accountability. Finally we shall say that a set of literals is acceptable for a group G iff it is a set of grounded literals of A that is group-consistent with G and ensures group-accountability for G. The objective of a multi-agent abductive system is thus to find a hypothesis that is acceptable for the whole system.
While consistency or accountability of a hypothesis with respect to both (Ti, Oi) and (Tj , Oj ) is not equivalent to consistency or accountability wrt (Ti ∪ Tj , Oi ∪ Oj ), we still can ensure some relation between them in classical logic. Specifically, group-inconsistency of H with G implies groupinconsistency of H with any superset of G, which ensures that hypothesis inconsistent with a sub-group of agents (possibly a single agent) can be ruled out as a potential solution. Moreover, group-accountability of H for both G and G′ implies group-accountability of H for G ∪ G′ (but not reciprocally), which ensures that accountability can be checked locally.
In order for a learner agent to propose a hypothesis to a critic, it is necessary that his agent can produce such a hypothesis. However, given only a few clauses of the whole clausal theory, it might not be able to find an explanation for the observations using only abducibles. Therefore, we shall allow an agent to build partial hypothesis, which contains some non-abducible literals. Those literals might be the unexplained observations, or preferrably some other literals of the language that would explain it. While interacting with other agents, they will share knowledge to expand these hypotheses in order to progressively build a fully abducible one. Note that of course, a hypothesis respecting the bias condition will always be favored over one who does not.
We shall now present MARS, a mechanism for solving multi-agent abductive problems based on SOLAR.
To deal with distributed hypothesis formation in multiagent systems, we take a learner-critic approach, in which learner agents aim at producing a globally adequate hypothesis through internal computations and local interactions with other agents acting as critics. In our abductive setting, however, critic agent cannot ensure the consistency of the hypothesis 14C→L noHyp
propose repropose
okCtx 6L
ackCtx
by itself, and needs to interact with the learner in order to
find incoherence (computing the context of a hypothesis) and
produce complete hypotheses (exchanging useful information
by justifyin partial hypotheses). The underlying mechanism
was presented and proved correct in [
checkCtx checkCtx
ackinc accept
hasBetterHyp
Fig. 1. Multi-Agent Learner-Critic Abductive Protocol.
Fig. 1 illustrate this protocol. Nodes indicate states of the agents (steps of the mechanism), with superscript L or C indicating whether it concerns the Learner agent or the Critic agent. Note that states 13 and 14 indicate a switching of the roles, as the critic becomes the learner. Labeled arcs indicate that a given message can be sent by an agent in a given state, making the other agent go to the target state upon reception. Dashed arcs indicate an internal change of state without communication. This mechanism is divided in four main steps that we shall now detail.
1) Hypothesis selection: An interaction is initiated by a learner agent a0, in state 1L, proposing its hypothesis and its validity context to a critic agent a1 (propose(H0)). If learner’s information has changed since it last computed its possible hypotheses, it will recompute them through inverse entailment, using A¯ as a production field. In case it cannot find a hypothesis this way, it will compute a partial hypothesis by using an extended set of abducibles (possibly the whole language). If the proposed hypothesis h0 is a new one, the first context Ctx0 will be computed as the new consequences of 11L propose incons incons okCtx ack 5L 4C uncovered argue deny
13C→L
withdraw 12C withdraw
ack 8L 10L
h0 ∪T0 wrt h0, that is N ewcarc(T0, h0, PL) where PL = hLi. Otherwise, the previously computed context will be used as initial context Ctx0. Then, when receiving such proposal, a1 will start its critic, which consists of three steps: consistency check, accountability check and admissibility check. As the interaction continue, new hypotheses might have to be proposed. If the current learner cannot propose a hypothesis (which can only happens if it has blocked all its possible hypotheses during preivous admissibility check), it will send noHyp to the other agent to switch the roles (state 14). If this one has also exhausted all its hypotheses, then it will unblock all its hypotheses and propose again the best one (repropose). Note that the new critic agent will also unblock all its hypotheses when receiving such a message.
2) Consistency check: When receiving a proposed hypothesis and context, the first step of the critique is to check the group-consistency of the hypothesis with both agents involved. A context is progressively built for a given hypothesis H to compute the new consequences of H ∪ T0 ∪ T1 wrt to T0 ∪ T1. If the hypothesis is incoherent, then it will have ⊥ as a consequence. The occurence of a contradiction between the context and the agents’ theories will thus enable detection of incoherent hypotheses. This relies on the fact that the global theory itself is assumed to be consistent, so any inconsistency can only arise from the hypotheses. Indeed, if T is consistent and T ∪ H is inconsistent, then N ewcarc(T , U, PL) = {⊥}. The process is as follow :
1. First, remember that during the hypothesis selection step, learner agent a0 retrieve context Ctx0 of its hypothesis. If no context have been memorized from previous iteraction, then a new one is computed as N ewcarc(T0, H0, PL) (note that we should thus have H0 ∈ Ctx0).
2. When receiving H0 and Ctx0 (state 2C ), a1 first check if it already has some context Ctx′ for this given hypothesis. If it is the case, then it replaces Ctx0 by Ctx′0 = Ctx0 ∪ Ctx′. Context Ctx1 is then computed as N ewcarc(T1, Ctx′0, PL), and sent back to a0 with message CheckCtx(Ctx1)(unless a contradiction is found).
3. The process continues. At each step Ctxi is computed by agent aα as the new consequences N ewcarc(Tα, Ctxi−1, PL), where α = 0 if i is odd (state 3L), and α = 1 otherwise (state 2C ), and sent with a checkCtx message.
4. This computation stops when either a contradiction is found or Ctxi is included in either Ctxi−1 or Ctxi−2, in which case all consequence have been computed. • If an inconsistency is discovered, the part p0 of the hypothesis responsible for it is sent to the other agents with message incons(p0). leading eventually to state 5L. Both agents rule out p0 (and any hypothesis containing it) by adding its negation to their theory. The learner agent then move on to its next hypothesis and propose it, trigerring a new critic phase (states 12C and 1L). • Otherwise, the end of the computation is acknowledged by sending okCtx. Both agents memorize the final context Ctxf = Ctxi ∩ Ctxi−1 (where i is the final step) of this hypothesis. Any element in respectively Ctxi \ Ctxi−1 and Ctxi−2 \ Ctxi−1 are added to T1−α and Tα where again α = 0 is i is odd and 1 otherwise. Indeed an element will only be removed from the context if it is a direct consequence of one of the agent’s theory.
The critic phase move to the next step (state 7C ).. 3) Accountability check: In this step, the critic agent checks if all its observations are explained by H0 ∪ T1. If an unexplained observation o is found, the message uncovered(o) is sent to the learner agent, now in state 8L. We then have two possibilities.
• If o is not explained by H0 ∪ T0, it is a true counterexample. The learner agent then computes a new hypothesis that will also cover o, and propose it, triggering a new critic phase (states 12C and 1L). • If o is already explained by H0∪T0, then the learner agent will notify the critic of this fact with argue(p0), where p0 is the part of the hypothesis that is used in explaining o with T0. The critic agent will add the clause {o ∨ ¬p0} in its theory2. This new information will ensure that the critic agent can find the hypothesis on its own in further steps, or build up upon it. It will then proceed to the next unexplained observation.
If there is no unexplained observation, the critic proceeds to the next step (state 9C ).
4) Acceptability check: Any hypothesis that reaches this step is consistent and accounts for the observations, but it might include some non-abducible literals, or unnecessary parts. This step ensures that alternative hypotheses are explored if needed.
1. If the critic has a hypothesis Hc that is prefered to H0 (according to ≥p), it will reverse roles (hasBetterHyp) and submit it. This will finally either result in the acceptation of a better hypothesis, or cause the former critic agent to learn why its hypothesis cannot be used.
2. Otherwise, if the hypothesis contains non-abducibles (partial hypothesis), the critic agent will temporarily block it, and ask the other agent to do the same (deny). I will then also switch roles (state 13C→L). This ensures that all partial hypotheses that could provoke information exchange leading to building an abducible hypothesis are explored if needed.
3. If the hypothesis is acceptable, or if a partial hypothesis has been reproposed (meaning the exploration is complete), then the critic send an accept message. The final outcome of the interaction is thus chosen. Hypotheses that were temporarily blocked are unblocked, and the best hypothesis is chosen as the final hypothesis. It is adopted and memorized by both agents, ending the interaction.
Each interaction allows the participants to refine their hypotheses and augment their knowledge concerning their consequences. The protocol described before is enough to allow two agents to form a hypothesis that is group-consistent and 2Note that since p is a conjonction of literals, ¬p0 is indeed a clause. ensures group-accountability for the pair of agents. When more agents are involved, it is possible to chain such interactions to converge towards a consistent state of the system. To take into account possibly variable communication constraints in the system, we propose a rumor-like approach, ensuring the local behaviour and interactions of the agents make the system converges to a state in which all agents have a mas-consistent hypothesis ensuring mas-accountability.
An agent is motivated by the will to ensure it has an explanation with respect to its neighours. As such, it will attempt to have local interactions with them whenever needed to ensure that, memorizing the result of their last interaction with each of their neighbours. In practice, an agent ai will engage in a local interaction with a neighbour aj whenever its hypothesis and context (hi, Ctxi) differ from those obtained during its last interaction with aj.
In [
The main computational cost of our mechanism lies in the multiple calls to a consequence-finding tools, which is used in the various steps to conduct the logical reasoning, especially for computing possible hypotheses through inverse entailment, computing the context of these hypotheses, and checking their accountability. To improve efficiency, it is thus crucial to reduce as much as possible the computational cost of each of these calls, as well as to reduce their number.
The tools we are using in our implementation, SOLAR, is based on tableaux methods. We assess the computational cost of a call by counting the number of inferences performed during it. Without entering in the details of the procedure, we will discuss here the factors that influence the cost of the computation of N ewcarc(F, T , PL). The number of inferences is directly related to the number of clauses used in the procedure. Used claused are clauses which can resolved with one of the top clauses (elements of F ), or with a consequence of them. Thus, reducing the number of clauses in T and more importantly in F can both help to reduce the computations steps. Note that Carc(T , PL) is in practice computed as N ewcarc(T , ∅, PL), so computing new consequences rather than all consequences is already a good step to ensure better efficiency. Reducing the number of literals of the top clauses also helps as it limits the number of clauses they can be resolved with. Then, another factor that can affect the computations is the size of the production field. A small production field limits the number of options to be explored and as a results, the number of inferences to be done.
With respects to our mechanism, these considerations means that we should keep each agent’s individual theory as small as possible, which is ensured by adding single clauses with just the necessary parts of the hypothesis to memorize inconsistencies (when sending or receiving incons.(p0) or accountability arguments (when sending argue(o ∨ ¬p0) in state 8L). Moreover, during consistency check, we should minimize the computations for the context. We shall see in next subsection how to reduce size of top clauses during this step by doing incremental computations. Then, we should also find ways to minimize the number of consequences computed during this consistency step by focusing on consequences that could lead to a contradiction, and even more importantly, to limit the number of partial hypotheses computed by focusing on those partial hypotheses that could trigger information exchanges leading to the formation of an acceptable hypothesis (as it would also reduce the number of applications of SOLAR).
During consistency check, context is progressively computed until it does not evolve anymore, but sending the whole context at each step of the computation and using it as top clause for computing the next step. To avoid redundant communications and computations, we propose to communicate only the new consequences of the context, pruning consequence discovered in previous step. It does not change the computation and sending of Ctx0 and Ctx1, but after computing Ctx1, the learner agent will only send back ctxStep1 = Ctx1 \ Ctx0 (note that we use the original Ctx0 here, and not Ctx′0).
Then, when receiving checkContext(ctxStepi), agent aα first computes N Ci+1 = N ewCarc(ctxStepi, Tα ∪ Ctxi−1). It can then use it to compute the current context Ctxi+1 = Ctxi−1 ∪N Ci+1, and send the update ctxStepi+1 = N Ci+1 \ ctxStepi. If there is a clause c than is in ctxStepi that is not subsumed by any clause of N Ci+1, it means that it is a consequence of Tα. It should then be sent to the other agent (with message inf orm(c)) to ensure that both agents will have the same final context. This replaces the theory adjustment with Ctxi \ Ctxi−1 and Ctxi−2 \ Ctxi−1 that were made before. Note that the termination condition becomes much simpler, as the context can be confirmed as soon as ctxStepi is empty.
1) Languages: Given a clausal theory T, we denote by
L(T ) the set of non-logical symbols that occur in T , and
by L(T ) the language formed upon them. Each agent has
its own theory Ti, from which we can define its individual
language L(Ti). We can then compute for each pair of agent
ai, aj (i 6= j), in the manner of [
2) Context narrowing: When computing context, we want to ensure that any new consequence of the hypothesis that can be derived from the union of the agent’s theories is indeed found. It means a0 need to send any consequence of H wrt T0 that could resolved with a clause of T1. In pratice, a0 compute its context using its restricted individual language as a production field, and then retain in Ctx0 only the one that contains at least a literal of the concerned communication language (here L0,1). Upon receiving it, a1 will then temporarily add L(Ctx0) to L0,1, and if it already has a context Ctx′, a1 will use the same pruning before adding it to get Ctx′0 and compute Ctx1 (with his restricted individual language as a production field). The pruning (with updated language) is applied to Ctx1 (or ctxStep1) before sending it, and the process continue. Each time, contexts are pruned to exclude any clauses that do not have literals in the current communication language before being sent to the other agent. Note that since we compute only new consequences, we cannot directly use the communication language as a production field,as shown by the following example:
Example 1: Let’s take T0 = {¬h∨a∨b, ¬h∨o}, T1 = {¬a} and T2 = {¬b}, all agents being connected. We have L0,1 = L({a}), and L0,2 = L({b}), so L0 = L({a, b}). We assume a0 has observation o and wants to check hypothesis h with a1. If Ctx0 was computed with L0,1, it would be empty, and no contradiction would be found when a0 checks later with a2. However, using L0 as a production field, we get consequence a ∨ b that contains literal a ∈ L0,1. It is thus sent to a1 that will give in return b. When proposing this context to a2 later on, a0 will thus be able to derive a contradiction.
3) Choice of partial hypotheses: For computing partial hypotheses, and deciding whether to propose a given one to a neighbour or not, the same principles can be used. When no admissible hypothesis can be found, inverse entailment is performed again with an extended set of abducibles. To ensure that at least one solution can be found, the manifestations are added to the abducibles, enabling trivial explanations for some part of the hypothesis. Then, the idea is to use literals that can act as links between the theories. In practice, it means that we should include in the extended abducibles the literals in the restricted individual language of the agent. This should also be augmented with literals obtained through the arguments of other agents (when receiving argue(o ∨ p0) in state 7C ). This allow us to compute all potentially useful partial hypothesis. For a given exchange, however, it is sufficient to propose those partial hypotheses that contains at least one literal of the communication language of the interacting agents.
We describe here preliminary experimental results on a small set of problems4, testing our two improvements of the MARS protocol (namely, incremental context computation and restriction of the languages). Though it might be useful to assert the validity of our conclusions on a broader number of problems, we believe that the small problems used for evaluation highlight the main difficulties that can be encountered in a distributed abduction system.
The first problem, pb-1, is taken from [
Tables I gives the results for the four variants of our mechanism. Computational cost is given by the total number of operations performed by the consequence finding tool over the course of the protocol, whereas communicational cost is expressed as the total number of bits exchanged by the agents during the process. From these results, it is obvious that using individual communication languages does indeed greatly reduce both costs. It is especially true for the most complex problems, and the gain ratio is more important when there 4Complete description of all these problems can be found at http://rjcia09.fr/MARS.
TABLE I
EXPERIMENTAL RESULTS Language focus Incremental ctx comp.
Computational cost Pb-1 Pb-1 (line) Pb-1 (clique) Pb-fvar (line) Pb-fvar (clique) Chain 8.2 Chain 8.4 (line) Chain 8.4 (circ.) Chain 8 (line) Chain 8 (circ.) Schedulevar Scheduledir Communicational cost Pb-1 Pb-1 (line) Pb-1 (clique) Pb-fvar (line) Pb-fvar (clique) Chain 8.2 Chain 8.4 (line) Chain 8.4 (circ.) Chain 8 (line) Chain 8 (circ.) Schedulevar Scheduledir 2 ag. 3 ag. 3 ag. 3 ag. 3 ag. 2 ag. 4 ag. 4 ag. 8 ag. 8 ag. 8 ag. 8 ag. 2 ag. 3 ag. 3 ag. 3 ag. 3 ag. 2 ag. 4 ag. 4 ag. 8 ag. 8 ag. 8 ag. 8 ag. are a greater number of communicational links. Incremental computation of context is however less convincing, as it only helps when there are several context computations step, which is not such a common occurence, unless theories are really mixed (it is the case for pb-1 and all chain_8 problems, which do benefit from this improvement). In the end, this improvement is useful, but only marginally so in most situations. While more experiment would be required to say anything more definite, the present results give us some hint about the influence of topology and “encoding”. Having a topology with cycle can lead to redundant computations, but can also provide easier exchange of information by avoiding the extra cost of bringing back a crucial fact or rule (as demonstrated by the addition of the link a0-a7 in chain_8). Overall, using individual communication language allows us to reduce the cost of redundant computations, so that we can take more benefit from situations where additional links are helpful. Moreover, reducing the number of agents can be either detrimental (in chain_8) or benificial (in pb-1): the size of the communication languages seem to be a more relevant factor. At last, the huge difference between schedulevar and scheduledir seems to indicate that our protocol is much more efficient for finding whether an abducible hypothesis is consistent than it is for finding an abducible hypothesis by exploring all partial hypotheses. When formalizing a given problem, it is thus more efficient to ensure one agent can easily generate candidate hypotheses, and express rules that constrain it.
We presented in this paper a formalization of a
multiagent abduction problem, and proposed a sound mechanism
for computing an abductive explanation that is guaranteed to
find a solution whenever one exists. We then discussed way to
improve the average efficiency of this protocol, called Multi
agent Abductive Reasoning System (MARS). Two
improvements were proposed. The first one reduce the costs of building
a complex context by doing the computation incrementally.
It only helps when several steps are needed and was
therefore shown to have only a limited impact on efficiency by
experimenal results. The main improvement consist of using
informations about the individual language of each agent to
focus the exchanges on what can really advance the search for
a hypothesis (or the inconsistence of a candidate hypothesis).
Contrarily to [