On the Undecidability of the Situation Calculus Extended with Description Logic Ontologies

1 Introduction

Combining action formalisms, which describe how systems evolve over time as consequences of actions, and ontological formalisms, which capture knowledge about the domain structure that is invariant over time, is a strong desiderata in AI and CS. Initiatives like OWL-S have been putting forward explicitly this need [Martin and others, 2004]. More recently, the work on data aware processes has come back to this issue by giving a formal account of processes that manipulate unbounded data and devising techniques for their verification [Belardinelli et al., 2012; De Giacomo et al., 2012; Bagheri Hariri et al., 2013a; 2013b].

In this paper we study combining the situation calculus [Reiter, 1991; 2001], possibly the best known first-order based formalism for reasoning about actions, with description logics [Brachman and Levesque, 1984; Baader et al., 2003], which are currently considered the main formalisms for expressing ontologies. In particular we extend situation calculus action theories with description logics TBoxes, acting as a sophisticated form of state constraints [Lin and Reiter, 1994]. From the technical point of view, we consider the simplest and most natural combination, namely the union of the two sets of axioms. In this way, we have the two ingredients combined into a single logical theory, and we have a single logical language to talk about both static and dynamic aspects of the system.

In fact, this combination is related to combining description logics and temporal logics, which is a well studied subject. Even though recently some decidability results for simple description logics have been obtained [Artale et al., 2013], it is well known that this combination is problematic in general. Indeed, it gives rise to a notorious two-

Mikhail Soutchanski

Ryerson University Toronto, Canada mes@cs.ryerson.ca

dimensional semantics (where one dimension is for time and the other for the description logic domain), which suffers from a key computational problem: the possibility of specifying that roles, i.e., binary predicates, preserve their extension over time causes undecidability, due to the possibility of easily encoding bidimensional grids, and hence tilings or Turing machine computations [Wolter and Zakharyaschev, 1999; Gabbay et al., 2003]. Notice that if we drop the capability of preserving the extension of binary predicates over time, the usefulness of such a combination becomes disputable: for example we would not be able to represent that a person remains subscribed to some mailing list until s/he unsubscribes.

In light of these results we may already suspect that the combination of the situation calculus and description logics in a single logical theory is going to lead to undecidability of reasoning in general. The aim of this paper is to investigate how deep this problem really is. To do so, we consider a simplified setting in which we partition fluents into two kinds. The first kind includes fluents that constitute what we may call the "frame", for which effect axioms are directly specified and inertia is assumed (frame problem solved). The second kind includes fluents for which no direct effects are specified and inertia is not assumed. Hence these fluents evolve over time only due to ramifications through the state constraints of the effects on the fluents in the frame, and inertia is not assumed. State constraints predicate on the relationship between fluents of both kinds in a single state. Specifically, our simplified setting is as follows: (i) we use only unary and binary fluents (i.e., fluents with one or two object arguments, apart from the situation one); (ii) we characterize the frame through a situation calculus basic action theory [Reiter, 1991; 2001]; in particular, we use regular successor state axioms to specify how actions affects fluents in the frame (including the solution to the frame problem). (iii) as state constraints, we use a TBox expressed in a given description logic, i.e., a finite set of universal inclusion assertions that must hold in every situation; (iv) the initial situation description consists of a finite set of positive facts involving fluents.

Here we show that in the above setting the simplest form of reasoning, namely satisfiability, the minimal requirement for any logical theory, is undecidable, even when the state constraints are expressed in the simplest description logics, such as DL-Litecore, and the situation calculus action theory is of the simplest form, namely context free in the sense of [Reiter,

1991] and local effect [Vassos et al., 2008]. This contrasts, on the one hand, with the fact that, without state constraints, since the initial situation description consists only of a finite set of positive facts, satisfiability trivially holds [Reiter, 2001]; and, on the other hand, with the fact that, if one considers the initial situation description as an ABox, the decidability of satisfiability of such ABox with any TBox is guaranteed in all description logics [Baader et al., 2003]. Naturally, undecidability of satisfiability implies that all other typical tasks in reasoning about action, such as projection, executability of actions, verification, etc. are also undecidable.

Interestingly, sometimes state constraints can be compiled into the basic action theory itself [Lin and Reiter, 1994; Lin, 1995; Lin and Soutchanski, 2011]. In light of the good computational properties of description logics, one might hope that the compilation approach could be applied also in our setting to get computational effectiveness. But the very result of undecidability of satisfiability implies that this is not the case. Indeed, the basic action theory resulting from the compilation, besides the standard (though possibly complex) successor state axioms, would also contain a new initial situation description. Satisfiability would depend only on the latter, so by our undecidability result such initial situation description could not consist of a description logic knowledge base, since these are always decidable.

The negative results we obtained, even under extreme simplifying restrictions, indicate the need of alternative forms of combinations, strengthening some of the proposals in literature, which, although may look more ad-hoc, guarantee decidability or better computational behavior. We come back to this point in the conclusion.

The rest of the paper is organized as follows. After some preliminaries (Sec. 2), we show by a simple reduction from tiling, that satisfiability of basic action theories extended with ALC TBoxes is undecidable (Sec. 3). Then we strenghten the result to the simplest description logic of the AL family (Sec. 4). Finally, by resorting directly to a reduction from the halting problem of Turing machines, we show undecidability also for the simplest logics in the lightweight description logics families DL-Lite, and EL, even if the action theory is local effects and context free (Sec. 5). A short discussion concludes the paper (Sec. 6).

2 Preliminaries

Situation Calculus. The situation calculus [Reiter, 1991; 2001] is a multi-sorted predicate logic language for axiomatizing dynamic systems with sort actions, sort situations and sort objects. Actions αi(⃗x) are first-order (FO) terms built from an action function symbol αi and a possibly empty tuple ⃗x of object arguments. Situations are first-order terms denoting states resulting from sequences of actions. The constant S0 denotes the initial situation, namely the empty action sequence, and function do(a, s) denotes the next situation resulting from executing action a in situation s. Objects are first-order terms other than actions and situations. Fluents are relations whose values may vary between situations (we do not consider functional fluents). A fluent is denoted by a predicate symbol whose last argument has the sort situation.

A basic action theory (BAT) D is a set of five classes of axioms to model actions and their effects [Reiter, 2001] described below. In axioms, all free variables (they start with lower roman case letters) including object variables ⃗x, situation variable s, and a variable a of sort action are taken to be ∀-quantified at the front.

Foundational axioms for situations. These are domain independent second-order axioms that characterize situations [Reiter, 2001].

Unique name axioms (UNA). The actions of the domain and the object constants are pairwise unequal.

Action precondition axioms. For each action α(⃗x), there is one axiom of the form Poss(α(⃗x), s) ≡ Πα(⃗x, s), where Poss(α(⃗x), s) is a special predicate that denotes that the action α(⃗x) is executable in situation s, and the condition Πα(⃗x, s) is a formula uniform in s, i.e., such that s is the only situation term, with the other free variables among ⃗x at most, and where Poss cannot occur.

Successor state axioms (SSAs). For each fluent F(⃗x, s) (in the BAT), there is an axiom of the form

where γ+ F (⃗x, a, s), γF (⃗x, a, s) are formulas uniform in s. with free variables among ⃗x, a, and s at most. This SSA defines the value of F in the next situation do(a, s) in terms of what holds in the current situation s. Each formula γ+ F (⃗x, a, s) (resp., γF (⃗x, a, s)) is a finite disjunction of

for some action term αi(⃗t, ⃗y) and some situation calculus formula ψi(⃗x, ⃗y, s) uniform in s, called a context condition, all of whose free object variables are at most among ⃗x, ⃗y. All object variables ⃗t are included in ⃗x, and ⃗y are the new variables not included in ⃗x, if any. If the context condition is situation independent, e.g., ψi(⃗x, ⃗y, s) is a boolean combination of equalities between variables from ⃗x, ⃗y, then an action αi(⃗t, ⃗y) has an unconditional effect on a fluent F. In the SSA for the fluent F, if all actions have unconditional effects on F, then this SSA is called context-free. When all SSA are contextfree, the BAT is said to be context-free. Here, we consider the original variant of context-free SSAs [Reiter, 1991]:

where the SSA specifies the extension of F in the situation resulting from executing action a in s, only if a is indeed executable in s according to its precondition axiom.

When in Formula (1) above, the variables ⃗t in αi(⃗t, ⃗y) include all of the arguments ⃗x of the fluent on the left hand side of a generic SSA, we say that this action αi has a local effect on the fluent F because αi can change the fluent only at the single tuple of object constants, which is used to instantiate arguments of the action, [Vassos et al., 2008]. Notice that, an action with non-local effects can change a fluent at infinitely many object elements, in general. When all actions have only local effect, the BAT is said to be local effect.

Initial situation description. A set of logical formulas uniform in S0. It specifies the values of all fluents in the initial state. In particular in this paper we will consider DS0 to be constituted by a finite set of positive facts, i.e., ground atomic formulas (under open-world assumption). Notice that because of the form of basic action theories, if the axioms constituting the initial situation description (together with UNA) are satisfiable (and this is always the case, when such a description amounts to a finite set of positive facts) then the entire action theory is satisfiable [Reiter, 2001].

Description Logics TBoxes. Description logics (DLs) [Baader et al., 2003] are formalisms for representing knowledge on a domain of interest that is invariant over time, in terms of individuals denoting objects, concepts denoting sets of objects, and roles denoting binary relations between objects. In DLs, starting from countably infinite, mutually disjoint sets of concepts names (denoted by A) and roles names (denoted by P), we construct complex concept and role expressions (or simply, concepts C and roles R) by inductively applying constructors that depend on the DL in question.

A DL TBox is constituted by a finite set of (general) concept inclusions of the form C ⊑ C ′ , whose form again depends on the DL. Notice that we allow inclusions to be cyclic, e.g., ∃parent ⊑ Person, ∃parent - ⊑ Person, and Person ⊑ ∃parent which type the parent role on both components with Person, and express that every person has a parent. This is required in virtually all ontology-based and conceptual modeling applications: e.g., it is needed to capture UML Class Diagrams or ER Schemas [Baader et al., 2003]. 1

In this paper we focus mainly on the DLs ALC, EL⊥, and DL-Litecore. In ALC, roles are just names P, and concepts are formed according to the syntax:

IN fact C ⊔ C ′ is equivalent to ¬(¬C ⊓ ¬C ′ ), and ∀P.C to ¬∃P.¬C. An ALC TBox consists of concept inclusions between arbitrary ALC concepts.

In the DL-Lite family [Calvanese et al., 2007; 2013], a role R is either a role name P or an inverse role P -, while a concept C is either a concept name A, or the projection of a role P on its first, ∃P.⊤ written ∃P, or second, ∃P -.⊤ written ∃P -, component. A DL-Litecore TBox is a set of concept inclusions of the form C ⊑ C ′ or C ⊑ ¬C ′ , where C and C ′ are DL-Lite concepts. Notice that in DL-Lite negation is used just to express disjointness.

In the EL family [Baader et al., 2008], roles are names, and concepts obey the syntax C ::= A | C ⊓ C | ∃P .C. An EL⊥ TBox consists of concept inclusions of the form C ⊑ C ′ , C ⊑ ⊥, dom(P) ⊑ C, or ran(P) ⊑ C, where C, C ′ are EL concepts, ⊥ denotes the empty concept, dom(P) denotes the range of role P (i.e., ∃P) , and ran(P) its range (i.e., ∃P -).

We observe that DL-Litecore is a fragment of the variant of DL-Lite corresponding to the OWL 2 QL profile of OWL 2, and that EL⊥ is a fragment of EL++, the DL corresponding to the OWL 2 EL profile [Motik and others, 2012].

1 When a TBox is acyclic, it can be treated as a set of abbreviations that can be eliminated w.l.o.g. Hence, in our setting, an acyclic TBox does not need to be treated as a set of state constraints [Gu and Soutchanski, 2010].

The semantics of DLs is based on first-order interpretations. In fact, one can provide a translation function πx that translates an atomic DL concept C into an open formula C(x), and TBox inclusions into first-order axioms. The translation πx is inductively defined as follows:

BATs extended with TBoxes. We use DL TBoxes as state constraints [Lin and Reiter, 1994]. These are situation calculus sentences having a single situation variable s as the only situation term, which is universally quantified. To use a DL TBoxes as state constraints, it suffices to add a situation argument s to the atomic predicates corresponding to concepts and roles, and quantify over the situation universally in concept inclusions. In particular, we consider fluents partitioned into two sets. On the first set, which we call the frame, we have SSAs: so effects of actions are directly specified on them otherwise inertial holds (solution to the frame problem). On the second one we don't and their extension is only constrained by the values of the fluents in the first set and the TBox state constraints only. Inertia it is not assumed. We call the resulting action theories BATs extended with TBoxes.

3 BATs with ALC TBoxes

We start our analysis by showing undecidability of the satisfiability problem for basic action theories extended with an ALC TBox as state constrains. For now, we pose no restriction on the form of BAT. This is possibly the easiest case to consider, and the proof can be done quite naturally by relying on tiling. In the next sections we will gradually strengthen this result, first still relying on tiling, and then relying on a more involved encoding of Turing machines.

An instance of tiling [van Emde Boas, 1997] is constituted by a set D = {D1, . . . ,Dm} of tile types with an initial tile type D1, a horizontal adjacency relation H, and a vertical adjacency relation V over D. A D-tiling is a total function T : N × N -→ {D1, . . . ,Dm}. Given a instance T = 〈{D1, . . . ,Dm},D1,H, V 〉 of tiling, we call a D-tiling T correct for T if (T(i, j), T(i + 1, j)) ∈ H and (T (i, j), T (i, j+1)) ∈ V , where i, j ∈ N, and T (0, 0) = D1. The (unbounded quadrant) tiling problem consists in determining, given an instance of tiling, whether a correct tiling exists. This problem is well known to be undecidable.

Given an instance of the tiling problem, we construct an extended action theory Γ formed by a BAT and state constraints in the form of ALC TBox concept inclusions. We use one atomic concept G to denote the points in the grid (one coordinate being the object and the other coordinate being the situation), the atomic concepts D1, . . . , Dm denoting tile types, plus auxiliary ones PD1, . . . ,PDm, and one role Right to represent one dimension of the grid. There are no SSAs for the fluents Dk(x, s), k ∈ {1, . . . ,m}, but their values are implicitly defined via state constraints. For all the other we have SSA (they form the frame). We use a 0-ary action Up for the other dimension of the grid. The action Up is possible in every situation (Poss(Up, s) ≡ true). Thus, we build the grid by using the structural component for Right , and the temporal component for Up.

To deal with the tile types:

To encode the horizontal adjacency relation, we use the DL concept inclusions:

To encode the vertical adjacency relation, we use a successor state axiom exploiting the vertical relation V and auxiliary fluents PDh(x, s) that stand for "Tile Dh is possible at point (x, s)", and a TBox concept inclusion stating that if tile Dh is used then it must be "possible":

Finally for the initial situation, we have only two facts G(O0, S0) and D1(O0, S0), where O0 is an object constant. (The pair (O0, S0) represent the origin of the grid.)

Theorem 1. Satisfiability of BATs extended with an ALC TBox as state constraints is undecidable.

Proof. We use the above construction to show that existence of a correct tiling reduces to satisfiability of an extended BAT. Let T be an instance of the tiling problem and Γ the corresponding extended action theory.

First, we show how to construct from a correct tiling T for T a model M of Γ. The model M has only one action that interprets Up, has N as both the object and the situation domain, and is defined as follows:

• OM 0 = 0, SM 0 = 0, and do(Up, s)M = 1+ sM;
• Right M = {(x, x + 1, y) | x, y ∈ N};
• GM = {(x, y) | x, y ∈ N};
• DM k = PDMk = {(x, y) | T(x, y) =Dk}.

By definition, the correct tiling T respects the horizontal and vertical adjacency relations and the condition on the initial tile. It is easy to see that all axioms of Γ are satisfied inM.

Next, we show how to construct from a model M of Γ a correct tiling T for T. Specifically, to define T(x, y), for x, y ∈ N, let σy = do(Up, · · · do(Up, S0) · · · )M be obtained by applying the Up action y times to the initial situation S0, and let o0, o1, . . . , ox be objects such that o0 = OM 0 and (oi-1, oi, σy) ∈ Right M, for i ∈ {1, . . . , x}. Then T(x, y) = Dk, where (ox, σy) ∈ DM k . Notice that (i) The specific choice of o1, . . . , ox is irrelevant, since we quantify universally over the Right-successor (see axiom (7)); (ii) there is a unique predicate Dk that is true for object ox in situation σy, due to the disjointness axioms (5). It is easy to see that tiling T satisfies the horizontal and vertical adjacency relations, due to the axioms that encode such relations in Γ (in particular, axioms (7), (8), and (9)), and the initial tile condition. Hence, tiling T is correct.

4 BATs with AL TBoxes

We now turn to the simpler DL AL, which is a fragment of ALC where disjunctions and qualified existential are not allowed and negation is applied only to atomic concepts. AL concepts are build according to the following syntax: C ::= A | ¬A | C ⊓ C | ∃R | ∀R.C. Because of syntactic restrictions in AL, in the encoding developed above for ALC, the DL inclusion axioms (6) and (7) are not in AL. However, they can be reformulated in AL.

For axiom (6), it is immediate to observe that it is logically equivalent to the AL axiom:

To encode the horizontal adjacency relation in AL, instead of concept inclusions (7), we introduce new auxiliary concepts Ak, one for each Dk, and use the following 2m DL concept inclusions, where k, h∈{1, . . . ,m}:

Theorem2. Satisfiability of BATs extendedwith anALTBox as state constraints is undecidable.

Proof. The claim follows immediately from Theorem 1, by observing that the new axioms (10), (11), and (12) are logically equivalent to the axioms (6), (7) that they replace.

5 Local Effect, Context-Free BATs with Lightweight DLs TBoxes

Next we consider TBoxes expressed in lightweight DLs. We show undecidability of satisfiability when state constraints are formulated in DL-Litecore, the simplest logic of the DLLite family [Calvanese et al., 2007]. The result holds also for EL⊥. Moreover, while until now we have not considered restrictions on the form of the BAT itself, we show that undecidability holds even for BATs that are local effect [Vassos et al., 2008] and context-free [Reiter, 1991].

We exploit a reduction from the halting problem for Turing machines (TMs), relying on the fact that every TM can be transformed into the following variant. The machine starts with a blank tape that is infinite in both directions. Initially, the machine's head scans some cell on the tape, and we name this cell 0. If the given machine ever halts in some new cell, then it enters the special halting state. The fluents are the following: (1) Value(c, v, s), stating that the alphabet symbol in tape cell c is v in s. (2) State(q, s), stating that the machine's state is q in s. (3) Scan(c, s), stating that the machine's head is scanning tape cell c in s. (4) Next(l, r, s) relating adjacent cells in the tape (hence represents the tape), and stating that cell l is the one immediately to the left of cell r in s. (5) VT(x, s), stating that x is a tape cell belonging to the portion of the tape visited so far, in s. (6) NT(x, s) (disjoint from V T), stating that x is a (non-visited) tape cell (immediately) beyond the visited portion of the tape in s. (7) Halt(x, s), stating that the TM halts at cell x (entering the halting state, encoded by the constant QH) in s.

For each particular TM, we assume it is specified by a finite set of situation independent facts TM(q1, v1, q2, v2,m) encoding the TM transitions. Hence, q1, q2 range over the (finitely many) TM states, v1, v2 range over the (finitely many) tape alphabet symbols, and m ranges over {L,R}. 2

There are three actions, all encoding the TM transitions, but taking into account the position of the head with respect to the visited portion of the tape. Action Trans(l, c, r, q1, v1, q2, v2,m) means that the TM scanning symbol v1 in tape cell c when in state q1, enters state q2, writes tape symbol v2 to cell c (possibly replacing symbol v1 that was there previously) and the head makes transition m to another cell by moving either left or right. Cells l (read as "left of the current cell") and r (read as "right of the current cell") are adjacent to c. Actions TransL(ll, l, c, r, q1, v1, q2, v2) and TransR(l, c, r, rr, q1, v1, q2, v2) are similar to Trans, but take into account that the head is positioned on the left (resp., right) border of the portion of the tape visited so far and the move is just outside the current border. Moreover, an additional adjacent cell ll (resp., rr) is remembered for setting the new border when TransL (resp., TransR) become possible. The encoding as an extended action theory is as follows.

Precondition Axioms: Let the TM have a transition (q1, v1) m -→(q2, v2), i.e., TM(q1, v1, q2, v2,m) holds, where m ∈ {L,R}, and let the tuple 〈l, c, r〉 represent a block of three consecutive cells centered around the cell c under the machine's head. The action Trans(l, c, r, q1, v1, q2, v2,m) is possible in situation s iff the TM is in state q1, the head is scanning cell c, v1 is the alphabet symbol in c, the tape cells l, c, and r are next to each other, and the position to which the head moves has been already visited. Actions TransL(ll, l, c, r, q1, v1, q2, v2) (resp., TransR(l, c, r, rr, q1, v1, q2, v2)) are analogous, with the proviso that the move is to the left (resp., right) and the cell to which the head moves has never been visited before:

2 Note that the predicate TM can be trivially transformed into a fluent, by asserting the TM transitions as facts in S0 that no action can change.

Poss(Trans(l, c, r, q1, v1, q2, v2, m), s) ≡ TM (q1, v1, q2, v2, m) ∧ State(q1, s) ∧ Scan(c, s) ∧ Value(c, v1, s) ∧ Next (l, c, s) ∧ Next (c, r, s) ∧ ((m = L ∧ VT (l, s)) ∨ (m = R ∧ VT (r, s))) Poss(TransL(ll, l, c, r, q1, v1, q2, v2), s) ≡ TM (q1, v1, q2, v2, L) ∧ State(q1, s) ∧ Scan(c, s) ∧ Value(c, v1, s) ∧ Next (ll, l, s) ∧ Next (l, c, s) ∧ Next (c, r, s) ∧ NT (l, s) Poss(TransR(l, c, r, rr, q1, v1, q2, v2), s) ≡ TM (q1, v1, q2, v2, R) ∧ State(q1, s) ∧ Scan(c, s) ∧ Value(c, v1, s) ∧ Next (l, c, s) ∧ Next (c, r, s) ∧ Next (r, rr, s) ∧ NT (r, s)

Successor State Axioms (all context-free): The Next fluent (and hence the tape) is preserved across situations:

Poss(a, s) → (Next (l, r, do(a, s)) ≡ Next (l, r, s))

Cell x becomes visited only after a TransL or TransR action. Once a cell has been visited, it cannot become non-visited:

Poss(a, s) → (VT (x, do(a, s)) ≡ (∃ll, c, r, q1, q2, v1, v2.(a = TransL(ll, x, c, r, q1, v1, q2, v2))) ∨ (∃l, c, rr, q1, q2, v1, v2.(a = TransR(l, c, x, rr, q1, v1, q2, v2))) ∨ VT (x, s))

Cell x becomes NT after a TransL or TransR transition over the border, and it ceases to be NT if the head visits it:

Poss(a, s) → (NT (x, do(a, s)) ≡ (∃l, c, r, q1, q2, v1, v2.(a = TransL(x, l, c, r, q1, v1, q2, v2))) ∨ (∃l, c, r, q1, q2, v1, v2.(a = TransR(l, c, r, x, q1, v1, q2, v2))) ∨ (NT(x, s) ∧ ¬∃ll, l, c, r, rr, q1, q2, v1, v2.( a = TransL(ll, x, c, r, q1, v1, q2, v2) ∨ a = TransR(l, c, x, rr, q1, v1, q2, v2))))

The head can scan only one cell at a time. The head will be scanning the tape cell x in do(a, s) iff it was scanning c in s and moves either left or right to the adjacent cell x:

Poss(a, s) → (Scan(x, do(a, s)) ≡ ∃ll, l, c, r, rr, q1, q2, v1, v2.( a = Trans(x, c, r, q1, v1, q2, v2, L) ∨ a = Trans(l, c, x, q1, v1, q2, v2, R) ∨ a = TransL(ll, x, c, r, q1, v1, q2, v2) ∨ a = TransR(l, c, x, rr, q1, v1, q2, v2)))

The SSAs for the fluents State(q, s) consider that the TM goes into the state q by making a transition into this state, or it remains in state q if there is no transition out:

Poss(a, s) → (State(q, do(a, s)) ≡ ∃ll, l, c, r, rr, q1, v1, v2, m.( a = Trans(l, c, r, q1, v1, q, v2, m) ∨ a = TransL(ll, l, c, r, q1, v1, q, v2) ∨ a = TransR(l, c, r, rr, q1, v1, q, v2)) ∨ (State(q, s) ∧ ¬∃ll, l, c, r, rr, q1, v1, v2, m. ( a = Trans(l, c, r, q, v1, q1, v2, m) ∨ a = TransL(ll, l, c, r, q, v1, q1, v2) ∨ a = TransR(l, c, r, rr, q, v1, q1, v2))))

The SSA for Value(v, c, s) is very similar to the one for State(q, s):

Poss(a, s) → (Value(c, v, do(a, s)) ≡ ∃ll, l, r, rr, q1, v1, q2, m.( a = Trans(l, c, r, q1, v1, q, v, m) ∨ a = TransL(ll, l, c, r, q1, v1, q, v) ∨ a = TransR(l, c, r, rr, q1, v1, q, v)) ∨ (Value(c, v, s) ∧ ¬∃ll, l, r, rr, q1, v1, q2, m.( a = Trans(l, c, r, q1, v1, q, v, m) ∨ a = TransL(ll, l, c, r, q1, v1, q, v) ∨ a = TransR(l, c, r, rr, q1, v1, q, v))))

The next axiom states that the TM halts when it enters state QH .

Poss(a, s) → (Halt (x, do(a, s)) ≡ ∃ll, l, c, r, rr, q1, v1, v2.( a = Trans(x, c, r, q1, v1, QH, v2, L) ∨ a = Trans(l, c, x, q1, v1, QH, v2, R) ∨ a = TransL(ll, x, c, r, q1, v1, QH, v2) ∨ a = TransR(l, c, x, rr, q1, v1, QH, v2))).

TBox (formulated in DL-Litecore):

Scan ⊑ VT VT ⊑ ¬NT Halt ⊑ ¬VT ∃Next - ⊑ ∃Next ∃Next ⊑ ∃Next -

Initial situation description: It includes only the following positive facts 3 :

Scan(0, S0), Value(0, B, S0), Next(-1, 0, S0), Next(0, 1, S0), NT(-1, S0), NT(1, S0), State(Q0, S0)

The extended action theory above guarantees that in every model, there is a possibly infinite sequence of transitions corresponding to the TM transitions. As these transition occur, they force the existence of an expanding sequence of objects, correctly corresponding to the tape cells, connected by the Next relation 4 . These objects and their properties are preserved by the solution to the frame problem provided by the SSAs. In the case where the TM never halts, we get an unbounded tape. On the other hand, if the TM enters the halting state, we get a contradiction due to the fact that the object representing the tape cell under the head is forced to become simultaneously an instance of Halt and VT, which are disjoint. Hence, we get that the action theory above is satisfiable if and only the TM never halts. Note that all fluents are determined by the SSAs, i.e., are in the frame. This means that it is undecidable even to determine whether SSAs are consistent with TBox state constraints.

Theorem 3. Satisfiability of local effect, context free BATs extended with a DL-Litecore TBox as state constraints is undecidable.

The construction can be modified to prove undecidability also for EL⊥. The main difference is that, due to the lack of inverse roles, we need to work with a TM whose tape is infinite in only one direction, requiring more bookkeeping to deal with the beginning of the tape.

3 By UNA, all finitely many constants, including those in the situation independent facts encoding TM(· · · ), are pairwise disjoint.

4 Notice that, besides the part correctly encoding the TM computation, the model may contain also spurious objects and tuples.

Theorem 4. Satisfiability of local effect, context free BATs extended with an EL⊥ TBox as state constraints is undecidable.

We observe that [Reiter, 2001] separates action executability (possible situations) from satisfiability. To do so, it uses a variant of SSAs that are not conditioned on Poss. In this case, undecidability of satisfiability cannot be shown along the lines above. However, an analogous construction can be used to show that the executability problem, which focuses only on possible actions, remains undecidable. Obviously, if the theory is inconsistent checking executability makes no sense.

6 Conclusion

In this paper, we have shown that the simplest kind of situation calculus action theories (context free and local effect BATs) extended with state constraints TBoxes expressed in the simplest DLs, even for the simplest form of reasoning (satisfiability) become undecidable. From our constructions it appears that the source of these undecidability results is the very solution to the frame problem, as provided by the SSAs in BATs, combined with the possibility of having in the TBox cyclic assertions. The latter is a crucial feature in description logic ontologies, which however may enforce the existence of infinitely many new objects in the state. It remains to be seen if limiting TBoxes to even less expressive ontology languages would preserve decidability. In particular, we observe that in all our proofs, we use TBoxes with cycles involving assertions of the form A ⊑ ∃R. If we disallow these constraints, e.g., by restricting the TBox language to (the DL fragment of) RDFS [Franconi et al., 2013], we break the crux of the above undecidability proofs, and potentially decidability can be regained. 5

In general, the results in this paper call for alternative approaches in combining actions and ontologies, such as those in [Liu et al., 2006; Eiter et al., 2008; Yehia and Soutchanski, 2012]. One approach that has been proved quite robust in combining temporal logics and description logics is the one based on applying temporal operators only to description logic axioms. This is related to the so-called Levesque's functional view of KBs [Levesque, 1984], which sees a KB (the ontology) as a system that allows for two kinds of operations: ASK, which returns the (certain) answer to queries, and TELL, which produces a new KB as the result of the application of an atomic action (this is also related to update [Winslett, 1988]). In particular approaches like [Baader et al., 2012; Calvanese et al., 2011] demonstrate that under this view even verification of sophisticated temporal properties (e.g., formulated in first-order based variants of the mu-calculus) over ontologies, ranging from lightweight to very expressive ones, becomes decidable under interesting general conditions. These ideas may be applied to combining ontologies and action theories as well, as shown in, e.g., [Bagheri Hariri et al., 2013b].

5 Cycles involving assertions of the form A ⊑ ∃R allow for generating infinite chains of objects. Notice, however, that all the DLs we considered here, when taken in isolation, have the finite model property: that is even if there exists an infinite model formed by chains, there are other models in which these chains are actually finite loops. We use inertia embedded in the SSAs to indirectly disallow such finite loops.