Belief Manipulation Through Propositional Announcements

1 Introduction

We are concerned with the manner in which the beliefs of a group of agents can be manipulated by making public announcements of propositional formulas. Suppose that we have n agents, each with a set of current beliefs and an epistemic goal ψi. We are interested in finding a single formula φ such that each agent Ai will believe the corresponding goal ψi after a public announcement of φ. We address two problems related to this propositional announcement problem:

1. Is there always a solution, even when the goals are collectively inconsistent?
2. What is the complexity of finding a solution?

We also describe an implemented announcement finding tool, and demonstrate how it can be used as a robot controller.

Public announcements have been addressed in modal logic [Plaza, 2007]. The problem that we address roughly corresponds to the notion of an arbitrary public announcement [Balbiani et al., 2007] in the tradition of Dynamic Epistemic Logic (DEL) [Ditmarsch et al., 2008], except that we allow non-truthful announcements. The important distinction in our work is that we are interested in the simpler setting of propositional logic with AGM-style belief revision operators 1 . We focus on the AGM setting because we expect announcement finding to be computationally easier, as we avoid difficult problems due to nested belief. We argue that our approach is also appropriate for practical applications where the focus is on giving orders in the most efficient way possible.

This paper is an extension of [Hunter and Schwarzentruber, 2015], and it makes several contributions to existing work on the theory of belief change. First, we define arbitrary public announcements in an AGM setting. We demonstrate that the question is meaningful in this context, as there are natural applications where a reasonable treatment of announcements need not be concerned with nested beliefs. This paper can therefore be seen as part of the ongoing effort to connect the study of belief change between the AGM and DEL communities. The second contribution is a detailed analysis of the complexity of arbitrary announcements for a particular AGM revision operator, namely Dalal's revision operator [Dalal, 1988]. Finally, we make a practical contribution, as we introduce an implemented tool for finding announcements with respect to a range of different belief revision operators.

Motivating Example Consider a domain involving a robot controller, and n robots that act independently. The only way the controller can communicate with the robots is through broadcast messaging 2 . If there are constraints on messaging in terms of cost or timing, then the controller may seek to minimize the number of messages sent to ensure all robots have the correct beliefs. Towards this end, it is useful to send messages that will impact the beliefs of each robot differently.

As a concrete example, suppose that there are two surveillance robots R1 and R2 that are tasked with patrolling a certain area. If there is a breach at the gate, we would like one robot to go check the gate while the other continues patrolling. In order to achieve the desired behaviour, the controller would like to broadcast a single alarm message "breach" that will lead each robot to simultaneously have the appropriate beliefs about how they should behave. In this paper, we formalize this kind of reasoning in an abstract setting.

1 AGM stands for the highly influential approach to belief revision due to Alchourr`on, G¨ardenfors and Makinson [Alchourr´on et al., 1985].

2 Assumed here to be synchronous.

2 Preliminaries

2.1 Belief Revision

One highly influential approach to belief revision is the AGM approach, in which revision is captured by an operator that satisfies a particular set of rationality postulates [Alchourr´on et al., 1985]. The beliefs of an agent are represented by a belief set, which is a logically closed set of propositional formulas over a vocabulary P . In this paper, we assume P is finite; hence K, the belief set, is equivalent to a single formula. An AGM belief revision operator takes a belief set K and formula φ as input, and returns a new belief set that incorporates φ while keeping as much of K as consistently possible. We write |K| to denote the set of interpretations where K is true.

Every AGM revision operator ∗ has the property that, for any belief set K, there is an underlying total pre-order ≺K over interpretations of P such that |K ∗ φ| = min≺K (φ) [Katsuno and Mendelzon, 1992]. So AGM revision involves finding ≺K-minimal states consistent with a particular formula. One important example is the Dalal operator [Dalal, 1988], denoted by ∗d. For this operator, the underlying ordering is defined by the Hamming distance between interpretations. The Hamming distance between interpretations v, w is the number of propositional variables assigned different truth values by v and w. So then |K ∗d φ| is the set of models of φ that have minimal Hamming distance from a model of K.

Belief manipulation is concerned with the ability of one agent to convince another to hold certain beliefs. With some revision operators, agents can be manipulated to believe a target formula φ exclusively through indirect statements or evidence [Hunter and Booth, 2015]. The work in this paper can be seen as an exploration of multi-agent belief manipulation.

2.2 Dynamic Epistemic Logic

Dynamic Epistemic Logic (DEL) provides an alternative approach to reasoning about beliefs. In DEL, modal logics of knowledge and belief are combined with dynamic logic to model epistemic change. Standard modalities include K (knowledge), B (belief), and the parametrized announcement modality [φ]. The semantics of [φ] is defined as a restriction to worlds where φ holds. For an overview of DEL, we refer the reader to [Ditmarsch et al., 2008].

There have been versions of DEL that incorporate belief revision operators over worlds in the AGM sense; see, for example ([Benthem, 2007; Baltag and Smets, 2006; 2008]). In these logics, each agent a has an ordering over possible worlds and the semantics of [φ] is defined by model transformations that adjust the orderings.

The most obvious distinction between the AGM approach and the DEL approach to belief revision is the fact that the DEL approach permits the representation of nested beliefs. As a result, it is much more expressive. Also, some of the properties we expect in the AGM setting are no longer valid. For example, the Success postulate for AGM revision states that φ ∈ K ∗ φ. In a modal setting, this is equivalent to the schema [φ]Bφ. This is not valid in most multi-agent epistemic logics, because an announcement of φ often changes the world such that φ should not actually be believed. 3 .

3 This is the case in so-called Moore sentences, for example.

The fact that announcing φ does not ensure belief in φ leads to a natural question: how can we get another agent to believe something through announcement? This question is addressed in DEL via the logic of arbitrary public announcements [Balbiani et al., 2007]. Arbitrary announcement logic is similar, but not identical, to the problem addressed in this paper. First of all, we do not have belief revision operators in public announcement logic; we have only hard updates. Furthermore, in DEL, announcements are required to be truthful.

2.3 Known Complexity Results

In this section, we give some known complexity results related to public announcements. The first result is really the starting point for this work.

Theorem 1 ([French and van Ditmarsch, 2008]) Satisfiability in the logic of arbitrary announcements is undecidable.

Hence, if we have nested knowledge and a rich domain of Kripke structures, we can not hope to find public announcements to change the beliefs of agents in the desired manner. A simpler logic called DLPA-APAL (Dynamic Logic of Propositional Assignments with Arbitrary Public Announcement Logic) is defined in [Charrier and Schwarzentruber, 2015]. In DLPA-APAL, Kripke structures are restricted to include just one world with each valuation, and epistemic relations are represented by programs over propositional assignments.

Theorem 2 ([Charrier and Schwarzentruber, 2015]) Satisfiability in DLPA-APAL is NEXPTIME-complete for the single announcement case.

This result shows that restricting to reasoning over beliefs on valuations is decidable. Our goal in this paper is to show that if we restrict further, by removing nested beliefs, we can get a better complexity. This is true even if we consider willful manipulation, where announcements can be false.

3 The Propositional Announcement Problem

3.1 The Basic Problem

Given n agents and n AGM belief revision operators ∗i as input; we are looking for the existence of a consistent formula φ such that

where Ki and ψi represent the belief set and the goal of the agent i, respectively. Obviously, if ∧i ψi is consistent, then we can just revise by this. But this is not always the case.

Example Consider the robot controller example over the vocabulary {patrol, checkgate}. We think of this vocabulary as defining a state machine, where each interpretation represents a state; the robot can have actions that are triggered by transitions to given states. This is a standard control mechanism for simple agents in a video game setting, and it can function as a control mechanism for our simple robot agents as well. In our example, the patrol variable is true when the robot should be patrolling their area and the checkgate variable is true when the robot is supposed to check the gate.

Suppose we have two robots R1 and R2 with initial belief states defined as follows:

The controller believes there is a problem at the gate. Is there a formula that can be broadcast to immediately get R1 to check the gate while R2 patrols the grounds? In other words, is there a formula φ such that:

{¬patrol ∨ ¬checkgate} ∗ φ |= ¬checkgate ∧ patrol

The answer is yes; we can set φ = patrol.

The preceding example is framed in the context of the robot controller, but it also demonstrates an important case for propositional announcement. In particular, it shows that there are cases where the goals are inconsistent, yet a solution is possible.

3.2 Existence of Solutions

In this section, we give some basic results related to the existence of solutions for the propositional announcement problem. The following result is immediate.

Proposition 1 For all n > 1, there are instances of (1) with no solution.

Proof Assume the vocabulary {p}, let K1 = {p}, K2 = {¬p}, ψ1 = ¬p and ψ2 = p. It follows immediately that any solution φ satisfies φ |= p ∧ ¬p, so there is no consistent solution. □

The following result may be less obvious, but it is similarly straightforward. The idea is that, if there are "enough" propositional variables, we can set up a set of inconsistent goals that can be guaranteed by an appropriate revision.

Theorem 3 Let P be a vocabulary and let the number of agents n satisfy n < 2|P| . Then there is an instance of (1) over P with inconsistent goals that has a solution.

Proof Let P0, . . . , Pn be a list of mutually inconsistent maximal conjunctions over literals of P; we know that such a list exists, because there are 2|P| distinct maximal conjunctions of literals, and we know that 2|P| > n by assumption. For

Note that the conjunction ∧i ψi is clearly inconsistent. If we set φ = P0, then it is easy to verify that Ki ∗i φ |= ψi for each i, which is what we wanted to show. □

These results demonstrate that the general propositional announcement problem is non-trivial. There are instances with no solution and there are instances with solutions, and we can not easily identify which is the case without considering the possible revisions. This leads to the following question: How hard is it to determine if there is a solution to a given instance of the problem? We turn to this problem in the next section.

4 Complexity

4.1 The Decision Problem

In this section, we restrict the problem slightly by requiring that all agents have the same revision operator. Given n agents and an AGM revision operator ∗, we are looking for the existence of a consistent formula φ such that

where Ki and ψi represent the belief set and the goal of the agent i, respectively. In principle, ∗ could be any shared revision operator.

In practice, we will often be interested in the complexity of finding announcements; but we must first consider the corresponding decision problem.

The Propositional Announcement Problem (PAP(∗)) Input:

An integer n

A list K1, . . . ,Kn of formulas (initial beliefs).

A list ψ1, . . . , ψn of formulas (goals).

Ouput:

Yes, if there exists φ satisfying (2)

No, otherwise.

We refer to this problem as PAP(∗) to emphasize that it depends on some given operator ∗ on belief sets. We normally assume that ∗ is an AGM revision operator, but this need not be the case in general.

4.2 Announcement Existence

For the moment, we are interested in analyzing a simple case to obtain the most efficient algorithm possible. Hence, we consider Dalal's well-known revision operator based on Hamming distance[Dalal, 1988]. As in §2.1, we let ∗d denote Dalal's revision operator.

We present a non-deterministic algorithm that decides PAP(∗d). In the algorithm, we use non-determistic choice to select the minimum distance di between Ki and ψi. Also note that d(K, v) denotes the minimum Hamming distance between the set of models of formula K and interpretation v.

1. Let m be the size of the underlying input vocabulary of K1, . . . ,Kn, ψ1, . . . , ψn
2. Guess d1, . . . , dn ∈ {0, 1, . . . ,m}
3. Guess valuations v1, . . . , vn
4. For all i, j ∈ {1, . . . , n} If d(Kj , vi) < dj , reject.

We need to prove that EXIST ANN( ¯K, ¯ ψ) actually produces the desired result. In the proof, we write min≤Ki (φ) for the minimal Hamming distance from a model of φ to a model of Ki .

Theorem 4 Let ¯K = K1, . . . ,Kn and let ¯ ψ = ψ1, . . . , ψn be sequences of formulas. Then EXIST ANN( ¯K, ¯ ψ) accepts if and only if there exists φ such that Ki ∗d φ |= ψi for each i.

Proof Suppose that EXIST ANN( ¯K, ¯ ψ) accepts, and let us consider an accepting run. Let φ be a formula with ||φ|| = ⋃i {vi}, where the valuations vi are those from an accepting run guessed on line 2. By line 3,

because if this is not the case, the algorithm would have rejected the input. But then, by line 4,

In other words, for each i, the models of φ that are models of Ki are of distance di fromKi. Finally, since the conditions of all lines are false, it follows that for every v such that v |= φ, it must be the case that d(Kj, v) = dj implies v |= ψj. Hence, the minimal models of φ with respect to Ki are also models of ψi. So K ∗ φ |= ψi, which is what we wanted to show.

Now suppose that there exists φ such that Ki ∗d φ |= ψi for each i. For each i, define di = min≤Ki (φ). For each i, let vi denote one of the valuations of ψi such that d(Ki, vi) = di. We know that such a vi exists, since Ki ∗d φ |= ψi. If we guess ¯ d = d1, . . . , dn and ¯ v = v1, . . . , vn on lines 1 and 2 of the algorithm, then we have an accepting run. □

So EXIST ANN( ¯K, ¯ ψ) does what we want it to do: it determines if there is a public announcement φ such that each agent i believes ψi following revision by φ. We can also say something about the complexity. The initial guessing is a polynomial number of guesses with respect to the input length. Note that in the algorithm, tests d(Kj, vi) < dj etc. can be answered by an NP oracle. Hence, the algorithm intuitively seems to lie in the complexity class ΣP2 = NP NP . The following result makes this claim precise.

Proof After the initial guesses, the algorithm clearly runs in polynomial time other than the checks of the form d(K, v) < d at several stages. But recall that we are using the Hamming distance here, so this check can be performed as follows. Guess a set of atomic propositional variables of size less than d, and let v′ be the interpretation obtained from v by switching the truth values of these variables. If v′ |=K, then the minimum distance between K and v is less than d. This process is in NP.

Hence the entire algorithm runs in time NP with a polynomial number of calls to an NP oracle. This gives the complexity NP NP = ΣP2 , which was the desired result. □

Recall that announcement finding was NEXPTIMEcomplete in the modal case, even if we restricted possible worlds to be valuations. So this result shows that the problem is much easier in the AGM case. Note that hardness of PAP(∗d) is left as an open issue.

So far, we have restricted attention to Dalal's revision operator. This choice can be justified to some extent by the fact that Dalal's operator permits iterated revision, which we anticipate will be important in practice for a robot controller. Inspection of our proofs shows that the actual properties of the Hamming distance operator only occur in two places.

• When the minimum distance is guessed in the algorithm.
• In the checks of the form d(K, v) < d.

The advantage of Dalal's revision operator in both cases is that we have a polynomial number of steps, because the distance only ranges from 0 to the size of the vocabulary. However, this is obviously not true for other revision operators; we return to this point in the conclusion.

5 Implementation

5.1 Basic Approach

In this section, we are interested in a different question: can we use announcement finding to implement a feasible solution to a problem of practical interest? To answer this question, we describe a practical tool that uses announcement finding as the basis for a simulated robot controller.

We describe AnnB, an automated robot controller that calculates public announcements to manipulate the beliefs of agents and force them to perform particular tasks. The key points of operation for AnnB are as follows:

• Each agent has a set of beliefs and a revision operator.
• There is a fixed set of movement behaviours.
• Believing certain formulas causes an agent to perform behaviours.

In this environment, giving an agent information for revision can trigger changes in activity. Given a set of goal behaviours, AnnB computes the announcement required to change the beliefs of the agents in a way that gets each agent to perform a desired action.

AnnB is written in Kotlin 4 . It is built on the publicly available libraries of GenB [Hunter and Tsang, 2016]. Briefly, GenB is a general belief revision solver that is able to calculate the result of any AGM belief revision operation. There are built-in sample operators, but GenB also allows the user to specify any revision operator by giving the corresponding faithful assignment. Hence, building AnnB on the GenB framework gives us considerable flexibility.

4 Kotlin is a variant of java, available at www.kotlinlang.org.

5.2 Defining Behaviours

The first step is to specify the agents. This is done through a simple dialog box in which agents are added and given an initial belief state, as in Figure 1. By convention, we introduce a propositional variable that matches with the colour of the agent. This variable will initially only be believed by an agent of that colour. Figure 2 gives the simulation view.

After setting up the set of agents, we define behaviours through the behaviour definition table. Essentially, the behaviour definition table associates the truth of propositional formulas with movement on screen. Built-in algorithms define standard movement patterns such as wander, patrol, and find-path. The behaviour of an agent is determined by checking if it believes each formula in the behaviour window, starting from the top and working down. An example is given in Figure 3. In this example, the yellow agent is initially patrolling at position y = 0. The green agent is initially patrolling at position y = 2, because it does not believe the first two propositions. The final line in the behaviour table is the default behaviour that any agent should display if it does not believe any of the previous propositions.

5.3 Algorithm

The algorithm used by AnnB is based on EXIST ANN; however, there are several changes. First, the input includes a plausibility function Pi for each agent i. Informally, Pi(v) < Pj(w) indicates that agent i considers the valuation v to be more plausible than w. This function defines a faithful assignment, which allows any revision operator to be specified. The second difference is that the algorithm is deterministic, so it loops through possible values rather than guessing.

The following is a high level description of the algorithm. In practice, we interate over the di's starting each at 0 and incrementing one position at a time. We write form(¯ v) to mean the disjunctive normal form sentence obtained from a sequence of valuations in a the natural way.

1. Let m = maxi,s Pi(s)
2. For each ¯ d = (d1, . . . , dn) with 0 ≤ di ≤ m:
3. For each n-tuple ¯ v = (v1, . . . , vn) of valuations:
4. If Pj(vi) < dj for any i, j, continue.
5. If Pi(vi) > di for any i, continue.
6. If Pj(vi) = dj and vi ̸|= ψj for any i, j, continue.
7. Return φ = form(¯ v)
8. Return "no solution."

We can prove that this algorithm is correct.

Theorem 6 Let ¯K = K1, . . . ,Kn, and ¯ ψ = ψ1, . . . , ψn be sequences of formulas. Let P1, . . . , Pn be a sequence of plausibility functions. If φ is the formula returned by FIND ANN DET( ¯K, ¯ P, ¯ ψ) then Ki ∗i φ |= ψi for each i, where ∗i is the AGM revision operator obtained from the plausibility function Pi.

Proof Parallel to the proof of Theorem 4. □

In Figure 4, we give an illustration of the way this algorithm is used. Suppose that we would like the yellow agent to stop patrolling, and guard the north entrance. At the same time, we would like the red agent to continue patrolling. We can specify this behaviour in a declarative manner by indicating that yellow should no longer believe patrol, whereas red should continue to believe it. We can then find a suitable announcement by clicking the Find Announcement button. Clicking on Commit changes the beliefs of each agent, and causes the new behaviour to be exhibited in the simulation window.

5.4 Performance and Functionality

One advantage of AnnB is that it is able to solve the announcement problem for all AGM revision operators. However, if we would like to do a second revision, we need to supply a new set of plausibility orderings. While it would be possible to do this in accordance with a particular iterated revision operator, it must be done manually in the current software.

Due to the complexity result in Theorem 5, we can not expect a general announcement solver to find solutions quickly for large instances. For the application at hand, this is not a major limitation. We are able to define behaviours using a small set of variables and patterns, inspired by standard character movement in video games. However, run times for large instances quickly become unmanageable. To analyze the efficiency, we need to define and specify suitable bench mark problems in our domain of interest; such a specification is beyond the scope of the present paper. We leave a systematic analysis of the practical efficiency of AnnB for future work.

It is not our intention to suggest that AnnB can function as a complete robot control system. But it can play an important role. In general, the coordination of autonomous robots involves replanning when obstacles are faced [Coltin and Veloso, 2013]. When an obstacle is encountered by one Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

robot, a broadcast announcement is the simplest way to inform the others. By using an announcement finder, we can select an announcement that ensures all goals are acheived.

6 Discussion

6.1 Relation withModal Approaches

Belief revision has been addressed in several different modal frameworks, including [Benthem, 2007; Baltag and Smets, 2006; Caridroit et al., 2015; 2016]. The most obvious difference in our approach is that we are unable to capture nested beliefs. However, it is also significant that we are not constrained with any notion of the "actual" world. Indeed, the announcer is just searching for a formula that suitably interacts with the revision operators; this gives us a more flexible setting to address problems of belief manipulation.

Although we work in a propositional framework, our results are closely connected to modal work on announcement finding. In particular, we remark that we can actually reformulate PAP(∗) as a variant of the model checking problem of DEL with plausibility models ([Benthem, 2007; Baltag and Smets, 2006]). We create a (potentially exponentially bigger than K1, . . . ,Kn) pointed Kripke model M, w such that the valuations of the most plausible worlds in w are exactly models of Ki for all agents i ∈ {1, . . . , n}. Then we ask whether there exists a propositional formula φ such that M, w |= [φ]BR(B1ψ1, . . . , Bnψn) where [φ]BR is the announcement operator that semantically performs the belief revision for all agents and Bi is the belief operator for agent i.

6.2 FutureWork

We have only considered the complexity of announcement finding in the case of the Dalal's revision operator, where the number of levels in the plausibility ordering is at most |P| (the size of the vocabulary). In general, the worst case complexity to check all levels of a total pre-order over a vocabulary of size P will be 2|P| . If we are actually required to make this many checks, then the decision problem for other revision operators would lie at a higher level of the polynomial hierarchy. This would not be surprising, as it is known that Dalal's operator is computationally simpler than other AGM revision operators [Eiter and Gottlob, 1992]. We leave the complexity of additional AGM operators for future work.

It would also be useful to consider announcement finding for iterated revision in the tradition of Darwiche and Pearl [Darwiche and Pearl, 1997; Jin and Thielscher, 2007]. In this context, the problem takes n agents and n Darwiche-Pearl revision operators ∗i as input. We are looking for the existence of a consistent formula φ such that ψi ∈ min(≺i ∗i φ) for each i, where ≺i and ψi represent the epistemic state and the goal of the agent i, respectively. Following [Liberatore, 1997], we expect the complexity will be higher in this case.

At a practical level, improvements can be made to AnnB. One obvious direction for future work would be to improve the running time of the algorithm through suitable heuristics, or by using an efficient SAT solver for the NP calculations. We are also interested in moving past simulation to a prototype controller for real, physical robots using our tool.

6.3 Conclusion

We have considered arbitrary public announcements in the setting of propositional belief revision. We have proved that the decision problem for announcement finding in this setting is computationally simpler than it is in a modal setting, even under very strong simplifying assumptions. We have argued that this result is important, because revision by announcements can be used in practical applications where the notion of fully nested beliefs is not required. This has been demonstrated in practice through the development of robot control software based on announcement finding.

Acknowledgements

Many thanks are due to Hans van Ditmarsh, who hosted the first two authors as visitors at the Lorrainne Research Laboratory in Computer Science and its Applications (LORIA) while they wrote an early version of this paper.