Bounded Epistemic Situation Calculus Theories

Introduction

The Situation Calculus [McCarthy and Hayes, 1969; Reiter, 2001] is a widely used and expressive first-order logical framework for reasoning about action in which many issues have been addressed, e.g., the frame problem, time, continuous change, complex actions and processes, uncertainty, etc. In [De Giacomo et al., 2012], it was shown that for an important class of so called bounded action theories in the situation calculus, verification of a very expressive class of first-order µ-calculus temporal properties is decidable. Bounded action theories are basic action theories [Reiter, 2001], where it is entailed that in all situations, the number of fluent atoms that are true is bounded by a constant. In such theories, the object domain remains nonetheless infinite, as is the domain of situations. Boundedness may seem like a restrictive condition, but it can be argued that in real domains facts rarely persist indefinitely as everything decays and changes. Moreover, agents often forget facts either because they are not used or because they cannot be confirmed by sensing. [De Giacomo et al., 2012] give many examples of domains that can be modeled as bounded action thories. They also identify various ways in which one can obtain bounded action thories: (1) by strenghtening preconditions to block actions where the bound would be exceeded, (2) by ensuring that actions are effect bounded and never make more fluents true than they make false, and (3) by using fading fluents whose strength fades over time unless they are reconfirmed.

In this paper, we devise analogous results in the epistemic situation calculus [Scherl and Levesque, 2003], where one Fabio Patrizi DIAG Sapienza Universit`a di Roma Roma, Italy

patrizi@dis.uniroma1.it

can refer in the language to what the agent knows and does not know after performing some actions, as well as what is true, and also deal with sensing/knowledge producing actions. It is natural to look at boundedness in this setting, as the intuition for bounded action theories is partly epistemic. We define a notion of e-bounded theories where it is entailed that in all situations, the number of fluent atoms that the agent thinks may be true is bounded by a constant. The object domain remains nonetheless infinite, as is the domain of situations. There may be an infinite set of different fluent atoms that the agent thinks may be true over the course of an infinite run, even though in any given situation, the set of fluent atoms that the agent thinks may be true is bounded. We discuss how one can obtain e-bounded theories in practice. Our main result is that for e-bounded theories, verification of a very expressive class of first-order µ-calculus temporal epistemic properties is decidable. We also show that e-boundedness of an epistemic action theory can be related to the boundedness of the action theory that the agent uses to model change in the world. We prove that if the agent's knowledge in the initial situation is e-bounded and the objective part of an action theory maintains boundedness (i.e., if the number of fluent atoms that are true initially is bounded it remains bounded in later situations), then the entire epistemic theory is e-bounded.

Our notion of e-bounded theory is based on bounding the number of fluent atoms that the agent considers possible in a situation. This yields a very simple and general notion of epistemic boundedness. It is defined relative to the standard possible worlds semantics for incomplete knowledge, which refers to the possibilities that the agent considers plausible. This accomodates very general forms of partial knowledge, e.g., disjunctive knowledge, existential knowledge, etc. We briefly discuss alternative approaches at the end of the paper. While our study is set in the situation calculus, the insights and results we obtained could be applied to other settings where there is an interplay between knowledge and action.

Epistemic Situation Calculus

The situation calculus [McCarthy and Hayes, 1969; Reiter, 2001] is a sorted predicate logic language for representing and reasoning about dynamically changing worlds. All changes to the world are the result of actions, which are terms in the language. We denote action variables by lower case letters a and action types by capital letters A. A possible world history is represented by a term called a situation. The constant S0 is used to denote the actual initial situation where no actions have yet been performed. Sequences of actions are built using the function symbol do, where do(a, s) denotes the successor situation resulting from performing action a in situation s. Besides actions and situations, there is also the sort of objects for all other entities. Predicates whose value varies from situation to situation are called fluents, and are denoted by symbols taking a situation term as their last argument (e.g., Holding(x, s)). We denote fluents by F and the finite set of primitive fluents by F. The arguments of fluents (apart from the last which is of sort situation) are assumed to be of sort object. For simplicity, and w.l.o.g., we assume that there are no functions and no non-fluent predicates.

In this setting [Reiter, 2001], one can write successor state axioms that succinctly characterize how the world changes. These imply both effect axioms and frame axioms and provide a solution to the frame problem. A special predicate Poss(a, s) is used to state that action a is executable in situation s, and one can write preconditions axioms to characterize this predicate. The abbreviation Executable(s) means that every action performed in reaching situation s was possible in the situation in which it occured.

To capture how the agent's knowledge changes when she performs sensing, (as well as introspection), we need to model knowledge explicitly in the language. A popular approach for this is to add a possible world account of knowledge to the situation calculus as proposed in [Moore, 1985; Scherl and Levesque, 2003]. This can be done by introducing a special fluent K(s′ , s) read as situation s′ is epistemically accessible fron situation s, i.e., the agent thinks that s′ is a possible way the world may be in situation s. Then we can introduce the following definition:

i.e., the agent knows that φ in situation s iff φ holds in all stituations s′ the agent considers possible in s. Here φ is a situation suppressed (i.e., with the situation argument in fluents suppressed) epistemic situation calculus formula uniform in its (suppressed) situation argument, where Knows may occur. We recall that in essence, a situation calculus formula is uniform if it refers only to a single situation [Reiter, 2001]. We denote by φ[s] the corresponding formula with the situation argument reintroduced and assigned to situation s. To specify the information provided by boolean/binary sensing actions, [Levesque, 1996] introduces a special fluent SF(a, s), which holds if action a returns the binary sensing result 1 in situation s. Using this we can write sensed fluent axioms like

i.e., the action senseOpen(door) returns the result 1 in situation s iff door is open in s. (For the non-binary sensing action case, see [Scherl and Levesque, 2003].) One can then specify how the agent's knowledge changes using the following successor state axiom for the K fluent [Scherl and Levesque, 1993; 2003]:

i.e., situation s′′ is accessible after action a is performed in s iff it is the result of performing a in a situation that was accessible in s and where a was executable and the sensing result agrees with that produced in s.

The above assumes that actions are fully observable (every s′ such that K(s′ , s) involves the same action history as s). [Bacchus et al., 1999] generalizes the framework to accomodate partial observability of actions, noisy sensing, and non-deterministic actions. Instead of sensed fluent axioms, they use observation-indistinguishability axioms of the form:

one for each action type A, where φA(A(⃗x), a′ , s) characterizes the conditions under which actions A(⃗x) and a′ are indistinguishable in situation s. E.g., we could use

to specify that the agent cannot tell whether he succeeds or fails when he attempts to pick up block x. With this, they use the folllowing successor state axiom for the K fluent:

i.e., situation s′′ is accessible after action a is performed in s iff it is the result of performing an action a′ that is observation-indistinguishable in s from a in a situation s′ that was K-accessible in s where a′ is executable. 1 Precondition axioms are then used to relate the result of a possibly noisy sensing action, which must be one of its parameters, to the sensed condition in the actual situation, e.g.

Given this language, one can formulate epistemic basic action theories [Levesque et al., 1998; Reiter, 2001] that describe how the world state and what the agent knows changes as the result of the available actions. Here, we assume that there is a finite number of action types. Moreover, we assume that the terms of object sort are in fact a countably infinite set N of standard names for which we have the unique name assumption and domain closure [Levesque and Lakemeyer, 2001]. We also assume that the accessibility relation K is initially reflexive, transitive and euclidean, and the successor state axiom for K preserves this for all situations. We assume that precondition axioms do not mention K. We also assume that the condition on the right hand side of observationindistinguishability axioms is a domain-independent formula. Domain independent formulas are those for which the evaluation depends only on the active domain: essentially negation is only used to express difference of extensions and not complement. An example of domain-independent formula is ∃x.V ehicle(x) ∧ ¬Car(x), and a domain-dependent variant is ∃x.¬Car(x). These are standard in the Database literature, see [Abiteboul et al., 1995]. We make use of domain independence in the observation-indistinguishability axioms to ensure that no new objects are introduced other than action parameters. 2

1 In [Bacchus et al., 1999] this need only hold if action a is executable in s; we drop this restriction for simplicity.

Bounded Epistemic Action Theories

Let b be some natural number. We can use the notation |{⃗x | φ(⃗x)}| ≥ b to stand for the FO formula:

We can also define (|{⃗x | φ(⃗x)}| < b) .= ¬(|{⃗x | φ(⃗x)}| ≥ b). Using this, [De Giacomo et al., 2012] define the notion of a fluent F(⃗x, s) in situation s being bounded by a natural number b as BoundedF,b(s) .= |{⃗x | F(⃗x, s)}| < b and the notion of situation s being bounded by b:

An action theory D is bounded by b if

[De Giacomo et al., 2012] show that that for bounded action theories, verification of sophisticated temporal properties is decidable. It also identifies interesting classes of bounded action theories.

Here we devise analogous notions of boundedness for epistemic action theories. We define the notion of a fluent F (⃗x, s) in situation s being e-bounded by a natural number b as:

Observe that:

Thus fluent F(⃗x, s) is e-bounded by b in situation s if the number of distinct ⃗x such that the agent considers it possible that ⃗x is in F in s is bounded by b. We define the notion of situation s being e-bounded by a natural number b as follows:

We say that an epistemic action theory D is ebounded by b if

We shall see that for e-bounded epistemic action theories, verification of sophisticated properties is decidable.

Example 1 (Wumpus Hunter) Consider a version of the well known Wumpus World [Russell and Norvig, 2010] where there is an agent H whose only task is to hunt wumpus monsters that live in various dungeons (we assume that there are no pits to avoid or gold to pick up, but many dungeons and wumpuses). Each dungeon is laid out as an 8 × 8 grid. Initially, H is in dungeon D1 at location 〈0, 0〉 facing Right. The agent and wumpus are both alive, and 〈0, 0〉 is the only location the agent has visited. The agent knows all of this, which is specified by the following initial state axioms:

2 Note that domain independence is also used in the decidability proof, but the assumption is later dropped exploiting well-known results [Libkin, 2007].

Knows (DungeonH(d) ≡ d = D1, S0) Knows (LocH(l) ≡ l = 〈0, 0〉, S0) Knows (DirH(d) ≡ d = Right, S0) Knows (AliveW, S0) Knows (AliveH, S0) Knows (V isited(l) ≡ l = 〈0, 0〉, S0)

H knows that the wumpus is at some unique location other than 〈0, 0〉, but does not know which; in fact he is at 〈1, 1〉:

Now let's specify the world dynamics. The agent can move around by going forward one square in the direction he is facing, provided he has not reached the grid edge, and by turning 90 degrees clockwise (always possible). The following successor state axioms and precondition axioms specify this:

LocH(l, do(a, s)) ≡ a = moveFwd ∧ ∃d∃l′ (DirH(d, s) ∧ LocH(l′ , s) ∧ Adjacent(l′ , d, l)) ∨ LocH(l, s) ∧ a ̸= moveFwd DirH(d, do(a, s)) ≡ a = turn ∧ (DirH(Up, s) ∧ d = Right ∨ . . .) ∨ DirH(d, s) ∧ a ̸= turn P oss(moveFwd, s) ≡ ∃l∃d∃l′ (LocH(l, s) ∧ DirH(d, s) ∧ Adjacent(l, d, l′ ))

The location of the wumpus never changes except when the agent arrives in a new dungeon; in this case, the wumpus's location is determined by the partially observable exogenous action arriveInDungeon(d, l) (discussed later):

The wumpus is alive when H arrives in a dungeon and remains so until H shoots an arrow forward towards him (always possible):

Similarly we have an axiom stating that H remains alive unless he moves to a location where there is a live wumpus. V isited records the locations the agent has visited so far; it is reset to {〈0, 0〉} when the agent arrives in a new dungeon:

V isited(l, do(a, s)) ≡ ∃d∃l′ a = arriveInDungeon(d, l′ ) ∧ l = 〈0, 0〉 ∨ a = moveFwd ∧ ∃d∃l′ (DirH(d, s) ∧ LocH(l′ , s) ∧ Adjacent(l′ , d, l)) ∨ V isited(l, s) ∧ ¬(∃d∃l′ a = arriveInDungeon(d, l′ ) ∨ a = moveFwd)

H remains in the current dungeon until he exits it, after which he is outside, and then the exogenous action arriveInDungeon(d, l) may occur, after which he is in dungeon d:

DungeonH(d, do(a, s)) ≡ ∃la = arriveInDungeon(d, l) ∨ a = exitCurDungeon ∧ d = Outside ∨ DungeonH(d, s) ∧ ¬(∃l a = arriveInDungeon(d, l) ∨ a = exitCurDungeon)

H may exit the current dungeon if he is at 〈0, 0〉. arriveInDungeon(d, l) may occur if the agent is outside any dungeon, where l is the location where the wumpus will hide; it must be a valid location different from 〈0, 0〉:

P oss(exitCurDungeon, s) ≡ LocH(〈0, 0〉) Poss(arriveInDungeon(d, l), s) ≡ DungeonH(Outside, s) ∧ V alidLoc(l) ∧ l ̸= 〈0, 0〉

The action arriveInDungeon(d, l) is only partially observable; the agent knows that he has arrived in dungeon d, but does not know the location l where the wumpus is; i.e., arriveInDungeon(d, l) is observation indistinguishable from arriveInDungeon(d, l′ ). All other actions are fully observable:

Oi(arriveInDungeon(d, l), a, s) ≡ ∃l′ a = arriveInDungeon(d, l′ ) Oi(A(⃗x), a′ , s) ≡ a′ = A(⃗x)) for all A ̸= arriveInDungeon

Finally, the agent can get information about the wumpus's location by performing the sensing action smell(r); if the wumpus is located in an adjacent location, the agent will get a sensing result r of 1, otherwise the result will be 0:

P oss(smell(r), s) ≡ ∃l∃d∃l′ (LocW(l, s) ∧ LocH(l′ , s) ∧ Adjacent(l, d, l′ )) ∧ r = 1 ∨ ∃l∃l′ (LocW(l, s) ∧ LocH(l′ , s) ∧ ∀d¬Adjacent(l, d, l′ )) ∧ r = 0

It is easy to show (by induction on executable situations) that this theory is e-bounded by the gridsize g. In S0, locW is e-bounded by g, as the agent thinks that the wumpus may be in any location other than 〈0, 0〉. All the other fluents are e-bounded by 1. Thus EBoundedg(S0). Suppose that EBoundedg(s) for some executable s. Then it is easy to check that EBoundedg(do(a, s)) for any a such that Poss(a, s). All fluents other than V isited and locW remain bounded by 1. V isited is always known and may only become true for grid locations. The set of l that the agent thinks may be locW remains the same if a is neither smell(r) nor arriveInDungeon(d, l). If it is the former, the set shrinks or remains the same. If it is the latter, it is reset to all grid locations other than 〈0, 0〉. Thus do(a, s) is e-bounded by g.

While the theory is e-bounded, it should be noted that the number of different dungeons d that the agent may visit and for which Knows (dungeonH(d)) may come to hold over a path is unbounded. This is not a propositional theory. Also, the agent initially has incomplete knowledge about the location of the wumpus, but can acquire more information about it. As well, note that the agent forgets everything that he knew about the previously visited dungeons when he arrives in a new one. The theory was specified using fluents that implicitly refer to the current dungeon and partially observable actions to achieve this. It would not be hard to make the dungeons that the agent arrives into have a dynamic graph-like layout with a bounded number of named locations. The dungeon structure could be defined using exogenous actions like addLoc(l) and addConnection(l, l′ ). Then the set of locations that the agent comes to know about over a path would no longer be bounded, although we could still ensure that it is e-bounded in any situation as the number of locations in a dungeon remains bounded and the agent only thinks about the current dungeon.

Relating Boundedness and E-Boundedness

One question that naturally arises is what are interesting sufficient conditions to guarantee e-boundedness. Here we formulate one, a key result relating the boundedness of action theories that model change in the world with the e-boundedness of the entire epistemic theory. Specifially, we show that if an epistemic theory has e-bounded knowledge in the initial situation, and its objective part 3 which describes how the world changes, maintains boundedness [De Giacomo et al., 2012], then the entire theory is e-bounded. We say that an objective theory Dobj, with initial situation description D0, maintains boundedness, if for every bounded initial situation description D′0 we have that (Dobj -D0) ∪D′0 is bounded. Thus:

Theorem 1 Let D be an epistemic action theory with objective part Dobj and initial epistemic situation description DK0. If Dobj maintains boundedness and DK0 is e-bounded, then D is e-bounded.

Proof (sketch). This holds because if the initial epistemic situation description is e-bounded it can be represented with a bounded number of isomorphic types (cf. Verification Section). From each of these types the successor situations remain bounded, as sensing actions can only reduce the number of epistemic alternatives, and if there are observationally indistinguishable actions, while they may increase the number of epistemic alternatives, given the domain independence condition, they do not introduce new elements into the active domain, but only reshuffle the ones already present, hence do not change the set of isomorphic types. So the entire theory is e-bounded.

Notice that the actual e-bound for the whole theory can be computed from the e-bound of DK0 and the bound maintained by the objective part Dobj. This result, together with the various conditions for boundedness in [De Giacomo et al., 2012], provides effective means for designing e-bounded epistemic theories. For example, if the initial epistemic situation description is e-bounded, and we assume bounded effects or fading fluents (both of which maintain boundedness), then the resulting theory is e-bounded.

3 The objective part of epistemic theory is formed by all axioms that do not mention the K, SF and Oi fluents.

Example 2 (Wumpus Hunter Cont.) We can use Theorem 1 to show that our example theory is e-bounded. As discussed earlier, the initial epistemic situation description is e-bounded by the grid size g. It is easy to see that the objective part maintains boundedness as all fluents are bounded by 1 except for V isited which is bounded by g.

Expressing Dynamic Properties

To express properties about epistemic action theories, we use a FO variant of the µ-calculus [Emerson, 1996; Stirling, 2001], one of the most powerful temporal logics, subsuming both linear time logics, such as LTL and PSL, and branching time logics such as CTL and CTL* [Baier et al., 2008]. We introduce the logic µLK, whose syntax is as follows:

where p is an atomic situation-suppressed situation calculus FO formula, ϕ an arbitrary epistemic formula (we allow for quantifying in), ϕc an arbitrary closed epistemic formula, Z a SO (0-ary) predicate variable, and where in 〈-〉Φ, Φ must be closed with respect to individual variables. Thus we do not allow quantification across dynamic operators.

We use the usual abbreviations for booleans, [-]Φ for ¬〈-〉¬Φ, and νZ.Φ = ¬µZ.¬Φ[Z/¬Z]. As usual in the µcalculus, formulae of the form µZ.Φ (and νZ.Φ) must satisfy syntactic monotonicity of Φ wrt Z, which states that every occurrence of the variable Z in Φ must be within the scope of an even number of negation symbols.

The fixpoint formulas µZ.Φ and νZ.Φ denote respectively the least and the greatest fixpoint of the formula Φ seen as a predicate transformer λZ.Φ (their existence is guaranteed by the syntactic monotonicity of Φ). Using these operators we can define sophisticated inductive and coinductive temporal/dynamic properties. For instance, we can use the least fixpoint formula µZ.ϕ ∨ 〈-〉Z to say that it is possible to achieve Φ, written in CTL notation as E♦Φ. Similarly, we can use the greatest fixpoint formula νZ.ϕ∧ [-]Z to say that Φ always holds, written in CTL notation as A□Φ.

To define semantics, since µLK contains formulae with free predicate variables, given a model M of an action theory D with domain ∆ for sort object and domain S for sort situation, we need to introduce an object variable valuation v, and a predicate variable valuation V, i.e., a mapping from predicate variables Z to subsets of S. Then we assign semantics to formulae by associating toM, v and V two extension functions (·)Mv and (·)MV , which together map µLK formulae to subsets of S as inductively defined as follows:

Notice that the extension function (·)Mv is a standard epistemic FO interpretation function, while (·)MV deals with the temporal part. (·)MV assumes that epistemic FO formulas that constitute the atoms of the temporal formulas are closed, so it does not need to refer to the object variable valuation v. The only formulas of interest in verification are those that are closed (wrt predicate variables), and for them (·)MV does not depend on the predicate valuation V. Thus, when Φ is closed, we simply write (Φ)M. We say that a theory D verifies a µLK closed formula Φ, written D |= Φ, if S0 ∈ (Φ)M, for every model M of D.

Example 3 (Wumpus Hunter Cont.) If the wumpus (in the current dungeon) is alive then it is possible for the hunter to eventually know that he has killed him: A□(AliveW ⊃ E♦Knows (¬AliveW)). It is also the case that the hunter knows that if the wumpus is alive then it is possible for him to eventually be killed by the wumpus: A□Knows (AliveW ⊃ E♦¬AliveH). We can also show that the agent is aware of some of his memory limitations, e.g., even if the agent knows where the wumpus is, he may forget this if he moves to a different dungeon: A□(∃l Knows (locW(l))∧locH = 〈0, 0〉 ⊃ 〈-〉〈-〉¬∃l Knows (locW(l))).

Our µLK language does not allow for quantification across situations. However the richness of the situation calculus mitigates this limitation. For instance we can introduce a finite number of "registers", i.e., fluents that store only one tuple, and then use them to store and refer to tuples across situations; see [De Giacomo et al., 2012] for details. However, it remains of interest to generalize our framework to allow some forms of quantification across situations. Some encouraging results along these lines appear in [Hariri et al., 2012a; Belardinelli et al., 2012; Hariri et al., 2012b].

Verification

We now show that verifying µLK temporal properties against bounded epistemic action theories is decidable. We first focus on epistemic action theories with a complete specification of S0, i.e., s.t. D0 contains an axiom F (⃗x, S0) ≡ φF0 (⃗x) for each fluent F ∈ F and an axiom K(s, S0) ≡ φK0 (s) specifying the initial uncertainty, as well as axioms specifying that K is an equivalence relation in S0. At the end, we generalize our results to the incomplete specification case. Our first result is:

Theorem 2 If D is an e-bounded epistemic action theory with complete specification of S0, and Φ a closed µLK formula, then verifying if D |= Φ is decidable.

To explain this result, notice first that, as a consequence of complete knowledge, D has a unique model M with object sort ∆ = N. Thus, we only need to check whether S0 ∈ (Φ)M. Let LK denote the set of uniform (in the situation argument) epistemic FO formulas of the situation calculus, and observe that the evaluation of any φ(⃗x, s) ∈ LK does not depend on the situation s, but only on the corresponding epistemic state (e-state), i.e., the pair 〈Is,Bs〉 s.t. Is = 〈∆, ·Is 〉 is the interpretation of F associated with s, and Bs = {Is′ |K(s′ , s)} (observe that Is ∈ Bs). It can be shown that for any two situations s1, s2 ∈ S, Is1 = Is2 and Bs1 = Bs2 iff it is the case that for every φ(⃗x, s) ∈ LK and every variable valuation v over N, M, v |= φ(⃗x, s1) iff M, v |= φ(⃗x, s2). This applies in particular to successor state axioms, yielding that, for any action a, if 〈Is1 ,Bs1 〉 = 〈Is2 , Bs2 〉, then 〈Is′1 , Bs′1 〉 = 〈Is′2 , Bs′2 〉, with s′1 = do(a, s1) and s′2 = do(a, s2).

Observe that the e-states 〈I, B〉 of M induce a partition of S s.t. two situations s, s′ are in the same cell iff Is = Is′ and Bs = Bs′ . By the above results, for any executable action a, we can generate the e-state 〈I ′ ,B′ 〉 of the successor situation of each situation in a cell H, by operating on 〈I,B〉. To do so, we evaluate on I the situation-suppressed successor state axioms instantiated on action A(⃗ d) with ⃗ d taken from ∆, obtaining I ′ (evaluating preconditions in the same way), and do the same for all action types A′ (⃗ d′ ) observationallyindistinguishable from A(⃗ d) (these are FO-defined) on each Ib ∈ B, joining all the resulting states into B′ . By considering all cells and actions, this defines a transition system (TS) T = 〈∆,Q, q0,→〉, s.t.: the object domain is ∆ = N; Q is the set of states, corresponding to e-states; q0 = 〈IS0 , BS0 〉 is the initial state; each transition 〈I,B〉 → 〈I ′ ,B′ 〉 is obtained by executing an action on 〈I,B〉, as above. T retains all the information necessary to evaluate Φ on M. To show this, we transfer the semantics of µLK to TSs, using an inductive definition matching that of (·)MV with:

Once (Φ)TV is evaluated, it can be interpreted as a set of situations. The following result, consequence of the fact that µLK formulas are built fromLK formulas, explains this, and states the equivalence of theM- and T-based semantics.

Lemma 1 If T is as above, then for any µLK formula Φ and valuation V, (Φ)MV = {s ∈ S | 〈Is,Bs〉 ∈ (Φ)TV }.

Thus, to check whether S0 ∈ (Φ)MV , instead of using M, we can use T, and check whether 〈I0,B0〉 ∈ (Φ)TV . Notice however that, being infinite, T can neither be inspected nor even constructed. We next solve both problems.

Let adom(I) denote the active domain of I, i.e., the set of all objects occurring in some fluent extension F I , and let adom(B) = ⋃Ib∈B adom(Ib). We denote by C ⊂ N the finite set of all constants, i.e, standard names, appearing in D. Two e-interpretations 〈I1,B1〉 ∈ I ∆1 F and 〈I2,B2〉 ∈ I ∆2 F are KA-isomorphic, written 〈I1, B1〉 ∼ 〈I2, B2〉, if C ⊆ ∆1, C ⊆ ∆2, and there exists a bijection h : adom(B1) ∪ C → adom(B2) ∪C that is the identity on C, and s.t.: h(I1) = I2 and B2 = {h(Ib1) | Ib1 ∈ B1}, for h(I) the interpretation obtained from I by renaming all of its objects o as h(o). Intuitively, KA-isomorphic e-interpretations have matching relational structures. Next, we define a constructive procedure that, under e-boundedness, produces a finite-state TS ˆ T KAbisimilar to T. The notion of KA-bisimilarity matches standard bisimilarity, except that the local condition in its definition requires two states to be KA-isomorphic. The following transfers a fundamental theorem for the µ-calculus to µLK:

Lemma 2 Given two KA-bisimilar TSs T and T ′ , and a µLK formula Φ, q0 ∈ (Φ)T iff q′0 ∈ (Φ′ )T ′ where Φ′ is a domain independent formula equivalent to Φ.

The transformation of Φ into Φ′ is required as Φ could be domain-dependent, and T, T ′ may have distinct interpretation domains. Through syntactic manipulations, Φ can be turned into a logically equivalent domain-independent formula Φ′ , see [Libkin, 2007]. To construct ˆ T we proceed exactly as done for T, except that we take values from a finite doman ˆ∆ ⊂ N (instead of ∆) s.t. C ⊆ ˆ∆ and | ˆ∆| = |C| + be + Nvars, where be is the bound (derived from the e-bound e) on the maximum number of distinct objects occurring in some e-state, and Nvars is the maximum among the number of distinct variables (assuming all quantified variables are renamed apart) occurring in some successor-state, observation-indistinguishability axioms, or the initial epistemic situation description D0. Such numbers are motivated by the fact that, to enforce KA-bisimilarity, a minimal requirement is that every state of T have a matching KA-isomorphic state in ˆ T, thus be. Further, since ˆ T is obtained by executing actions on its states, a sufficient number of additional elements, Nvars is needed, to abstract all the possible combinations of the objects used in some action, and mentioned in the axioms.

Lemma 3 T and ˆ T are KA-bisimilar.

Thus, by Lemma 2, by checking whether ˆ q0 ∈ (Φ′ ) ˆ T , we can check whether q0 ∈ (Φ)T . Since this can effectively be done by applying standard algorithms for model checking of the µ-calculus, suitably extended to evaluate the LK sentences occurring in Φ′ , we obtain an actual procedure for the verification of e-bounded epistemic theories against µLK. This completes the proof of Theorem 2.

Finally, we consider the general case where we may have an incomplete specification of S0.

Theorem 3 If D is an e-bounded epistemic action theory (with possibly an incomplete specification of S0) and Φ a closed µLK formula, then verifying if D |= Φ is decidable.

This follows from the fact that, for fixed ˆ∆, any two TSs ˆ T and ˆ T ′ as above, s.t. q0 ∼ q′0 , are KA-bisimilar, and that KA-isomorphic e-states satisfy exactly the same LK formulas. Thus, by Lemma 2 and the above construction, to check all the models whose initial state satisfies D0, it is sufficient to construct and check one ˆ T per class of isomorphic e-states satisfying D0. Since by e-boundedness such classes are finite, this can be done by checking a finite number of TSs.

Conclusion

We have defined the class of e-bounded theories in the epistemic situation calculus and shown that for them verification of a very expressive class of first-order µ-calculus temporal epistemic properties is decidable. The proof is constructive and gives us an effective procedure for verification. A related result in the context of interpreted systems appeared in [Belardinelli et al., 2012]. The main difference, apart from the setting and the verification logic (they use a first-order variant of CTL), is that our epistemic framework supports incomplete theories, while theirs is tailored towards single models.

Note that if we do not have a fixed bound for all situations, then one can represent Turing machine configurations (including the tape, which is at any moment finite) in situations, and use basic action theories to encode transitions between configurations. Thus the mu-calculus formula µZ.Halt ∨ 〈-〉Z, where Halt is just a propositional fluent representing the fact that the machine reached an acceptance state, is undecidable. The number of objects in each model remains infinite. But in each (epistemic) situation when new objects are inserted in the active domain, old objects must be removed so as to maintain the bound. In each infinite branch of the situation tree the number of objects mentioned may still be infinite. A sophisticated abstraction is needed to reduce this infinite set into a finite one. Of course a situation can mention fewer objects than the bound.

In e-bounded theories, the number of fluent atoms that the agent thinks may be true is bounded. But note that there may be an infinite number of x such that ¬Knows (F(x)) ∨ Knows (¬F(x)). Properties F for which there is an infinite number of x for which it is unknown whether or not F(x) holds cannot be represented and must be left out of the language. Alternative approaches that bound what is known by the agent as opposed to what is considered possible should also be investigated. But this would appear to require strong assumptions about what forms of knowledge are being considered. We could bound the number of fluent atoms that are known to be true or known to be false. Or we could bound the number of prime implicates that are known to be true or false. But not all of first order epistemic logic can be expressed in such forms, so the resulting account would be restricted in the kinds of knowledge specifications it handles. We leave exploring such alternative notions for future work. Another interesting avenue for future work is to introduce Golog and ConGolog programs to specify processes over e-bounded theories, and extend our verification techniques to this setting.

Acknowledgements

Authors acknowledge support of EU Projects FP7-ICT 257593 (ACSI) and FP7-ICT 318338 (OPTIQUE).