Reasoning on Procedural Programs using Description Logics with Concrete Domains Ronald de Haan Technische Universität Wien Abstract. Existing approaches to assigning semantics to procedural programming languages do not easily allow automatic reasoning over programs. We assign a model theoretic semantics to programs of a sim- ple procedural language, by encoding them into description logics with concrete domains. This allows us to flexibly express several reasoning problems over procedural programs, and to solve them efficiently using existing reasoning algorithms, for certain fragments of the programming language. Furthermore, it allows us to explore for what further fragments of the programming language reasoning problems are decidable. 1 Introduction There has been much research investigating the formal semantics of (procedural) pro- grams. This has resulted in several different approaches (see for instance [5, 6]). Such approaches include defining several notions of semantics for programs (e.g. operational semantics, denotational semantics, axiomatic semantics) and investigating the rela- tions between these different notions. These approaches to investigating the semantics of programming languages are very useful for proving the correctness of compilers, for instance. However, it is very difficult to automatically solve reasoning problems on procedural programs (e.g. deciding whether two programs are equivalent) using such kinds of semantics. Also, there is no unified approach to express and automatically solve various different reasoning problems, based on these existing notions of semantics of programming languages. We propose an approach that solves these problems. We assign a model theoretic semantics to procedural programs. In particular, we will encode procedural programs as description logic knowledge bases. Description logics are widely used formalisms to reason about large and complex knowledge bases [1], and there are many efficient reasoners available for description logics. We will show that by means of this encoding of programs into description logic knowledge bases, we can express reasoning problems over programs in the description logic language, and in this way reduce such reasoning problems to description logic reasoning. This allows us to leverage the performance of existing reasoning algorithms for our reasoning problems. Furthermore, we illustrate how this approach can be helpful in identifying fragments of programming languages for which these reasoning problems are decidable, and analyzing the computational complexity of such reasoning. The paper is structured as follows. We begin with briefly repeating how the syntax and the semantics of the prototypical description logic ALC can be extended with concrete domains, resulting in the description logic ALC(D), before defining a simple R.K. Rendsvig and S. Katrenko (Eds.): ESSLLI 2012 Student Session Proceedings, CEUR Work- shop Proceedings vol.: see http://ceur-ws.org/, 2012, pp. 32–42. Reasoning on Procedural Programs using Description Logic 33 representative procedural programming language While. Then, we show how programs of this programming language can be encoded into the description logic ALC(D) in a semantically faithful way. Also, we illustrate how this allows us to encode reasoning problems over While programs into ALC(D) reasoning problems. Finally, we will discuss the benefit of this method, in combination with suggestions for further research. 2 Preliminaries A concrete domain D is a pair (∆D , ΦD ), where ∆D is a set and ΦD a set of predicate names. Each predicate name P ∈ ΦD is associated with an arity n and an n-ary predicate P D ⊆ ∆n D . A predicate conjunction of the form ^ (i) (i) c= (x0 , . . . , xn i ) : Pi , i≤k (i) where Pi is an ni -ary predicate, for all i ≤ k, and the xj are variables, is satisfiable iff there exists a function δ mapping the variables in c to elements of ∆D such that (i) (i) (δ(x0 ), . . . , δ(xni )) ∈ PiD , for all i ≤ k. A concrete domain is called admissible iff its set of predicate names is closed under negation and contains a name ⊤D for ∆D , and the satisfiability problem for finite conjunctions of predicates is decidable. An example of an admissible concrete domain is N = (N, ΦN ), where ΦN contains unary predicates ⊤N and ρn , and binary predicates ρ, for ρ ∈ {=, 6=, <, ≤, >, ≥}, and ternary predicates +, −, ⋆, \, and the required negations of predicates. All predicates are given the usual interpretation (here ρn holds for a value x iff x ρ n holds). We will use the description logic ALC(D) [2], which is the extension of the proto- typical description logic ALC [7] with concrete domains. For an overview of description logics with concrete domains, see [3]. We get the logic ALC(D), for a given concrete domain, by augmenting ALC with abstract features (roles interpreted as functional relations), concrete features (inter- preted as a partial function from the logical domain into the concrete domain), and a new concept constructor that allows to describe constraints on concrete values us- ing predicates from the concrete domain. More concretely, we can construct concepts ∃u1 , . . . , uk .P and u↑, for u, u1 , . . . , uk paths and P ∈ Ψ D a k-ary predicate. A path is a sequence f1 . . . fn g, where f1 , . . . , fn (for n ≥ 0) are abstract features and g is a concrete feature. Paths are interpreted as (partial) functions from the logical domain into the con- crete domain, by taking the composition of the interpretation of their components. Concepts ∃u1 , . . . , uk .P are interpreted as the set of objects that are in the domain of the interpretation of all ui , such that the resulting concrete objects satisfy the pre- dicate P . Concepts u↑ are interpreted as those objects that are not in the domain of the interpretation of u. For a complete, formal definition of the syntax and semantics of ALC(D), see [2, 3], for instance. 3 The Programming Language While 3.1 Syntax We define the syntax of the simple representative procedural programming language While (defined and used for similar purposes in [5, 6]) with the following grammar 34 Ronald de Haan (we use right-associative bracketing). Let X be a countably infinite set of variables. We let n range over values in N1 , x over X, a over expressions of category AExp, b over expressions of category BExp, and p over expressions of category Prog. a ::= n | x | a + a | a ⋆ a | a − a b ::= ⊤ | ⊥ | a = a | a ≤ a | ¬b | b ∧ b p ::= x := a | skip | p; p | if b then p else p | while b do p We consider programs as expressions of category Prog. We denote the set of variables occurring in a program p with V ar(p), the set of subterms of p of category BExp with Bool(p), and the set of subterms of p of category AExp with Arith(p). Furthermore, with cl(p) we denote the smallest set of programs such that: – cl(p) is closed under subterms, i.e., if p1 ∈ cl(p), p2 ∈ Sub(p) and p2 ∈ Prog, then p2 ∈ cl(p); and – if while b do p1 ∈ cl(p), then also p1 ; while b do p1 ∈ cl(p) ∈ cl(p). 3.2 Operational Semantics Given a finite subset of variables X ⊆ X, we define the set of states over X, denoted with StateX , as the set of total mappings µ : X → N. We define the function BX that interprets expressions of category BExp as a function from StateX to B. BX (s, a1 σ a2 ) = AX (s, a1 ) σ AX (s, a2 ) for σ ∈ {=, ≤} BX (s, ¬b) = ¬BX (s, b) BX (s, b1 ∧ b2 ) = BX (s, b1 ) ∧ BX (s, b2 ) We define the function AX that interprets expressions of category AExp as a function from StateX to N. AX (s, n) = n for n ∈ N AX (s, x) = state(x) for x ∈ X AX (s, a1 ρ a2 ) = AX (s, a1 ) ρ AX (s, a2 ) for ρ ∈ {+, ⋆} AX (s, a1 − a2 ) = AX (s, a1 ) − AX (s, a2 ) if AX (s, a1 ) − AX (s, a2 ) ≥ 0 AX (s, a1 − a2 ) = 0 if AX (s, a1 ) − AX (s, a2 ) < 0 For s ∈ StateX , x ∈ X and n ∈ N, we define s[x 7→ n](y) = n, if x = y, and s[x 7→ n](y) = s(y) if x 6= y. For a program p and a set X such that var(p) ⊆ X ⊆ X, we define the op- erational semantics as follows. We consider the transition system (Γ, T, ⇒), where Γ = {(q, s) | q ∈ cl(p), s ∈ StateX }, T = StateX , and ⇒ ⊆ Γ × (Γ ∪ T ). We define the relation ⇒ as the smallest relation such that for each s ∈ StateX , for each a ∈ AExp, and for each b ∈ BExp – we have (skip, s) ⇒ s; – we have (x := a, s) ⇒ s[x 7→ AX (a, s)]; – (p1 , s) ⇒ (p′1 , s′ ) implies (p1 ; p2 , s) ⇒ (p′1 ; p2 , s′ ); – (p1 , s) ⇒ s′ implies (p1 ; p2 , s) ⇒ (p2 , s′ ); 1 In this paper, we restrict ourselves to natural numbers, but the approach can be extended straightforwardly to other concrete domains. Reasoning on Procedural Programs using Description Logic 35 – we have (if b then p1 else p2 , s) ⇒ (p1 , s), if PX (b, s) = ⊤; – we have (if b then p1 else p2 , s) ⇒ (p2 , s), if PX (b, s) = ⊥; and – we have (while b do p, s) ⇒ (if b then (p; while b do p) else skip, s). Note that ⇒ is deterministic, i.e., for any s, t, t′ , if s ⇒ t and s ⇒ t′ , then t = t′ . We say that p terminates on s with outcome t if (p, s) ⇒∗ t for t ∈ T . We say that p does not terminate on s if there is no t ∈ T such that (p, s) ⇒∗ t. We take notice of the fact that if p does not terminate on s, then there is an infinite sequence (p, s) ⇒ (p′ , s′ ) ⇒ . . . starting from (p, s). 3.3 Normal Form In order to simplify our encoding of While programs into the description logic ALC(D) later, we define a notion of normal forms for While programs. Consider the following substitutions, preserving the operational semantics of programs, for a fresh variable x, for ρ ∈ {+, ⋆, −}, and π ∈ {=, ≤}: ϕ[x := a1 ρ a2 ] ❀ x1 := a1 ; ϕ[x := x1 ρ a2 ] if a1 6∈ X ϕ[x := a1 ρ a2 ] ❀ x2 := a2 ; ϕ[x := a1 ρ x2 ] if a2 6∈ X ϕ[a1 π a2 ] ❀ x1 := a1 ; ϕ[x1 π a2 ] if a1 6∈ X ϕ[a1 π a2 ] ❀ x2 := a2 ; ϕ[a1 π x2 ] if a2 6∈ X p ❀ p; skip if p not of the form q; skip Using the transformations on programs given by the above substitutions, we can trans- form any program p to an operationally equivalent program p′ such that the following holds: – each subexpression of p′ of category AExp is either of the form x ρ y, for x, y ∈ X and ρ ∈ {+, ⋆, −}, or of the form n for n ∈ N; – for each subexpression of p′ of category BExp of the form t ρ s, for ρ ∈ {=, ≤}, holds t, s ∈ X; and – either p′ = skip, or p′ is of the form e; skip. We will say that programs that satisfy this particular condition are in normal form. 4 Encoding Programs into ALC(D) We model programs in the language While using description logic and its model- theoretic semantics. The concrete (i.e. numerical) values in the programming language correspond to concrete values in the description logic. States are represented by ob- jects, and programs are represented by concepts. We represent the execution of pro- grams on states by a (functional) role nextState. In particular, for a given program p with V ar(p) = {x1 , . . . , xn }, we denote states s ∈ StateV ar(p) with objects that have concrete features valueOf xi . An execution of a program p will then be modelled by means of a nextState sequence of objects. The objects in this sequence represent the states occurring in the particular execution of the program. Whenever in this execution of the program there occurs a state s such that the execution is continued from this state s with the intermediate program p′ , the object corresponding to s is an element of the concept Cp′ . Also, whenever this execution terminates, the final object in this sequence is an element of the concept Cskip . 36 Ronald de Haan 4.1 Encoding Take an arbitrary program p, i.e., an expression of category Prog. W.l.o.g., we assume p is in normal form. We define an ALC(D) TBox T p as follows. We use concept names Cq for each q ∈ cl(p), and concept names Db for each b ∈ Bool(p). For each variable x ∈ V ar(p), we create a concrete feature valueOf x , and we require ⊤ ⊑ ¬valueOf x↑ (1) We let nextState be an abstract feature and for Cskip we require: Cskip ⊑ ¬∃nextState.⊤ (2) For each b ∈ Bool(p), we require the following, where x1 , x2 range over X, and b1 , b2 range over Bool(p): Dx1 =x2 ≡ ∃(valueOf x1 )(valueOf x2 ). = (3) Dx1 ≤x2 ≡ ∃(valueOf x1 )(valueOf x2 ). ≤ (4) D¬b1 ≡ ¬Db1 (5) Db1 ∧b2 ≡ Db1 ⊓ Db2 (6) Furthermore, we let D⊤ denote ⊤ and D⊥ denote ⊥. Then, for each q ∈ cl(p) of the form p1 ; p2 we require the following for Cq , where p1 , p2 , q1 , q2 range over cl(p), x, y1 , y2 range over X, a ranges over Arith(p), C(x:=a);p2 ⊑ ∃nextState.⊤ ⊓ ∃nextState.Cp2 (7) Cskip;p2 ⊑ Cp2 (8) C(x:=n);p2 ⊑ ∃(nextState valueOf x ). =n (9) C(x:=y);p2 ⊑ ∃(nextState valueOf x )(valueOf y ). = (10) C(x:=y1 +y2 );p2 ⊑ ∃(nextState valueOf x )(valueOf y1 )(valueOf y2 ).+ (11) C(x:=y1 −y2 );p2 ⊑ (¬∃(valueOf y2 )(valueOf y1 ). ≤ ⊔ ∃(valueOf y1 )(nextState valueOf x )(valueOf y2 ).+) ⊓ (¬∃(valueOf y2 )(valueOf y1 ). > ⊔ ∃(nextState valueOf x ). =0 ) (12) C(x:=y1 ⋆y2 );p2 ⊑ ∃(nextState valueOf x )(valueOf y1 )(valueOf y2 ).⋆ (13) C(x:=a);p2 ⊑ ∃(valueOf y )(nextState valueOf y ). = for y 6= x (14) C(if b then q1 else q2 );p2 ⊑ (¬Db ⊔ Cq1 ;p2 ) ⊓ (Db ⊔ Cq2 ;p2 ) (15) C(while b do q);p2 ⊑ (¬Db ⊔ Cq;(while b do q);p2 ) ⊓ (Db ⊔ Cp2 ) (16) Notice that, in general, the TBox T p is not acyclic, since Axioms (7), (8), (15) and (16) can together induce a cycle. 4.2 Correctness In order to use the above encoding of a program p into an ALC(D) TBox T p to reduce reasoning problems over programs into ALC(D) reasoning, we show the following cor- respondence between the operational semantics of p and the model theoretic semantics of T p . Reasoning on Procedural Programs using Description Logic 37 Lemma 1. For any program p, any X such that V ar(p) ⊆ X ⊆ X, any state s ∈ StateX , any b ∈ Bool(p), and for any model I = (∆I , ·I ) of T p , we have that d ∈ ∆I and (d, s(xi )) ∈ valueOf Ixi for all 1 ≤ i ≤ n implies that d ∈ CbI iff BX (b, s) = ⊤. Proof (sketch). By induction on the structure of b. All cases follow directly from the fact that Axioms (3)-(6) hold. Theorem 1. For any program p, any X such that V ar(p) ⊆ X ⊆ X, any state s ∈ StateX such that p terminates on s with outcome t, and for any model I = (∆I , ·I ) of T p we have that d ∈ CpI and (d, s(xi )) ∈ valueOf Ixi for all 1 ≤ i ≤ n implies that I e ∈ Cskip and (e, t(xi )) ∈ valueOf Ixi for all 1 ≤ i ≤ n, for some e ∈ ∆I . Proof. By induction on the length of the ⇒-derivation (p, s) ⇒k t. Assume d ∈ CpI and (d, s(xi )) ∈ valueOf Ixi for all 1 ≤ i ≤ n, for some d ∈ ∆I . The base case k = 0 holds vacuously. In the case for k = 1, we know p = skip, since p is in normal form. Therefore, we know s = t, and thus e = d witnesses the implication. In the inductive case, we distinguish several cases. Case p = skip; q. We know (p, s) ⇒ (q, s) ⇒k−1 t. Since I satisfies T p , by Axiom (8), we know d ∈ CqI . The result now follows directly by the induction hypothesis. Case p = (x := a); q. We know (p, s) ⇒ (q, s′ ) ⇒k−1 t, and s′ = s[x 7→ AX (a, s)]. Since I satisfies T p , by Axioms (7), (9)-(13) and (14), we know there must exist a d′ ∈ CqI such that (d′ , s′ (xi )) ∈ valueOf Ixi for all 1 ≤ i ≤ n. Then by the induction hypothesis, the result follows directly. Case p = (if b then p1 else p2 ); q. Assume BX (b, s) = ⊤. Then (p, s) ⇒ (p1 ; q, s) ⇒k−1 t. By Lemma 1, we know d ∈ DbI . Then, by the fact that Axiom (15) holds, we know d ∈ CpI1 ;q . The result now follows directly by the induction hypothesis. For BX (b, s) = ⊥ an analogous argument holds. Case p = (while b do p1 ); q. Assume BX (b, s) = ⊤. Then (p, s) ⇒2 (p1 ; p, s) ⇒k−2 t. By Lemma 1, we know d ∈ DbI . Then, by the fact that Axiom (16) holds, we know d ∈ Cp1 ;p . The result now follows directly by the induction hypothesis. If, however, in the same case holds BX (b, s) = ⊥, then (p, s) ⇒3 (q, s) ⇒k−3 t. By Lemma 1, we know d 6∈ DbI . By the fact that Axiom (16) holds, we know d ∈ CqI . The result now follows directly by the induction hypothesis. Theorem 2. For any program p, any X such that V ar(p) ⊆ X ⊆ X any state {x1 7→ c1 , . . . , xn 7→ cn } = s ∈ StateX such that p does not terminate on s, there exists a model I = (∆I , ·I ) of T p such that for some d ∈ ∆I we have d ∈ CpI , (d, ci ) ∈ valueOf Ixi , I for all 1 ≤ i ≤ n, and Cskip = ∅. Proof. Since p does not terminate on s, we know there exists an infinite ⇒-sequence (pi , si ) ⇒ (pi+1 , si+1 ), for i ∈ N, where (p1 , s1 ) = (p, s). Consider the following in- terpretation I = (∆I , ·I ), where ∆I = {(pi , si ) | i ∈ N}. For q ∈ cl(p), we let CqI = {(pi , si ) | pi = q}. For b ∈ Bool(p), we let DbI = {(pi , si ) | i ∈ N, PX (b, s) = ⊤}. For each x ∈ X, we let valueOf Ix = {((pi , si ), si (x)) | i ∈ N}. We let nextStateI = {((pi , si ), (pi+1 , si+1 )) | i ∈ N}. I I The definition of I implies that Cskip = ∅. Assume (pk , sk ) ∈ Cskip . Then pk = skip, and thus (pk , sk ) ⇒ sk , which contradicts our assumption of non-termination. I Clearly, I satisfies Axiom (1). Since Cskip = ∅, I also satisfies Axiom (2). It is easy I to verify, that by the definition of Db we get that I satisfies Axioms (3)-(6). To see that I satisfies Axioms (7)-(16), we take an arbitrary object (pj , sj ) in the interpretation an arbitrary class CqI , and we distinguish several cases. Consider 38 Ronald de Haan pj = skip; q. Then by the constraints on ⇒, pj+1 = q and sj+1 = sj . This witnesses that the subsumption in Axiom (8) holds. Consider pj = (x := a); q. Then by the constraints on ⇒, pj+1 = q and sj+1 = sj [x 7→ AX (a, sj )]. By definition of I, we know ((pj , sj ), (pj+1 , sj+1 )) ∈ nextStateI . It is now easy to verify that the subsumptions in Axioms (7), (9)-(13) and (14) are satisfied. Consider pj = (if b then p′1 else p′2 ); q. Assume BX (b, sj ) = ⊤. Then (pj , sj ) ∈ DbI . Also, by the constraints on ⇒, pj+1 = p′1 ; q and sj+1 = sj . It is easy to verify that, in this case, the subsumption in Axiom (15) holds. The case for BX (b, sj ) = ⊥ is completely analogous. Consider pj = (while b do p′ ); q. If BX (b, sj ) = ⊤, then (pj , sj ) ∈ DbI and pj+1 = p ; pj and sj+1 = sj . If BX (b, sj ) = ⊥, then (pj , sj ) 6∈ DbI and pj+1 = skip; q and ′ sj+1 = sj . It is easy to verify that, in either case, the subsumption in Axiom (16) holds. Theorem 3. For any program p, any X such that V ar(p) ⊆ X ⊆ X any state {x1 7→ c1 , . . . , xn 7→ cn } = s ∈ StateX such that p terminate on s, there exists a model I = (∆I , ·I ) of T p such that for some d ∈ ∆I we have d ∈ CpI , (d, ci ) ∈ valueOf Ixi , for all 1 ≤ i ≤ n. Proof (Sketch). We know there exists (p, s) ⇒k (p′ , s′ ) ⇒ t. Analogously to the proof of Theorem 2, we can construct a model I from the sequence (p, s) ⇒k (p′ , s′ ). By similar arguments to those in the proof of Theorem 2 it follows that I |= T p . Then, (p, s) ∈ CpI witnesses the further constraints on I. Note that the syntax and operational semantics of While can be adapted to various concrete domains with varying operators. The encoding into ALC(D) can be adapted correspondingly, and a corresponding correlation between the operational semantics and the model theoretic semantics can be proven. 4.3 Example To illustrate the method described above, of encoding While programs into ALC(D) TBoxes, we will consider an example. Let p0 be the following program in normal form, that computes the factorial of the value stored in variable x and outputs this in variable y. Note that variable z is simply used to refer to the constant value 1. p0 = (y := 1; z := 1; while x > z do (y := y ⋆ x; x := x − z); skip) Furthermore, we will use the following abbreviations to refer to subprograms of p0 . p1 = (z := 1; while x > z do (y := y ⋆ x; x := x − z); skip) p2 = (while x > z do (y := y ⋆ x; x := x − z); skip) p3 = (y := y ⋆ x; x := x − z) p4 = (x := x − z) Reasoning on Procedural Programs using Description Logic 39 We can now construct the ALC(D) TBox T p0 , in the fashion described above. T p0 = { ⊤ ⊑ ¬valueOf x↑, ⊤ ⊑ ¬valueOf y↑, ⊤ ⊑ ¬valueOf z↑, Cskip ⊑ ¬∃nextState.⊤, Dx ⊔ ∃(nextState valueOf x ). =0 ), C(x:=x−z);p2 ⊑ ∃(valueOf y )(nextState valueOf y ). =, C(x:=x−z);p2 ⊑ ∃(valueOf z )(nextState valueOf z ). = } Note that T p0 is not acyclic, since there are inclusion axioms (a) with Cp2 as lhs and Cp3 ;p2 in the rhs, (b) with Cp3 ;p2 as lhs and Cp4 ;p2 in the rhs, and (c) with Cp4 ;p2 as lhs and Cp2 in the rhs. These axioms are marked with the symbol †. It is straightforward to construct models of the TBox T p0 . One can simply take an execution of the program p0 , and transform this execution into a model of T p0 according to the intuition behind the encoding described above. 5 Reasoning Problems Theorems 1, 2 and 3 allow us to use the encoding of While programs into ALC(D) to reduce several reasoning problems over While programs to reasoning problems over ALC(D). For instance, termination of a program p reduces to unsatisfiability of the ABox Ap = {o1 : Cp } with respect to the TBox T p ∪ {Cskip ⊑ ⊥}. Also, we are able to encode abduction problems over While problems in the de- scription logic ALCO(D), which is ALC(D) extended with nominals. The question what input states for a program p could have led to the (partial) output state s, for dom(s) ⊆ V ar(p), reduces to finding models for Ap = {i : Cp , o : Cskip } ∪ {(o, s(x)) : valueOf x | x ∈ dom(s)} and T p , where Cskip is required to be a nominal concept. Another example is checking whether two (terminating) programs p1 and p2 are equivalent. Without loss of generality, we can assume V ar(p1 ) = V ar(p2 ). This equiv- alence check can be reduced to the problem of ALCO(D) unsatisfiability of the ABox Ap1 ,p2 = {o : Cp1 , o : Cp2 , s : Ctest } with respect to the TBox Sp1 ∪Sp2 ∪T eq , where Spi is 40 Ronald de Haan T pi with Cskip replaced by Cskipi , and T eq = {Ctest ≡ (∃.(res1 valueOf x1 )(res2 valueOf x1 ). 6= 1 2 ⊔ · · · ⊔ ∃.(res1 valueOf xn ) (res2 valueOf xn ). 6=) ⊓ ∃res1 .Cskip ⊓ ∃res2 .Cskip }, for res1 , 1 2 res2 abstract features, and Cskip , Cskip and Ctest nominal concepts. Naturally, this approach allows us to encode more intricate reasoning problems over While programs into description logic reasoning problems. Description logic offers us a very flexible formalism to express a variety of reasoning problems over While programs. 5.1 Decidability A bit of care has to be taken with this powerful and general approach. The problems we consider generally balance on the bounds of decidability. A concrete domain D is called arithmetic if its values contain the natural numbers, and it contains predicates for equality, equality with zero and incrementation. Unfor- tunately, satisfiability of ALC(D) concepts for arithmetic concrete domains D with respect to general TBoxes is undecidable [4]. So, for many cases, our approach doesn’t directly result in a decision procedure. This is no surprise, however. We know that we cannot decide equivalence of While programs in general. For instance for the concrete domain Z (with addition and equal- ity) we can easily encode the undecidable problem of whether a given Diophantine equation Φ(x1 , . . . , xn ) = 0 has an integer solution (the subject of Hilbert’s Tenth Problem) as a reasoning problem over While programs. Similarly, it can be proven that equivalence of While programs with concrete domain N is undecidable. Nevertheless, several decidable fragments of the While language can be obtained by either restricting the concrete domains or by forbidding statements of the form (while b do p). By forbidding these while-statements, we end up with acyclic TBoxes. We know that reasoning with respect to acyclic TBoxes is decidable for ALC(D). Restricting the concrete domain (and keeping while-statements), does not change the fact that we are dealing with general TBoxes. In this case, the concrete domain needs to be restricted quite severely, to get decidability. 5.2 Examples We can use the example from Section 4.3 to illustrate how to encode several reasoning problems over While programs into ALC(D) reasoning problems. For instance, we can encode the problem of checking whether p0 is terminating as the unsatisfiability problem of the ABox {o1 : Cp0 } with respect to the TBox T p ∪ {Cskip ⊑ ⊥}. Using the expressivity of the description logic ALC(D), we can in fact express a variety of different semantic properties to be checked automatically. For instance, in this fashion, we can express the problem whether p0 does not terminate with an output value for y that is less than or equal to 20 for all input values for x that are greater than or equal to 4. This problem can be reduced to the unsatisfiability of the ABox {o1 : Cp0 ⊓∃(hasValuex ). ≥4 } with respect to the TBox T p ∪{Cskip ⊑ ∃(hasValuey ). ≤20 }. These examples of expressing reasoning problems in the ALC(D) language illustrate the flexibility we get in expressing different reasoning problems. We can reduce the decision of any semantic property of While programs that is expressible using the modelling of While programs in the ALC(D) language to reasoning on ALC(D). Reasoning on Procedural Programs using Description Logic 41 6 Further Research The results presented in this paper are only the beginning of a larger inquiry investigat- ing the possibilities and bounds of approaching automated reasoning over (procedural) programming languages by means of assigning model-theoretic semantics to programs. We suggest a number of directions for further research needed to get a better under- standing of the topic. Similar encodings of programming languages into the description logic ALC(D) could also be devised also for other procedural programming languages, as well as for declarative programming languages. It needs to be investigated to what extent this method is extendable to such other languages. Suitable programming languages for which this could be investigated as a next step include extensions of the programming language While with language constructs for nondeterminism or parallellism, proce- dural programming languages that are based on goto-statements rather than while- statements, and simple, representative functional and logic programming languages that operate on similar domains (e.g. numerical values). Once the method presented in this paper has been applied to such languages, it will also be possible to investigate to what extent reasoning problems on multiple programs of different programming lan- guages (e.g. the equivalence problem of a While program and a program of a goto-based language) can be encoded in this framework. Another important direction for further research is identifying larger fragments of the programming language While for which reasoning problems on programs such as the ones we considered in this paper are decidable. By encoding programs into de- scription logics, we get a conceptually simpler setting to investigate such questions. Programming languages can have a variety of different constructs behaving in various ways. Reasoning over such diverse structures can get rather messy and complex. On the other hand, practically all reasoning problems for description logics can be reduced to finding models for description logic knowledge bases (i.e. reduced to the satisfia- bility problem). The problem of finding such models is conceptually simple, and the semantic definition of the description logic language guides the search for models. Such a conceptually simpler setting might make it easier to identify decidable fragments. In addition to this conceptual simplification of the problem, we could use results and techniques from the field of description logic when investigating the decidability of such fragments. For those fragments of the programming languages that lead to de- cidable reasoning problems, we can investigate the computational complexity of these reasoning problems. 7 Conclusions We assigned a model theoretic semantics to programs of the simple procedural lan- guage While, by encoding them into the description logic ALC(D). This allowed us to express a variety of reasoning problems over While programs using the expressivity of the description logic ALC(D). Furthermore, for a number of restricted fragments of the programming language While, this directly results in a method of solving such reason- ing problems using existing (description logic) algorithms. Furthermore, this encoding leads to a new approach of exploring what fragments of the programming language allow for decidable reasoning over programs. Further research includes a further char- acterization of fragments of the language that allow decidable reasoning, and extending this approach to different procedural (and declarative) programming languages. 42 Ronald de Haan References 1. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.: The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press (2003) 2. Baader, F., Hanschke, P.: A scheme for integrating concrete domains into concept languages. In: Proceedings of the 12th international joint conference on Artificial intelligence - Volume 1. pp. 452–457. IJCAI’91, Morgan Kaufmann Publishers Inc., San Francisco, CA, USA (1991) 3. Lutz, C.: Description logics with concrete domains—a survey. In: Advances in Modal Logics Volume 4. King’s College Publications (2003) 4. Lutz, C.: NExpTime-complete description logics with concrete domains. ACM Trans. Comput. Logic 5(4), 669–705 (Oct 2004) 5. Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer- Verlag New York, Inc., Secaucus, NJ, USA (1999) 6. Nielson, H.R., Nielson, F.: Semantics with Applications: A Formal Introduction. John Wiley & Sons, Inc., New York, NY, USA (1992) 7. Schmidt-Schaubß, M., Smolka, G.: Attributive concept descriptions with comple- ments. Artif. Intell. 48(1), 1–26 (Feb 1991)