Reasoning with Temporal aboxes: Combining dl-litecore with ctl

Abstract

The work shows the combination of standard description logics (DLs) with standard temporal logics (TLs). Indeed, the introduction of DLs as logic-based knowledge representation formalisms has emerged in many elds and many applications have taken advantage from it. Although that, in many of these applications also temporal aspects play an important role. It follows that a new formalism is needed in order to represent both terminological and temporal knowledge. At this aim, the majority of research works proposed the combination of DLs and TLs producing a new formalism to knowledge representation: temporal description logics (TDLs). This work illustrates the combination of the dl-litecore description logic with the temporal logic ctl. It de nes a temporal knowledge base with time-invariant tbox and time-variant abox. Furthermore an algorithm based on semantic model checking is proposed in order to query the knowledge base.

Keywords

• Description Logics
• Temporal Logics
• Semantic Web
• dl-lite
• ctl
• Model Checking

-

Recent work in service oriented architectures, business processes, databases focused on the need of dealing both with facts and processes [1{10]. In particular, the Temporal Description Logic is becoming more and more used for such a kind of problems [1, 4, 8{10]. Nevertheless, reasoning and query answering for a Temporal Description Logic is, in general, untractable or even undecidable (depending on which kind of Descrption Logic and which kind of Temporal Logic are considered [ 11 ]). This is due to the fact that in general a temporal knowledge base consists of a time-variant tbox and a time-variant abox, the abox is de ned according to an intensional de nition, with a time-variant domain, under the Open World Assumption. As a consequence, several authors studied how complexity can be reduced for speci c types of Temporal Description Logics where some of the above assumptions are dropped [ 11 ].

This paper presents a minimalistic approach based on a temporal knowledge base where the tbox is time invariant, the abox is de ned in an extensional fashion, the domain is constant, and the Closed World Assumption is adopted. The above choices allows us to obtain a tractable query answering algorithm that can be still used in several problems of practical interest, e.g. selection and composition of semantic web services, veri cation of business processes, management of e-learning processes.

The paper is structured as follows. Section 2 shows works that deal with temporal description logics. Section 3 depicts the temporal knowledge base proposed in this work. Section 4 illustrates the syntax and the semantics of temporal conjunctive queries used to query the temporal knowledge base. In 5 is shown the temporal conjunctive query answering algorithm based on propositional model checking. Finally, Section 6 closes the paper discussing the obtained results and some comparisons with other works are given. Finally, it will be proposed the future work. 2

Related Work

In the recent years many works focused on Temporal Description Logics [ 12, 11 ]. They mostly inspect how terminological aspects can be combined with temporal ones and evaluate the complexity of reasoning with such logics based on two-dimensional semantics [ 13 ]. Furthermore, other works introduce temporal description logics in order to deal with particular knowledge base query problems in several application elds.

Some works deal with web services specially for discovery, selection and composition[1, 14{16, 4]. Agarwal [ 1, 14 ] integrates the description logics SHIQ(D) and SHOIN (D) with the temporal description logic -calculus. The goal of the work is the de nition of a speci cation language for discovery, selection and composition of web services. The works proposed by Pistore et al. [ 15 ] and Di Pietro et al. [ 16, 4 ] deal with semantic web services selection using semantic model checking over the behavior description of services.

Weitl et al. [ 17 ] integrate the description logic ALC with the temporal logic ctl. in order to automate the veri cation of semi-structured documents. In that work, each proposition that appears in a ctl formula is a description logic axiom, i.e. a tbox statement. In a further work [ 18 ], they deal also with the generation of a more precise and comprehensible couterexample than the previous algorithm.

Hariri et al. [ 8 ] introduce the so-called Knowledge and Action Bases (KABs). A KAB is a knowledge base composed by a time invariant tbox expressed in dl-lite and a variable abox. Starting from an initial state of the knowledge base abox, its consecutive states are determined by executing conditioned actions over the abox. KAB properties veri cation is done using the -calculus temporal logic enriched with conjunctive queries. Baader et al. [ 9 ] develop a mechanism to temporalizing Ontology-Based Data Access (OBDA). They de ne a temporal knowledge base composed by a time invariant tbox and a sequence of aboxes that describes the observations about the state of a system of interest. Such knowledge base can be interrogated with temporal speci cations based on conjunctive queries and LTL temporal logic.

Temporal Knowledge Base Representation In general, a temporal knowledge base can be de ned as follows: De nition 1 (Temporal Knowledge Base). A Temporal Knowledge Base K = hTi; Aiii 0 consists of a sequence of tuples hTi; Aii which vary in respect to time instants i 0, where: Ti and Ai are respectively the terminological part ( tbox) and the assertional part ( abox) of the knowledge base at instant i.

In literature [ 12, 11 ] many approaches are proposed in order to specialize the general de nition of temporal knowledge base. Several of them focus on the definition of temporal description logics and, consequently, accomplish specialized knowledge bases suitable for the logics. The main elements that can be vary in order to realize di erent temporal knowledge bases are the following. The domain

I of the interpretation I = ( I ; I ) may be constant or vary over the time. The closed or open world assumption which determines whether the information available is complete or not. Furthermore both tboxes and aboxes may vary over the time. Finally, concerning the assertional part of the knowledge base, aboxes evolution can be intesionally or extensionally de ned. Those temporal knowledge base design choices in uence the knowledge base expressiveness and complexity. In the following are shown and explained the choices taken for this work.

First of all, it is supposed to have a constant (constant domain assumption [ 11 ]) and nite domain and the knowledge base makes use of the closed world assumption. This means that the domain does not depend on time instant and that the available information is complete. The above assumptions make feasible model checking as described in section 5.

According to De nition 1, a temporal knowledge base is formed by two components: tbox (the terminological part, i.e. a set of concepts) and abox (the assertional part, i.e. a set of facts). For the purpose of this work, it is taken account of dl-litecore [19{21].

In this description logic tbox statements are restricted only to inclusion statements (see Table 1.b). Intuitively, we can model an ontology only by means of subsumption between concepts, i.e. Cl v Cr. Notice that the tbox statement Cl1 t Cl2 v Cr is equivalent to the pair of statements Cl1 v Cr and Cl2 v Cr, and that Cl v Cr1 u Cr2 is equivalent to Cl v Cr1 and Cl v Cr2. In this very simple but still expressive logic, concepts and roles are de ned as follows: Cl ! A j 9R Cr ! A j 9R j :A j :9R

R ! P j P

Concerning an abox, intuitively it may represent the data of a knowledge base. An abox contains statements (or assertions) as described in Table 1.c. Intuitively, a concept assertion a:A (or A(a)) means that the individual denoted by constant a is an instance of concept A. A role assertion a:P = b (or P (a; b)) means that the pair of individuals (a; b) is an instance of role P , in other words a given individual b is a value for the role P of a.

The conjunctive query answering problem has a polynomial time complexity with this kind of description logic [ 19 ].

Concerning the representation of temporal aspects, the knowledge base presented here uses temporal aboxes (according to the de nition in [ 11 ]), i.e. a time-invariant tbox and a time-variant abox. Therefore an abox represents the state of a temporal knowledge base in a precise temporal instant. A time-variant abox can be represented according to either an intensional de nition (e.g. [ 8 ]) or an estensional de nition. In order to make feasible the query answering problem, in the work proposed in this paper, an estensional de nition is adopted.

Borrowing the notions of state and state transitions from the formal methods eld [ 22, 23 ], the temporal aspect of the knowledge base can be modeled as a state transition system on which, for each state, an abox is de ned. Indeed, the state of a system can usually be described by the values of a set of variables. These values change in the course of time and the changes are called state transitions. Some states are marked as initial states in order to represent the values that the system variables may have at the beginning (at time zero). These models usually assume that each state contains su cient information to allow future behavior to be determined only by the current state, and not by its past history; this is an example of the so-called Markovian process. In this work, a kind of state transition system is proposed which is called an annotated state transition system (asts). A transition relation describes how the state can evolve, therefore which aboxes at instant (t + 1) can be reached from an abox at instant t. Formally speaking: De nition 2 (Annotated State Transition System). Let T be the terminological part ( tbox) of a description logic. An annotated state transition system A de ned over a state transition system is a tuple hT ; ; i where: T is the terminological part ( tbox) of a description logic,

= hS; S0; Ri is the state transition system, S is the nite set of states; S0 S is the set of initial states; R S S is the transition relation;

: S ! 2AT is the annotation function, where AT is the set of all the concept assertions and role assertions de ned over T .

As a result of the formalization of the temporal aspects of the temporal knowledge base follows the following de nition which details De nition 1: De nition 3 (Temporal aboxes Knowledge Base). Let A = hT ; ; i be an asts. Let K = hTi; Aiii 0 a temporal knowledge base. Then K is a Temporal aboxes Knowledge Base if and only if: 8i Ti = T , 8i 9 si 2 S such that Ai = (si).

The temporal knowledge base evolution can be seen as (potentially unlimited) sequences of tuples hT ; (si)i where (si) is the abox on the state si at time instant i of the state transition system = hS; S0; Ri. 4

Integrating dl-lite with ctl

As proposed by Baader et al. [ 9 ] and extending the de nition of conjunctive query of description logics, the Temporal Conjunctive Query can be formally de ned as follows: De nition 4 (Temporal Conjunctive Query). Let A be an asts. Let K be a temporal aboxes knowledge base de ned over A. Then, a temporal conjunctive query which refers to K is recursively de ned as follows: = q j ^ j _ j : j

AF j AG j EF j EG !

j j AX A ( U ) j E ( U ) j A (

R j EX ) j E ( j R ) where q is a conjunctive query.

Intuitively, the temporal conjunctive query is a combination of conjunctive queries tied together by means of both propositional and temporal operators. Each conjunctive query q has the form q = ^ipi(xi), where: pi(xi) is either xi : Ci or xi;1:Ri = xi;2; and xi; xi;1; xi;2 are variables or individuals. Assuming that V(q) denotes the set of variables of q and C(q) denotes the set of individuals of q, then VC(q) = V(q) [ C(q) denotes the set of variables and individuals of q. When V(q) = ;, q is a ground conjunctive query, i.e. it is a conjunction of assertions. The de nition of V is extended to temporal conjunctive queries as follows: V( (q1; : : : ; qm)) = V(q1) [ V(q2) [ : : : V(qm). The de nition of C and VC can be extended in a similar way. When V( (q1; : : : ; qm)) = ;, (q1; : : : ; qm) is a ground temporal conjunctive query. Obviously, it is possible to annotate other temporal languages (e.g. ltl [ 24 ], or -calculus [ 25 ]), but for the sake of complexity, the annotation of ctl formulas is enough.

The semantics of a temporal conjunctive query is inductively de ned in two steps: | rst, the semantics of a conjunctive query is the base case; | second, the semantics of a temporal conjunctive query is the inductive step based on the semantics of ctl.

The semantics of a conjunctive query is based on the semantics of the underlying description logic, as reported in [ 26 ]. This means that the semantics of a conjunctive query can be viewed in terms of tables of a relational database. q(x) is the schema of the table (i.e. the relation schema) and I(q(x); s) is an instance of the table (i.e. a relation instance), in other words a set of tuples that hold in state s. Each tuple a is an assignment to x that answers to query q in the abox (s).

ctl is a propositional, branching-time, temporal logic that has Kripke semantics [ 24 ]. Intuitively, a temporal condition must be veri ed along all possible computation paths (state sequences) starting from the current state. Formally: a computation path is an in nite sequence hs0; s1; s2; : : : ; i of states in S such that 8i:9 : si ! si+1 2 R: Concerning the temporal operators (i.e., AF, EF, AX, and so on), they maintain the same intuitive meaning that they have in standard ctl. Here, the only di erence is that there are conjunctive queries instead of propositions.

As a consequence, the semantics of a temporal conjunctive query can be de ned as follows: De nition 5 (Semantics of a Temporal Conjunctive Query). Let K be a temporal aboxes knowledge base de ned over A. Let q[x] be a conjunctive query over K such that x = fx1; : : : ; xng. Let and be temporal conjunctive queries. Then:

K; s j= q[x] i 9 a:I(a) 2 ( I )n and hT ; (s)i j= q[x=a] K; s j= ^ i K; s j= and K; s j= K; s j= : i K; s 6j= K; s j= EX i 9hsi; s(i+1); s(i+2); : : : ; i such that s = si and K; s(i+1) j= K; s j= EG i 9hsi; s(i+1); s(i+2); : : : ; i such that s = si and 8j 0 . K; s(i+j) j= K; s j= E ( U ) i 9hsi; s(i+1); s(i+2); : : : ; i such that s = si and 9j:(K; s(i+j) j= and 8k < j:K; s(i+k) j= )

Notice that the constant domain assumption has been adopted, i.e. individuals are never destroyed or created over time [ 11 ] ( I is always the same for each state). The semantics of the other operators (i.e. _, !, EF, AF AG, EG, AX, EX, E(.R.), A(.U .), A(.R.)) can easily be derived from the semantics of the minimal set of operators by means of the following equivalences:

A( U ) :E(: U (: ^ : )) ^ :EG: AF :EG: EF E(true U ) AG :EF: E( R ) :A(: U : )

AX :EX: A( R ) :E(: U : ) 5

Temporal Conjunctive Query Answering

The temporal conjunctive query answering involves two problems: the entailment problem and the answering problem.

Regarding the rst problem, the following de nition is given: De nition 6 (Entailment Problem). Let be a temporal conjunctive query. Let K be a temporal aboxes knowledge base de ned over A. The Entailment Problem consists in deciding whether the temporal aboxes knowledge base K satis es the temporal conjunctive query . Formally: In other words, the entailment problem aims at checking whether a temporal knowledge base verify a given temporal speci cation or not. As a consequence, the result of this problem is a boolean value: true or false. The entailment problem does not give information about the temporal knowledge base data. Indeed, in most of the cases the goal of querying a knowledge base is to retrieve data that satisfy a given query. This problem can be de ned as follows: De nition 7 (Answering Problem). Let be a temporal conjunctive query. Let K be a temporal aboxes knowledge base de ned over A. The Answering Problem aims at searching all the individuals in the temporal knowledge base K which satis es the temporal conjunctive query . Formally:

Ans(K; [x]) = fa j I(a) 2 ( I )n and 9 s 2 S0; K; s j= [x=a]g where: x is an n-tuple denoting the variables of the temporal conjunctive query and a is an n-tuple of individuals that can be assigned to x.

It is clear that the Answering Problem (De nition 7) is tied with the Entailment Problem (De nition 6): the former checks whether a temporal conjuctive query models or not a temporal aboxes knowledge base and the latter gives the instances tuples which satis es the query. It follows the proposition: Proposition 1 (Temporal Conjunctive Query Answering). Let K be a temporal aboxes knowledge base de ned over A. Let be a temporal conjunctive query. Let Ans(K; [x]) be the outcome of the answering problem resulting by querying the temporal knowledge base K with the temporal conjunctive query . Then:

K j= i

Ans(K; [x]) 6= ;

In order to deal with both the problems de ned above, this work takes advantage of the work by Di Pietro et al. [ 16, 4 ] regarding semantic model checking for the semantic web service selection. They proposed four steps in order to verify whether a temporal speci cation matches a service process or not. Their algorithm can be used to deal with the temporal knowledge base proposed in this work.

De nition 8 (Semantic Model Checking Result). Let A be an asts. Let s 2 S be an asts state. Let [x] be a temporal conjunctive query and [x=a] be the related formula obtained by assigning a to x. Let A; s ` [x=a] denote that, according to the semantic model checker, [x=a] is true which refers to A and state s. Then, the outcome of the semantic model checker is de ned as follows: smc( A; [x]) = fa j I(a) 2 ( I )n and 9 s 2 S0; A; s ` [x=a]g

The fact that there exists at least an assignment (i.e. smc( A; [x]) 6= ;) is denoted as: A ` .

For the sake of space, here it is reported only a short introduction to such an algorithm. The reader may refer to [ 4 ] for a more detailed description and to Appendix A for the pseudocode of the semantic model checking algorithm. The steps of the algorithm are the following. First, a given temporal conjunctive query is translated into its positive normal form (temporal conjunctive query normalization), a more convenient form for the semantic model checking algorithm. The normal form can be obtained by pushing negations inward as far as possible. Then, temporal knowledge base grounding consists in applying to each abox in

A, each conjunctive query in . This step aims at mapping conjunctive queries in into propositions in order to obtain a nite sts. According to the closed world assumption, when a conjunctive query has a non-empty answer in a given state (abox), the corresponding proposition is set to true in that state, to false otherwise. All the assignments, that represent an answer for any conjunctive query, are joined in a table called Asser in the algorithms in Appendix A. Regarding the query, temporal conjunctive query grounding is performed to obtain a set of propositional queries containing conditions on state propositions in place of queries of the original formula . Considering the closed world assumption, this step generates a set of propositional (ground) temporal speci cations, one for each tuple in table Asser. At this point, the entailment problem has been reduced into a propositional model checking problem. Therefore, propositional model checking aims at verifying for each tuple in Asser whether the related propositional temporal speci cation is satis ed. If so, the tuple is inserted in smc( A; ). At the end, smc( A; ) contains all the answers to the temporal conjunctive query.

Now it is possible to state the following theorem about the soundness and completeness of the proposed approach.

Theorem 1 (Soundness & Completeness).

A; s `

A ` i i

K; s j= Proof. [Hint] The proof of (1) is reported in [ 4 ]. From (1) it follows that smc( A; [x]) = Ans(K; [x]). Hence, it follows (2)

Given that the entailment and answering problems (De nitions 6 and 7) are solved using semantic model checking, their complexities can be evaluated with the complexity of the semantic model checking algorithm. It follows: Theorem 2 (Complexity). The semantic model checking algorithm is decidable in time

max(O(j Aj j j jCQAj) ; O(j Aj jM Cj)) where j Aj is proportional to the number and size of the states, j j is proportional to the length of , jCQAj is the complexity of conjunctive query answering, and jM Cj is the complexity of propositional temporal logic model checking. Proof. [Hint] The semantic model checking algorithm calls the conjunctive query answering algorithm n j S j times, where n is the number of conjunctive queries in the temporal speci cation (proportional to j j) and j S j is the number of states (it is proportional to j Aj). The result of conjunctive query answering is used to build a set of propositions whose number is less than or equal to m j ( I )h j. The algorithm builds a join table in polynomial time. From this table, a set of propositional temporal speci cations is built in polynomial time. Finally, the semantic model checking algorithm performs a traditional propositional temporal logic model checking a number of times that is proportional to the size of the join table. The size of the join table depends on the number of individuals in I and, thus, on j Aj. 6

Discussion and Conclusion

In this paper is presented a minimalistic approach to the problem of query answering in temporal knowledge bases.

Results reported in Section 5 show how temporal reasoning with a temporal knowledge base, under the minimalistic approach (i.e. the assumptions introduced in Section 3: dl-litecore, ctl, time invariant tbox, time variant abox, constant and nite domain, closed-world assumption) is tractable. Up to now, such an approach has been con rmed to be useful to solve several veri cation (entailment) problems: semantic web service identi cation [ 27 ], selection [ 16 ], composition [ 15 ], and security [ 28 ]. Furthermore, its application to entailment problems ranges from business processes [ 29 ] to e-learning processes [ 30 ]. The original contribution of this paper consists in proposing to apply the minimalistic approach to query-answering problems as well, maintaining the same complexity and the same assumptions. As a matter of fact, it is still possible to use the same semantic model checking algorithm (as discussed in Section 5). Some practical experiments in real world applications of the proposed approach to temporal query-answering has been planned as future work.

Algorithms

tcq normalization(in: ; out: 0); tkb grounding (in: A; 0; out: ; Asser); tcq grounding (in: 0; Asser; out: ) b := f alse; smc( A; ) := ; for each '(r) 2 do f if prop model checking (in: ; '(r)) then b := true smc( A; ) := smc( A; ) [ frg

Fig. 1. The semantic model checking algorithm. Algorithm 2: tkb grounding input : A = hhS; S0; Ri; T ; i /* asts */

0 = 0(q1; : : : ; qm) /* Temporal conjunctive query */ output: = hhS; S0; Ri; P; X i /* Finite sts */

Asser /* Join of all the tables */ := ;; P := ; for each qi (1 i for each s 2 S do f for each a : C 2 (s) do for each a:R = b 2 (s) do g for each s 2 S do f

X (s) := ; ; for each qi (1 i m) do f

I(qi; s) := cq answering(qi; hT ; (s)i); if :qi 2 0 then

I(qi; s) := h n I(qi; s); Asser(qi) := Asser(qi) [ I(qi; s); for each pj (xj ) 2 qi do for each r 2 xj (I(qi; s)) do f := := [ fag;

[ fa; bg; P := P [ fP ROP (pj (r))g; if not (:qi 2 0) then

X (s) := X (s) [ fP ROP (pj (r))g; else if hT ; (s)i ` pj (r)

X (s) := X (s) [ fP ROP (pj (r))g;

:= ;; for each r 2 Asser do f '(r) := 0; for each x 2 V( 0) do /* substitute each occurence of x with x(r) */ '(r) := '[x= x(r)]; := [ f'(r)g;

Fig. 3. The temporal conjunctive query grounding algorithm.

References

1. S. Agarwal . A goal speci cation language for automated discovery and composition of web services . In International Conference on Web Intelligence , Silicon Valley, USA, 2007 .

2. A. Deutsch , L. Sui , V. Vianu , and D. Zhou . Veri cation of communicating datadriven web services . In PODS '06: Proceedings of the twenty- fth ACM SIGMODSIGACT-SIGART symposium on Principles of database systems , pages 90 { 99 , New York, NY, USA, 2006 . ACM.

3. Victor Vianu . Automatic veri cation of database-driven systems: a new frontier . In Proceedings of the 12th International Conference on Database Theory , pages 1 { 13 . ACM, 2009 .

4. I. Di Pietro , F. Pagliarecci , and L. Spalazzi . Model checking semantically annotated services . Software Engineering , IEEE Transactions on, 38 ( 3 ): 592 { 608 , 2012 .

5. S. Halle , R. Villemaire , and O. Cherkaoui . Specifying and validating data-aware temporal web service properties . IEEE Trans. on Software Engineering , 99 ( 2 ): 669 { 683 , 2009 .

6. Daniela Grigori , Juan Carlos Corrales, Mokrane Bouzeghoub, and Ahmed Gater . Ranking bpel processes for service discovery . Services Computing , IEEE Transactions on, 3 ( 3 ): 178 { 192 , 2010 .

7. Ahmed Awad , Artem Polyvyanyy, and Mathias Weske . Semantic querying of business process models . In Enterprise Distributed Object Computing Conference , 2008 . EDOC' 08 . 12th International IEEE, pages 85 { 94 . IEEE, 2008 .

8. Babak Bagheri Hariri , Diego Calvanese, Giuseppe De Giacomo, Riccardo De Masellis, Paolo Felli, and Marco Montali . Veri cation of description logic knowledge and action bases . In Proc. of the 20th Eur. Conf. on Arti cial Intelligence (ECAI 2012 ), 2012 .

9. Franz Baader , Stefan Borgwardt, and Marcel Lippmann. Temporalizing ontologybased data access . In Proceedings of the 24th International Conference on Automated Deduction (CADE-24), Lecture Notes in Arti cial Intelligence , Lake Placid, NY , USA, 2013 . Springer-Verlag. To appear.

10. Feng Yang , JiuWei Wang , and Hemin Jin . A study on the customer behavior tracking model based on temporal description logic in the process of e-commerce . In Systems and Informatics (ICSAI) , 2012 International Conference on, pages 2289 { 2293 , 2012 .

11. C. Lutz , F. Wolter , and M. Zakharyaschev . Temporal description logics: A survey . In S. Demri and C.S. Jensen, editors, 15th International Symposium on Temporal Representation and Reasoning , TIME 2008 , pages 3 { 14. IEEE Computer Society, 2008 .

12. A. Artale and E. Franconi . A survey of temporal extensions of description logics . Ann. Math. Artif. Intell., 30 ( 1-4 ): 171 { 210 , 2000 .

13. Klaus Schild . Combining terminological logics with tense logic . In Miguel Filgueiras and Lus Damas , editors, Progress in Arti cial Intelligence , volume 727 of Lecture Notes in Computer Science, pages 105 { 120 . Springer Berlin Heidelberg, 1993 .

14. S. Agarwal . Formal Description of Web Services for Expressive Matchmaking . PhD thesis , Universitat Karlsruhe (TH) , Fakultat fur Wirtschaftswissenschaften , 2007 .

15. M. Pistore , L. Spalazzi , and P. Traverso . A minimalist approach to semantic annotations for web processes compositions . In Proc. of the 3rd European Semantic Web Conference (ESWC 2006 ). Springer{Verlag, Berlin, Germany, 2006 .

16. I. Di Pietro , F. Pagliarecci , L. Spalazzi , A. Marconi , and M. Pistore . Semantic Web Service Selection at the Process-Level: The eBay/Amazon/PayPal Case Study . In Web Intelligence , pages 605 { 611 , 2008 .

17. F. Weitl , M. Jaksic , and B. Freitag . Towards the automated veri cation of semistructured documents . Journal of Data & Knowledge Engineering , 68 : 292 { 317 , 2009 .

18. F. Weitl , S. Nakajima , and B. Freitag . Structured counterexamples for the temporal description logic alcctl . In Software Engineering and Formal Methods (SEFM) , 2010 8th IEEE International Conference on, pages 232 { 243 , 2010 .

19. D. Calvanese , G. De Giacomo, D. Lembo , M. Lenzerini , and R. Rosati . Data Complexity of Query Answering in Description Logics . In Tenth International Conference on Principles of Knowledge Representation and Reasoning . AAAI Press, 2006 .

20. Alessandro Artale , Diego Calvanese, Roman Kontchakov, and Michael Zakharyaschev . The dl-lite family and relations . Journal of Arti cial Intelligence Research , 36 ( 1 ):1{ 69 , 2009 .

21. D. Calvanese , G. De Giacomo, D. Lembo , M. Lenzerini , and R. Rosati . Data complexity of query answering in description logics . Arti cial Intelligence , 2012 . cited By (since 1996 ) 1 ; Article in Press.

22. S. S. Lam and A. U. Shankar . A relational notation for state transition systems . IEEE Trans. on Softw. Eng. , 16 ( 7 ): 755 , July 1990 .

23. E. M. Clarke and J. M. Wing . Formal methods: State of the art and future directions . ACM Computing Surveys , 28 ( 4 ): 626 { 643 , December 1996 .

24. E. A. Emerson . Temporal and modal logic . In J. van Leeuwen, editor, Handbook of Theoretical Computer Science , volume B: Formal Models and Semantics , chapter 14 , pages 996 { 1072 . Elsevier Science Publishers B.V.: Amsterdam, The Netherlands, New York, N.Y., 1990 .

25. E. Allen Emerson. Model checking and the mu-calculus . In Neil Immerman and Phokion G. Kolaitis, editors, Descriptive Complexity and Finite Models, Proceedings of a DIMACS Workshop , January 14- 17 , 1996 , Princeton University, volume 31 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science , pages 185 { 214 . American Mathematical Society, 1996 .

26. M. Ortiz , D. Calvanese , and T. Eiter . Characterizing Data Complexity for Conjunctive Query Answering in Expressive Description Logics . In 21st AAAI Conference on Arti cial Intelligence , pages 275 { 280 . AAAI Press, 2006 .

27. D. Bianchini , F. Pagliarecci , and L. Spalazzi . From Service Identi cation to Service Selection: An Interleaved Perspective . In G. Agha, O. Danvy , and J. Meseguer, editors, Formal Modeling: Actors , Open Systems, Biological Systems - Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday , volume 7000 of Lecture Notes in Computer Science, pages 223 { 240 . Springer, 2011 .

28. L. Boaro , E. Glorio , F. Pagliarecci , and L. Spalazzi . Model Checking Security Requirements for Web Services . In International Conference on High Performance Computing Simulation (HPCS '10) , june 2010 .

29. L. Boaro , E. Glorio , F. Pagliarecci , and L. Spalazzi . Business process design framework for B2B collaboration . In W. Smari and G. Fox, editors, 2011 International Conference on Collaboration Technologies and Systems (CTS 2011 ), pages 633 { 635 , Philadelphia, Pennsylvania, USA, May 23 -27, 2011 . IEEE.

30. T. Leo , F. Pagliarecci , and L. Spalazzi . eLearning for Complex System Professionals: Material Knowledge Representation, Retrieval, and Building . In 4th International Forum on Knowledge Asset Dynamics (IFKAD 09) , Glasgow, United Kingdom, February 17 { 18 2009.