On Verifying Expectations and Observations of Intelligent Agents

1 Introduction

Agents have expectations about the world around, and they reason on the basis of what they observe around them, and such observations may or may not match with the expectations they have about their surroundings. Let us first provide two examples showing the diverse nature of such reasoning phenomena.

• Consider a person traveling from Switzerland to France in a car. Here is one way she would know whether she is in France. According to her expectations based on the traffic light signals of the different states, if she observes the sequence of (green∗ -amber-red∗ )∗ (∗ denotes the continuance of such sequences), she would know that she is in France, whereas if she observes (green∗ - amber-red∗ -amber)∗ , she would know that she is not.
• Consider three agents denoted by Sender (S), Receiver (R) and Attacker (A). Suppose S and R have already agreed that if S wants to convey that some decision has been taken, S would send a message, say m, to R; otherwise, S would send some other message, say m′ , to R. Suppose also that A has no information about this agreement. Then upon getting a message from S, there would be a change in the knowledge state of R but not A.

The first example concerns a certain rule that we follow in our daily life, and the second example brings in the flavour of coded message-passing under adversarial attacks. Expectations about the moves and strategies of other players also occur naturally in game theory, and possible behaviours of players are represented in these terms. Moving from theory to actual games, in the strategy video game Starcraft 1 , one player may know/expect that the other player will attack her base as soon as possible, and thus may play accordingly. Games like Hanabi 2 , and Colored Trails [de Weerd et al., 2017] also consider the connection between expectations and observations regarding the moves and strategies of the other players.

The challenge now is to build intelligent systems that are able to reason about knowledge regarding expectations, and plan accordingly. Whereas epistemic logic [Fagin et al., 1995] and more generally, its dynamic extensions, popularly known as dynamic epistemic logics (DEL) [van Ditmarsch et al., 2008] help us to build agents that reason about knowledge, they do not offer any mechanism dealing with expectations. In the same way, epistemic planning, based on the model checking of DEL ([Bolander et al., 2020]), extends classical planning with epistemic reasoning, but is unable to take agent expectations into account. Fortunately, following [Wang, 2011], Public observation logic (POL) [van Ditmarsch et al., 2014], a variant of DEL, reasons about knowledge regarding expectations. POL provides dynamic operators for verifying whether a given epistemic property holds after observing some sequence of observations matching certain expectations that are modelled by regular expressions π.

However, investigations on algorithmic properties of POL were left open. In this paper, we show that the POL model checking is decidable and PSPACE-complete. Our result relies on automata theory and the careful use of an oracle for deciding the algorithm running in poly-space.

For practical purposes, we investigate syntactic fragments that offer better complexities than reasoning in the full language of POL (see Figure 1), and are suitable for relevant verification tasks:

• the Word fragment, where any regular expression π is a word, is sufficient to verify that some given plan leads to a state satisfying some epistemic property;

1 https://en.wikipedia.org/wiki/StarCraft (video game)

2 https://en.wikipedia.org/wiki/Hanabi (card game)

• the Existential fragment, where the dynamic operators of POL are all existential, is suitable for epistemic planning (e.g., does there exist a plan?);
• the Star-Free fragment, where the regular expressions π are star-free, embeds bounded planning (in which sequences of observations to synthesize are bounded by some constant). In particular, the Star-FreeExistential fragment (i.e. the intersection of the Star-Free and the Existential fragments) is suitable for bounded epistemic planning.

Outline. Section 2 recalls POL with a formal presentation of the two examples mentioned in the introduction. Section 3 deals with all our complexity results about the model checking problem of POL. Section 4 shows the applicability of POL and its fragments in modelling interactive systems. It also includes a discussion on the implementation. Section 5 presents the related work and section 6 concludes the paper.

2 Background and Preliminaries

We first provide an overview of public observation logic (POL) as introduced in [van Ditmarsch et al., 2014]. Let I be a finite set of agents, P be a countable set of propositions describing the facts about the world and Σ be a finite set of actions. Below, we will not differentiate between the action of observing a phenomenon and the phenomenon itself.

2.1 Observations

For our purposes, we assume observations to be finite strings of actions. In the traffic example, an observation may be green-amber-red-green (abbreviated as garg) or, greenamber-red-amber-green (abbreviated as garag), among others, whereas, in the message-passing example, an observation is either m or m′ . An agent may expect different (even infinitely many) potential observations at a given state, but to model agent expectations, they are described in a finitary way by introducing the observation expressions (as regular expressions over Σ):

Definition 1 (Observation expressions). Given a finite set of action symbols Σ, the language Lobs of observation expressions is defined by the following BNF:

where ∅ denotes the empty set of observations, the constant ε represents the empty string, · denotes concatenation, + is union, ∗ represents iteration and a ∈ Σ.

In the traffic example, the observation expression (g∗ar∗ )∗ models the traveller's expectation of traffic signals in case she is in France. In the other one, the expression m models the expectation of the receiver in case a decision is made.

The size of an observation expression π is denoted by |π|. The semantics for the observation expressions are given by sets of observations (strings over Σ), similar to those for regular expressions. Given an observation expression π, its set of observations is denoted by L(π). For example, L(m) = {m}, and L((g∗ar∗ )∗ ) = {ε, a, ga, ar, gar, gargar, . . .}. The regular language π\w is the set of words given by {v ∈ Σ∗ | wv ∈ L(π)}. The regular language prefixes(π) is the set of prefixes of words in L(π), that is, w ∈ prefixes(π) iff ∃v ∈ Σ∗ such that wv ∈ L(π) (namely, L(π\w) ̸= ∅). 3

Example 1. (g∗ar∗a)∗ \(garaga) = r∗ (g∗ar∗a)∗ denotes the language of words {v : garaga · v ∈ L((g∗ar∗ )∗ )}. The set prefixes((g∗ar∗a)∗ ) contains garaga. However, garg is not in prefixes((g∗ar∗a)∗ ) and (g∗ar∗a)∗ \(garg) is empty.

2.2 Models

Epistemic expectation models [van Ditmarsch et al., 2014] capture the expected observations of agents. They can be seen as epistemic models [Fagin et al., 1995] together with, for each world, a set of potential or expected observations. Recall that an epistemic model is a tuple ⟨S,∼, V ⟩ where S is a non-empty set of worlds, ∼ assigns to each agent in I an equivalence relation ∼i⊆ S × S, and V : S → 2P is a valuation function.

Definition 2 (Epistemic expectation model). An epistemic expectation model M is a quadruple ⟨S, ∼, V, Exp⟩, where ⟨S,∼, V ⟩ is an epistemic model and Exp : S → Lobs is an expected observation function assigning to each world an observation expression π such that L(π) ̸= ∅ (non-empty set of finite sequences of observations). A pointed epistemic expectation model is a pair (M, s) where M = ⟨S, ∼, V, Exp⟩ is an epistemic expectation model and s ∈ S.

Intuitively, Exp assigns to each world a set of potential or expected observations. We now provide the model definitions of the examples mentioned in the introduction. The traffic light example where only one agent (the traveller) is involved can be depicted by the model Mtl (cf. Figure 2). Unless the traveller (T) observes the respective sequences of traffic signals, she would not know whether she is in France (f) or not (¬f). Her uncertainty is represented by the (bidirectional) link between the two worlds s and t. For the sake of brevity, we do not draw the reflexive arrows. Similar representations are used in the message-passing example as well (cf. Figure 3). Here, the receiver would get to know about the decision depending on the message he receives, whereas, the attacker would be ignorant of the fact irrespective of the message (m or m′ ) she receives.

The main idea for introducing this logic was to reason about agent knowledge via the matching of observations and expectations. In line of public announcement logic [Plaza, 2007], it is assumed that when a certain phenomenon is observed, people delete some impossible scenarios where they

3 For a more detailed explanation of these concepts, see the full arXiv version [Chakraborty et al., 2022].

Figure 3: Mmp (the message passing model).

would not expect that observation to happen. To this end, the update of epistemic expectation models according to some observation w ∈ Σ∗ is defined below. The idea behind an updated expectation model is to delete the worlds where the observation w could not happen.

Definition 3 (Update by observation). Let w be an observation over Σ and let M = ⟨S,∼, V, Exp⟩ be an epistemic expectation model. The updated model M|w = ⟨S′ ,∼′ , V ′ , Exp ′ ⟩ is defined by: S′ = {s ∈ S | L(Exp(s)\w) ̸= ∅}, ∼′i = ∼i|S′×S′ , V ′ = V |S′ , and for all s ∈ S′ , Exp ′ (s) = Exp(s )\w .

In Definition 3, S′ is the set of worlds s in S where the word w can be observed, i.e., L(Exp(s)\w) ̸= ∅. The definitions of ∼′ and V ′ are given by usual restrictions to S′ . The expectation at each world in S′ gets updated by observing the word w: finite strings of actions that are of the form wu are replaced by u while strings that are not of the form wu get removed because they do not match the expectation.

Example 2. Consider the model Mtl of Figure 2 and w = garga. The updated model Mtl|w = ⟨S′ ,∼′ , V ′ , Exp ′ ⟩ is such that S′ = {s}: world t is removed because garga is not a prefix of any word in L((g∗ar∗a)∗ ). The expectation Exp(s) is replaced by Exp ′ (s) = (g ∗ar ∗ )∗ \(garga) = r ∗ (g ∗ar ∗ )∗ .

2.3 Public Observation Logic (POL)

To reason about agent expectations and observations, the language for POL is provided below.

Definition 4 (Syntax). The formulas φ of POL are given by:

Intuitively, Kiφ says that 'agent i knows that φ', and [π]φ says that 'after any observation in π, φ holds'. The other propositional connectives are defined in the usual manner. We also define ⟨π⟩φ as ¬[π]¬φ and ˆKiφ as ¬Ki¬φ. We will mostly use these modalities in our proofs. The Star-Free fragment of POL is the set of formulas in which the π's do not contain any Kleene star ∗. A much more restricted version is the Word fragment of POL, where π's are words. The Existential fragment of POL is the set of formulas for which there is an odd number of negations in front of Ki and [π]

modalities. Equivalently, it corresponds to formulas in negative normal form in which only the operators ⟨π⟩ and ˆKi appear. Finally, we have the Star-Free Existential fragment of POL which is the Existential fragment with the extra guarantee that the π's do not contain any Kleene star ∗.

Definition 5 (Truth definition). Given an epistemic expectation model M = ⟨S, ∼, V, Exp⟩, a world s ∈ S, and a POLformula φ, the truth of φ at s, denoted byM, s ⊨ φ, is defined by induction on φ as follows:

The truth of Kiφ at s follows the standard possible world semantics of epistemic logic. The formula [π]φ holds at s if for every observation w in the set L(π) that matches with the beginning of (i.e., is a prefix of) some expected observation in s, φ holds at s in the updated model M|w. Note that s is a world inM|w because w ∈ prefixes(Exp(s)). Similarly, the truth definition of ⟨π⟩φ can be given as follows:

Intuitively, the formula ⟨π⟩φ holds at s if there is an observation w in L(π) that matches with the beginning of some expected observation in s, and φ holds at s in the updated model M|w. For the examples described earlier, we have:

• Mtl, s |= [g∗ ]¬(KTf ∨ KT¬f). This example corresponds to a safety property: there is no leak of information when observing an arbitrary number of g's because it is compatible with both the expectation g∗ar∗ )∗ of the French traffic light system, and the expectation g∗ar∗a)∗ of the non-French one.
• Mtl, s |= ⟨(garg)∗ ⟩(KTf). This example in the Existential fragment shows that we can express the existence of a sequence of observations that reveals that the traveller is in France.
• Mtl, s |= ⟨gar⟩¬(KTf ∨ KT¬f). This example in the Word fragment expresses that the sequence of observations gar would keep the traveller ignorant about her whereabouts.
• Mmp, s |= ⟨m⟩((KRd ∧ ¬KAd). This example, also in the Word fragment, expresses that after receiving the message m, the receiver gets to know about the decision but the attacker remains ignorant.

Model Checking for POL. Given a finite pointed epistemic expectation model M, s, and a formula φ, does M, s |= φ? We are interested in knowing the complexity of this problem. We will also consider restrictions of the model checking when the input formula φ is restricted to be in one of the syntactic fragments: Word, Star-Free, Existential and Star-FreeExistential.

3 Complexity Results

The main complexity result that we prove is given below. For all the proof details, see [Chakraborty et al., 2022].

Theorem 1. POL model checking is PSPACE-complete.

POL Model Checking Is in PSPACE. For proving the upper bound result, that is, showing that POL model checking is in PSPACE, we design the algorithm mcPOL (Algorithm 1). It takes as input a POL model M = ⟨S, ∼, V, Exp⟩, an initial starting world s ∈ S, and a POL formula φ and returns True iff M, s |= φ. We also prove mcPOL uses polynomial space. The recursive algorithm mcPOL is divided into various cases depending on the structure of φ. The subtle case is the observation modality ⟨π⟩ψ (that is dealt with in lines 7 to 11). It follows from the truth definition that M, s ⊨ ⟨π⟩ψ iff there exists a w ∈ L(π) such that M|w, s ⊨ ψ. We observe that for any M and w the model M|w can be represented by a string of size polynomial in the size of M (This is because M and M|w just differ by their expected observation functions as follows: for any world t, Exp ′ (t) = Exp(t)\w and Exp(t) share the same Non-deterministic Finite Automata (NFA), just the set of initial states is different.). Thus if we consider the set ΓM = {M|w | w ∈ Σ∗ }, the set of every updated model M|w, for a POL model M, over all w ∈ Σ∗ , we realize that all the models in ΓM has size polynomial in the size of M. Thus, by using both the observations together, when mcPOL has to check if M, s ⊨ ⟨π⟩ψ (in the for loop in lines 8 to 10) it goes over all models M′ in ΓM and (in line 8) checks if M′ = M|w for some w ∈ L(π) and finally (in line 10) calls mcPOL recursively to check if M|w, s ⊨ ψ. Thus mcPOL needs to call a polynomial space subroutine to check if M′ = M|w for some word w ∈ L(π). To prove that there exists such a polynomial space algorithm we present a slightly convoluted argument. Algorithm 2 provides a nondeterministic procedure running in polynomial space for deciding that M′ = M|w for some word w ∈ L(π). By Savitch's theorem [Savitch, 1970] which states that NPSPACE = PSPACE, we have that a polynomial space algorithm also exists. Algorithm 2 starts by guessing a word of exponential length, sufficiently long enough to explore all subsets of current states for NFAs of Exp(t) for all worlds t inMand for the NFA of π. Then the algorithm guesses the word w letter by letter and it progresses in the NFAs (note that it does not store the word w as it can be of exponential length). Algorithm 2 accepts when w ∈ L(π) (i.e., ϵ ∈ L(π′ )) and M=M′ . Otherwise, it rejects.

Model Checking for POL Is PSPACE-Hard. Interestingly, there are two sources for the model checking to be PSPACE-hard: Kleene star in observation modalities as well as alternations in modalities (sequences of nested existential and universal modalities). We prove the PSPACE-hardness of model checking against the Existential fragment and the Star-Free fragment of POL respectively.

Theorem2. The model checking for the Existential fragment of POL is PSPACE-hard.

Theorem 3. The model checking for POL is PSPACE-hard, when the POL formulas are Star-Free.

Algorithm 1 mcPOL

Input: M = ⟨S, ∼, V, Exp⟩, s ∈ S , φ Output: True iff M, s ⊨ φ 1: if φ = p is a propositional variable then 2: return True if p ∈ V (s); False otherwise 3: if φ = ¬ψ then 4: return not mcPOL(M, s, ψ) 5: if φ = ψ′ ∨ψ then 6: return mcPOL(M, s, ψ) or mcPOL(M, s, ψ′ ) 7: if φ = ⟨π⟩ψ then 8: for all modelsM′ in ΓM do 9: if s is a world in M′ and the oracle claims that M′ =M|w for some word w ∈ L(π) then 10: return mcPOL(M′ , s, ψ) 11: return False 12: if φ = ˆKiψ then 13: if ∃t ∈ S such that t ∼i s and mcPOL(M, t, ψ) then 14: return True 15: else 16: return False

Algorithm 2 Non-deterministic procedure to decides that

M′ = M|w for some word w ∈ L(π) Input: M = ⟨S, ∼, V, Exp⟩,M′ ∈ Γ M, π Output: has an accepting execution iffM′ =M|w for some w ∈ L(π) 1: π′ := π 2: for i = 1 to 2π ×Πt∈S2|Exp(t)| do 3: if ϵ ∈ L(π′ ) andM=M′ then 4: accept 5: guess a letter a fromΣ 6: π′ := π′ \a 7: for each world t in S do 8: Exp(t) := Exp(t)\a // we modify M locally 9: reject

Model Checking for Star-Free Existential and Word Fragment of POL. While Theorems 2 and 3 proved the PSPACE-hardness of the model checking for the Existential fragment and the Star-Free fragment of POL, respectively, if we consider the Star-Free Existential fragment then we can show that the model checking is NP-complete. Finally, we also prove that the model checking for the Word fragment is in P .

Theorem 4. The model checking problem for the Star-Free Existential fragment of POL is NP-complete.

Theorem 5. Model checking for the Word fragment is in P.

4 Application

Let us consider an automatic farming drone that is moving in a field represented as a grid (see Figure 5). Two agents a and b help the farming drone. The system is adaptive so the global behaviour is not hard-coded but learned. We suppose that the drone moves on a grid and agents a and b may observe one of the four directions: Σ := {▶,◀,▲,▼}. For instance, observing ◀ means that the drone moves one-step left. For this example, we suppose that agent a has learned that there are three possible expectations for the drone:

1. the drone may go up-right searching for water, but the drone can make up to one wrong direction (▼ or ◀). The corresponding set of expectations is captured by the regular expression (▶ ∪▲)∗ (▼∪ ◀ ∪ε)(▶ ∪▲)∗ where ε stands for the empty word regular expression.
2. the drone may go down-left searching for power supply, but the drone can make up to one wrong direction (▲ or ▶). The corresponding set of expectations is captured by the regular expression: (◀ ∪▼)∗ (▲∪ ▶ ∪ε)(◀ ∪▼)∗ .
3. the drone is patrolling making clockwise squares. The expectation is: (▶+ ▼+ ◀+ ▲+)∗ .

The regular expressions may be learned by the agents after observing several executions (see for instance [Balc´azar et al., 1997]) or might be computed by planning techniques [Bonet et al., 2009]. Agent b has more information and knows that the behaviour of the drone would include either searching for water or power supply. Agent a is programmed so that if she knows that the drone is searching for water (Kawater) then she will turn on the valve, and if she knows that the drone is searching for power (Kapower), she will prepare the power supply. Agent b is programmed in the same way. The model M, depicted in Figure 4, can be obtained by techniques described in [van Ditmarsch et al., 2014] (they use a mechanism from DEL for constructing the epistemic expectation model, by assigning the expectations at each world).

The verification tasks related to epistemic planning (e.g., verifying whether Kawater is true after some observations) reduce to the POL model checking problem. Let us now discuss the expressivity of the fragments: Word, Existential, Star-Free - Existential and Star-Free.

In the Word fragment, words are fixed sequences of observations. The fragment thus enables to write formulas of the form ⟨w⟩φ, meaning that φ holds after the sequence w of observations (that can be considered as the observations produced by the plan executed by the system). Thus, this fragment enables to write formulas to verify properties after the execution of a plan.

Example 3 (verification of a plan, Word fragment). Does agent a know that the drone is searching for water after the sequence ▶▶▶?

Epistemic planning is the general problem of verifying whether there exists a plan leading to a state satisfying a given epistemic formula. In our setting, it can be expressed by a formula of the form ⟨π⟩φ where π denotes the plan search space (more precisely the search space of sequences of observations produced by a plan).

Example 4 (epistemic planning, Existential fragment). Does there exist a plan for the drone such that agent b would know that the drone is searching for water while agent a would still consider patrolling a possibility?

In planning (and also in epistemic planning), we may ask for the existence of a plan of bounded length, e.g., less than 4 actions. The Star-FreeExistential fragment is sufficiently expressive to tackle the so-called bounded epistemic planning.

Example 5 (bounded epistemic planning, Star-Free Existential fragment). Does there exist a sequence of at most 4 moves such that agent b would know that the drone is searching for water while agent a would still consider patrolling a possibility?

Interestingly, the Star-Free fragment and the full language are able to express properties, mixing existence and non-existence of plans, in respectively the bounded and unbounded cases.

Example 6 (Star-Free fragment). Agent a would not gain the knowledge that the drone will search for water with less than or equal to 2 movements but it is possible with 3 movements:

Example 7 (full language). It is impossible for the agent a to know that the drone is searching for water with only down and left movements but there is a plan if all movements are allowed:

On Implementation. The model checking for the Word fragment can be implemented in poly-time with a bottomup traversal of the parse tree of the formula, as for CTL [Baier and Katoen, 2008, Section 6.4]. The model checking for the Star-FreeExistential fragment can be implemented via a reduction to SAT. The idea is to introduce propositional variables to model the Boolean values of the following statements: (i) the t-th letter of the guessed word is equal to a, (ii) a given automaton A is in state q after having read the first t letters of the guessed word, and, (iii) a subformula of the formula φ to check is true at a given world u. The last type of statements are combined in the spirit of the Tseitin transformation [Ben-Ari, 2012, p. 91] (for details, see [Chakraborty et al., 2022]and https://github.com/francoisschwarzentruber/polmc).

5 RelatedWork

Dynamic Epistemic Reasoning. The model checking of standard epistemic logic (EL) is PTIME-complete [Schnoebelen, 2002]. Public Observation Logic (POL) is quite similar to Public announcement logic (PAL) [Plaza, 2007]. When public announcements are performed, the number of possible worlds reduces, making the model checking of PAL still in PTIME [van Benthem, 2011] as for standard epistemic logic. When actions can be private, the model checking becomes PSPACE-complete for DEL with action models [Aucher and Schwarzentruber, 2013]. In PAL, a possible world is equipped with a valuation, while in POL it is also equipped with a regular expression denoting the expectation in that world. In PAL, the public announcement is fully specified and its effect is deterministic. In POL, we may reason on sets of possible observations represented by regular expressions π. When these sets are singletons, we again obtain a PTIME upper bound (Theorem 5). In this sense, POL is close to Arbitrary PAL (APAL) [French and van Ditmarsch, 2008] whose model checking is also PSPACEcomplete [ ˚Agotnes et al., 2010]. In APAL, any epistemic formula can be announced: there are no expectations. However, in POL, we have to reason about the constraints between the possible expectations, and the set of observations (given by π). Our contribution can be reformulated as follows: we prove that (i) reasoning about these constraints can still be done in PSPACE, and, (ii) this reasoning is sufficiently involved for the model checking to be PSPACE-hard. In POL, regular expressions are used to represent sets of observations, while van Benthem et al. [van Benthem et al., 2006] used regular expressions (actually, programs of Propositional dynamic logic (PDL) [Fischer and Ladner, 1979]) to denote epistemic relations. Charrier et al. [Charrier et al., 2019] considered a logic for reasoning about protocols where actions are public announcements and not abstract observations as in POL: in this sense, POL is more general.

Epistemic Temporal Reasoning. It is natural to describe computational behaviours with regular expressions. Finitestate controllers, i.e., automata are used to describe policies in planning [Bonet et al., 2009]. Interestingly, Lomuscio and Michaliszyn [Lomuscio and Michaliszyn, 2016] studied an epistemic logic where formulas are evaluated on intervals and the language provides Allen's operators on intervals: in their setting, the model is an interpreted system, and a propositional variable p is true in an interval I if the trace of I matches a given regular expression associated to p. In contrast, POL is not based on an already set-up model but relies on updates in a model. Bozzelli et al. [Bozzelli et al., 2017] studied the complexity of the model checking of that logic depending on the restrictions on the allowed set of Allen's operators. Their framework is similar to ours because it relies on regular expressions but the approach is orthogonal to model updates and hence, to epistemic planning.

Epistemic Planning. Epistemic planning frameworks (based on DEL [Bolander et al., 2020], or the so-called MEP for Multi-agent Epistemic Planning [Muise et al., 2022]) all provide a mechanism for reasoning about preconditions and effects of actions. Expectations about others or about the world are not dealt with. However, Saffidine et al. [Saffidine et al., 2018] propose a collaborative setup for epistemic planning where each agent executes its own knowledgebased policy/program (KBP) while agents commonly know all the KBPs that are being executed, meaning that agents expect that the other agents follow their own KBP. On the contrary, in POL, observations are public but expectations are in general not commonly known. Reasoning about some epistemic properties that are true after the execution of any kind of KBPs is undecidable, but is PSPACE-complete for star-free KBPs. The complexity is high for different reasons: the initial model is represented symbolically; observations are not already public, and KBPs may contain tests.

Strategic Reasoning. Usually in logics for strategic reasoning (e.g., alternating-time temporal logic [Alur et al., 2002] and strategy logic [Chatterjee et al., 2010]), agents do not have expectations: an agent may consider all possible strategies for the others. Recently, Belnardinelli et al. [Belardinelli et al., 2021] propose a variant of strategy logic (SL) where a player may know completely the strategy of another player. In contrast, in POL agents may have partial information about the expectations. In POL, agents also have higherorder knowledge about these expectations. In SL, strategies are abstract objects in the logical language whereas in POL, observations are represented as composite structures that the agents can reason about, similar to the work on games and strategies presented in [Ghosh and Ramanujam, 2012]. In this sense, POL can be seen as EL extended with PDL operators.

6 Conclusion

In this paper, we showed that the model checking for POL is PSPACE-complete. Such complexity studies were left open in [van Ditmarsch et al., 2014]. We also identified more tractable fragments (see Figure 1) of POL. Finally, we discussed the applicability of our study in verifying various features of interactive systems related to epistemic planning. A discussion on implementation is also provided.

We leave the investigations on model checking for EPL, an extension of POL, also proposed in [van Ditmarsch et al., 2014], for future work. We also aim to study the satisfiability problems of POL and EPL by adapting the techniques from [Aucher and Schwarzentruber, 2013; Lutz, 2006].

Many interesting features of such interactive systems remain to be investigated : private observations, like in DEL with action models [van Ditmarsch et al., 2008]; dynamic aspects (e.g., changing expectations); richer languages of expectations (e.g., context-free grammars for expectations), among others. Symbolic model checking can be considered as well following the trends of [van Benthem et al., 2018] and [Charrier et al., 2019].

This paper also opens up a research avenue for developing variants and extensions for reasoning about expectations and observations that can be expressive enough with reasonable complexities for the model checking problem.

To sum up, POL mixes epistemic logic and language theory for modelling mechanisms of social intelligent agents, and the current investigations on model checking set it up as a useful tool in building social software for AI.