Chair for Automata Theory of the Institute for Theoretical Computer Science, Faculty of Computer Science at TU Dresden

Publications

2006

 F. Baader and R. Küsters. Nonstandard Inferences in Description Logics: The Story So Far. In D.M. Gabbay, S.S. Goncharov, and M. Zakharyaschev, editors, Mathematical Problems from Applied Logic I, volume 4 of International Mathematical Series, pages 1–75. Springer-Verlag, 2006.
Bibtex entry  Paper (PDF)

Abstract

Description logics (DLs) are a successful family of logic-based knowledge representation formalisms that can be used to represent the terminological knowledge of an application domain in a structured and formally well-founded way. DL systems provide their users with inference procedures that allow to reason about the represented knowledge. Standard inference problems (such as the subsumption and the instance problem) are now well-understood. Their computational properties (such as decidability and complexity) have been investigated in detail, and modern DL systems are equipped with highly optimized implementations of these inference procedures, which - in spite of their high worst-case complexity - perform quite well in practice. In applications of DL systems it has turned out that building and maintaining large DL knowledge bases can be further facilitated by procedures for other, non-standard inference problem, such as computing the least common subsumer and the most specific concept, and rewriting and matching of concepts. While the research concerning these non-standard inferences is not as mature as the one for the standard inferences, it has now reached a point where it makes sense to motivate these inferences within a uniform application framework, give an overview of the results obtained so far, describe the remaining open problems, and give perspectives for future research in this direction.

F. Baader and C. Lutz. Description Logic. In Patrick Blackburn, Johan van Benthem, and Frank Wolter, editors, The Handbook of Modal Logic, pages 757–820. Elsevier, 2006.
Bibtex entry  Paper (PS)

Abstract

Description logics are a family of knowledge representation languages that were developed independently of modal logics, but later turned out to be closely related to them. This chapter introduces description logics and briefly recalls the connections between description and modal logics, but then concentrates on means of expressivity and reasoning problems that are important for description logics, but not in the focus of research in modal logics.

F. Baader, C. Lutz, and B. Suntisrivaraporn. CEL—A Polynomial-time Reasoner for Life Science Ontologies. In U. Furbach and N. Shankar, editors, Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR'06), volume 4130 of Lecture Notes in Artificial Intelligence, pages 287–291. Springer-Verlag, 2006.
Bibtex entry  Paper (PS)  Paper (PDF)  ©Springer-Verlag

Abstract

CEL (Classifier for EL) is a reasoner for the small description logic EL+ which can be used to compute the subsumption hierarchy induced by EL+ ontologies. The most distinguishing feature of CEL is that, unlike other modern DL reasoners, it is based on a polynomial-time subsumption algorithm, which allows it to process very large ontologies in reasonable time. In spite of its restricted expressive power, EL+ is well-suited for formulating life science ontologies.

F. Baader, C. Lutz, and B. Suntisrivaraporn. Efficient Reasoning in EL^+. In Proceedings of the 2006 International Workshop on Description Logics (DL2006), CEUR-WS, 2006. To appear.
Bibtex entry  Paper (PS)  Paper (PDF)

Abstract

F. Baader and A. Okhotin. Complexity of Language Equations With One-Sided Concatenation and All Boolean Operations. In Jordi Levy, editor, Proceedings of the 20th International Workshop on Unification, UNIF'06, pages 59–73, 2006.
Bibtex entry  Paper (PDF)

Abstract

Language equations are equations where both the constants occurring in the equations and the solutions are formal languages. They have first been introduced in formal language theory, but are now also considered in other areas of computer science. In particular, they can be seen as unification problems in the algebra of languages whose operations are the Boolean operations and concatenation. They are also closely related to monadic set constraints. In the present paper, we restrict the attention to language equations with one-sided concatenation, but in contrast to previous work on these equations, we allow not just union but all Boolean operations to be used when formulating them. In addition, we are not just interested in deciding solvability of such equations, but also in deciding other properties of the set of solutions, like its cardinality (finite, infinite, uncountable) and whether it contains least/greatest solutions. We show that all these decision problems are ExpTime-complete.

Franz Baader, Silvio Ghilardi, and Cesare Tinelli. A new combination procedure for the word problem that generalizes fusion decidability results in modal logics. Information and Computation, 204(10):1413–1452, 2006.
Bibtex entry  Paper (PDF)

Abstract

Previous results for combining decision procedures for the word problem in the non-disjoint case do not apply to equational theories induced by modal logics---which are not disjoint for sharing the theory of Boolean algebras. Conversely, decidability results for the fusion of modal logics are strongly tailored towards the special theories at hand, and thus do not generalize to other types of equational theories. In this paper, we present a new approach for combining decision procedures for the word problem in the non-disjoint case that applies to equational theories induced by modal logics, but is not restricted to them. The known fusion decidability results for modal logics are instances of our approach. However, even for equational theories induced by modal logics our results are more general since they are not restricted to so-called normal modal logics.

P. Bonatti, C. Lutz, A. Murano, and M. Vardi. The Complexity of Enriched µ-Calculi. In Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener, editors, Proccedings of the 33rd International Colloquium on Automata, Languages and Programming, Part II (ICALP'06), volume 4052 of Lecture Notes in Computer Science, pages 540–551. Springer-Verlag, 2006.
Bibtex entry  Paper (PDF)  ©Springer-Verlag

Abstract

The fully enriched mu-calculus is the extension of the propositional mu-calculus with inverse programs, graded modalities, and nominals. While satisfiability in several expressive fragments of the fully enriched mu-calculus is known to be decidable and ExpTime-complete, it has recently been proved that the full calculus is undecidable. In this paper, we study the fragments of the fully enriched mu-calculus that are obtained by dropping at least one of the additional constructs. We show that, in all fragments obtained in this way, satisfiability is decidable and ExpTime-complete. Thus, we identify a family of decidable logics that are maximal (and incomparable) in expressive power. Our results are obtained by introducing two new automata models, showing that their emptyness problems are ExpTime-complete, and then reducing satisfiability in the relevant logics to this problem. The automata models we introduce are two-way graded alternating parity automata over infinite trees (2GAPT) and fully enriched automata (FEA) over infinite forests. The former are a common generalization of two incomparable automata models from the literature. The latter extend alternating automata in a similar way as the fully enriched mu-calculus extends the standard mu-calculus.

P. Bonatti, C. Lutz, and F. Wolter. Expressive Non-Monotonic Description Logics Based on Circumscription. In Patrick Doherty, John Mylopoulos, and Christopher Welty, editors, Proceedings of the Tenth International Conference on Principles of Knowledge Representation and Reasoning (KR'06), pages 400–410. AAAI Press, 2006.
Bibtex entry  Paper (PDF)

Abstract

We show that circumscription can be used to extend description logics (DLs) with non-monotonic features in a straightforward and transparent way. In particular, we consider extensions with circumscription of the expressive DLs ALCIO and ALCQO and prove that reasoning in these logics is decidable under a simple restriction: only concept names can be circumscribed, and role names vary freely during circumscription. We pinpoint the exact computational complexity of reasoning as complete for NP^NExp and NExp^NP, depending on whether or not the number of minimized and fixed predicates is assumed to be bounded by a constant. We also show that we cannot allow role names to be fixed during minimization rather than having them vary: this modification renders reasoning undecidable already in the basic DL ALC. Finally, we argue that non-monotonic DLs based on circumscription are an appropriate tool for modelling defeasible inheritance. In particular, we can avoid the restriction of non-monotonic reasoning to domain elements that are named by an individual constant, as adopted by other non-monotonic DLs.

S. Brandt. Standard and Non-standard reasoning in Description Logics. Ph.D. dissertation, Institute for Theoretical Computer Science, TU Dresden, Germany, 2006.
Bibtex entry  Paper (PDF)

Abstract

The present work deals with Description Logics (DLs), a class of knowledge representation formalisms used to represent and reason about classes of individuals and relations between such classes in a formally well-defined way. We provide novel results in three main directions. (1) Tractable reasoning revisited: in the 1990s, DL research has largely answered the question for practically relevant yet tractable DL formalisms in the negative. Due to novel application domains, especially the Life Sciences, and a surprising tractability result by Baader, we have re-visited this question, this time looking in a new direction: general terminologies (TBoxes) and extensions thereof defined over the DL EL and extensions thereof. As main positive result, we devise EL++(D)-CBoxes as a tractable DL formalism with optimal expressivity in the sense that every additional standard DL constructor, every extension of the TBox formalism, or every more powerful concrete domain, makes reasoning intractable. (2) Non-standard inferences for knowledge maintenance: non-standard inferences, such as matching, can support domain experts in maintaining DL knowledge bases in a structured and well-defined way. In order to extend their availability and promote their use, the present work extends the state of the art of non-standard inferences both w.r.t. theory and implementation. Our main results are implementations and performance evaluations of known matching algorithms for the DLs ALE and ALN, optimal non-deterministic polynomial time algorithms for matching under acyclic side conditions in ALN and sublanguages, and optimal algorithms for matching w.r.t. cyclic (and hybrid) EL-TBoxes. (3) Non-standard inferences over general concept inclusion (GCI) axioms: the utility of GCIs in modern DL knowledge bases and the relevance of non-standard inferences to knowledge maintenance naturally motivate the question for tractable DL formalism in which both can be provided. As main result, we propose hybrid EL-TBoxes as a solution to this hitherto open question.

Dzung Dinh-Khac. Two Types of Key Constraints in Description Logics with Concrete Domains. Master thesis, TU Dresden, Germany, 2006.
Bibtex entry  Paper (PDF)

Abstract

Description Logics (DLs) are a family of logic-based knowledge representation formalisms for representing and reasoning about conceptual knowledge. To represent and reason about concrete qualities of real-world entities such as size, duration, or amounts, DLs are equipped with concrete domains. Interestingly, DLs and DLs with concrete domains are useful in many applications, such as modelling database schemas and the semantic web. Recently, it has been suggested that the expressive power of DLs with concrete domains can be further extended by adding database-like key constraints. In database schemas, key constraints can be a source of additional inconsistencies, which DLs used in reasoning about database schemas should be able to capture. Up to now, two different types of key constraints, namely uniqueness constraints and funtional dependencies, have been considered in the context of DLs with concrete domains. Surprisingly, to the best of our knowledge the two types of key constraints have not been investigated in one single logic despite the fact that in some applications, both of them are needed. In this paper, we consider the first description logic with concrete domains, uniqueness constraints, and functional dependencies. It it obtained by extending the description logic ALC(D) (the basic propositional closed description logic ALC equipped with a concrete domain D) with key boxes consisting of key constraints. More precisely, we analyze the impact of the presence of both types of key constraints on decidability and complexity of reasoning. Following from previous results, uniqueness constraints and functional dependencies bring undecidability in the general case and in order to preserve decidability we need to consider a slightly restricted form of key constraints. In the restricted form, we are able to show that reasoning w.r.t. both types of key constraints is not harder than reasoning w.r.t. each of them individually. Furthermore, several extensions with acyclic TBoxes, general TBoxes, and inverse roles are also discussed.

S. Ghilardi, C. Lutz, and F. Wolter. Did I Damage my Ontology? A Case for Conservative Extensions in Description Logics. In Patrick Doherty, John Mylopoulos, and Christopher Welty, editors, Proceedings of the Tenth International Conference on Principles of Knowledge Representation and Reasoning (KR'06), pages 187–197. AAAI Press, 2006.
Bibtex entry  Paper (PDF)

Abstract

In computer science, ontologies are dynamic entities: to adapt them to new and evolving applications, it is necessary to frequently perform modifications such as the extension with new axioms and merging with other ontologies. We argue that, after performing such modifications, it is important to know whether the resulting ontology is a conservative extension of the original one. If this is not the case, then there may be unexpected consequences when using the modified ontology in place of the original one in applications. In this paper, we propose and investigate new reasoning problems based on the notion of conservative extension, assuming that ontologies are formulated as TBoxes in the description logic ALC. We show that the fundamental such reasoning problems are decidable and 2ExpTime-complete. Additionally, we perform a finer-grained analysis that distinguishes between the size of the original ontology and the size of the additional axioms. In particular, we show that there are algorithms whose runtime is "only" exponential in the size of the original ontology, but double exponential in the size of the added axioms. If the size of the new axioms is small compared to the size of the ontology, these algorithms are thus not significantly more complex than the standard reasoning services implemented in modern description logic reasoners. If the extension of an ontology is not conservative, our algorithm is capable of computing a concept that witnesses non-conservativeness. We show that the computed concepts are of (worst-case) minimal size.

S. Ghilardi, C. Lutz, F. Wolter, and M. Zakharyaschev. Conservative Extensions in Modal Logics. In Guido Governatori, Ian Hodkinson, and Yde Venema, editors, Advances in Modal Logics Volume 6, pages 187–207. College Publications, 2006.
Bibtex entry  Paper (PDF)

Abstract

Every modal logic L gives rise to the consequence relation that relates formulas phi and psi iff \psi is true in a world of an L-model whenever phi is true in that world. We consider the following algorithmic problem for L. Given two modal formulas phi1 and phi2, decide whether their conjunction is a conservative extension of phi1 in the sense that whenever psi is a consequence of the conjunction of phi1 and phi2 and psi does not contain propositional variables not occurring in phi1, then psi is already a consequence of phi1.. We first prove that the conservativeness problem is co-NExpTime-hard for all modal logics of unbounded width (which have rooted frames with more than N successors of the root, for any N smaller than omega. Then we show that this problem is (i) co-NExpTime-complete for S5 and K, (ii) in \ExpSpace for S4 and (iii) \ExpSpace-complete for GL.3 (the logic of finite strict linear orders). The proofs for S5 and K use the fact that these logics have uniform interpolants of exponential size.

Jan Hladik and Rafael Peñaloza. PSPACE Automata for Description Logics. In B. Parsia, U. Sattler, and D. Toman, editors, Proceedings of the 2006 International Workshop on Description Logics (DL'06), volume 189 of CEUR-WS, 2006.
Bibtex entry  Paper (PDF)

Abstract

Tree automata are often used for satisfiability testing in the area of description logics, which usually yields EXPTIME complexity results. We examine conditions under which this result can be improved, and we define two classes of automata, called segmentable and weakly-segmentable, for which emptiness can be decided using space logarithmic in the size of the automaton (and thus polynomial in the size of the input). The usefulness of segmentable automata is demonstrated by reproving the known PSPACE result for satisfiability of ALC concepts with respect to acyclic TBoxes.

H. Liu, C. Lutz, M. Milicic, and F. Wolter. Description Logic Actions with general TBoxes: a Pragmatic Approach. In Proceedings of the 2006 International Workshop on Description Logics (DL2006), 2006.
Bibtex entry  Paper (PDF)

Abstract

We recently proposed action formalisms based on description logics (DLs) as decidable fragments of well-established action theories such as the Situation Calculus and the Fluent Calculus. One short-coming of our initial proposal is that the considered formalisms admit only acyclic TBoxes, but not GCIs. In this paper, we define DL action formalisms that admit GCIs, propose a pragmatic approach to addressing the ramification problem that is introduced in this way, show that our formalim is decidable and investigate its computational complexity.

H. Liu, C. Lutz, M. Milicic, and F. Wolter. Reasoning about Actions using Description Logics with general TBoxes. In Michael Fisher, Wiebe van der Hoek, Boris Konev, and Alexei Lisitsa, editors, Proceedings of the 10th European Conference on Logics in Artificial Intelligence (JELIA 2006), volume 4160 of Lecture Notes in Artificial Intelligence, pages 266–279. Springer-Verlag, 2006.
Bibtex entry  Paper (PDF)

Abstract

Action formalisms based on description logics (DLs) have recently been introduced as decidable fragments of well-established action theories such as the Situation Calculus and the Fluent Calculus. However, existing DL action formalisms fail to include general TBoxes, which are the standard tool for formalising ontologies in modern description logics. We define a DL action formalism that admits general TBoxes, propose an approach to addressing the ramification problem that is introduced in this way, show that our formalism is decidable and perform a detailed investigation of its computational complexity.

H. Liu, C. Lutz, M. Milicic, and F. Wolter. Updating Description Logic ABoxes. In Patrick Doherty, John Mylopoulos, and Christopher Welty, editors, Proceedings of the Tenth International Conference on Principles of Knowledge Representation and Reasoning (KR'06), pages 46–56. AAAI Press, 2006.
Bibtex entry  Paper (PDF)

Abstract

Description logic (DL) ABoxes are a tool for describing the state of affairs in an application domain. In this paper, we consider the problem of updating ABoxes when the state changes. We assume that changes are described at an atomic level, i.e., in terms of possibly negated ABox assertions that involve only atomic concepts and roles. We analyze such basic ABox updates in several standard DLs by investigating whether the updated ABox can be expressed in these DLs and, if so, whether it is computable and what is its size. It turns out that DLs have to include nominals and the "@" constructor of hybrid logic (or, equivalently, admit Boolean ABoxes) for updated ABoxes to be expressible. We devise algorithms to compute updated ABoxes in several expressive DLs and show that an exponential blowup in the size of the whole input (original ABox + update information) cannot be avoided unless every PTIME problem is LOGTIME-parallelizable. We also exhibit ways to avoid an exponential blowup in the size of the original ABox, which is usually large compared to the update information.

C. Lutz. Complexity and Succinctness of Public Announcement Logic. In Peter Stone and Gerhard Weiss, editors, Proceedings of the Fifth International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS'06), pages 137–144. Association for Computing Machinery (ACM), 2006.
Bibtex entry  Paper (PDF)

Abstract

There is a recent trend of extending epistemic logic (EL) with dynamic operators that allow to express the evolution of knowledge and belief induced by knowledge-changing actions. The most basic such extension is public announcement logic (PAL), which is obtained from EL by adding an operator for truthful public announcements. In this paper, we consider the computational complexity of PAL and show that it coincides with that of EL. This holds in the single- and multi-agent case, and also in the presence of common knowledge operators. We also prove that there are properties that can be expressed exponentially more succinct in PAL than in EL. This shows that, despite the known fact that PAL and EL have the same expressive power, there is a benefit in adding the public announcement operator to EL: it exponentially increases the succinctness of formulas without having negative effects on computational complexity.

C. Lutz and M. Milicic. A Tableau Algorithm for Description Logics with Concrete Domains and General TBoxes. Journal of Automated Reasoning. Special Issue on on Automated Reasoning with Analytic Tableaux and Related Methods, 2006. To appear.
Bibtex entry  Paper (PDF)

Abstract

To use description logics (DLs) in an application, it is crucial to identify a DL that is sufficiently expressive to represent the relevant notions of the application domain, but for which reasoning is still decidable. Two means of expressivity that are required by many modern applications of DLs are concrete domains and general TBoxes. The former are used for defining concepts based on concrete qualities of their instances such as the weight, age, duration, and spatial extension. The purpose of the latter is to capture background knowledge by stating that the extension of a concept is included in the extension of another concept. Unfortunately, it is well- known that combining concrete domains with general TBoxes often leads to DLs for which reasoning is undecidable. In this paper, we identify a general property of concrete domains that is sufficient for proving decidability of DLs with both concrete domains and general TBoxes. We exhibit some useful concrete domains, most notably a spatial one based on the RCC-8 relations, which have this property. Then, we present a tableau algorithm for reasoning in DLs equipped with concrete domains and general TBoxes.

C. Lutz, D. Walther, and F. Wolter. Quantitative Temporal Logics: PSpace and below. Information and Computation, 205(1):99–123, 2006.
Bibtex entry  Paper (PS)

Abstract

In many cases, the addition of metric operators to qualitative temporal logics (TLs) increases the complexity of satisfiability by at least one exponential: while common qualitative TLs are complete for NP or PSpace, their metric extensions are often ExpSpace-complete or even undecidable. In this paper, we exhibit several metric extensions of qualitative TLs of the real line that are at most PSpace-complete, and analyze the transition from NP to PSpace for such logics. Our first result is that the logic obtained by extending since-until logic of the real line with the operators `sometime within n time units in the past/future' is still PSpace-complete. In contrast to existing results, we also capture the case where n is coded in binary and the finite variability assumption is not made. To establish containment in PSpace, we use a novel reduction technique that can also be used to prove tight upper complexity bounds for many other metric TLs in which the numerical parameters to metric operators are coded in binary. We then consider metric TLs of the reals that do not offer any qualitative temporal operators. In such languages, the complexity turns out to depend on whether binary or unary coding of parameters is assumed: satisfiability is still PSpace-complete under binary coding, but only NP-complete under unary coding.

C. Lutz and F. Wolter. Modal Logics of Topological Relations. Logical Methods in Computer Science, 2(2), 2006.
Bibtex entry  Paper (PS)

Abstract

Logical formalisms for reasoning about relations between spatial regions play a fundamental role in geographical information systems, spatial and constraint databases, and spatial reasoning in AI. In analogy with Halpern and Shoham's modal logic of time intervals based on the Allen relations, we introduce a family of modal logics equipped with eight modal operators that are interpreted by the Egenhofer-Franzosa (or RCC8) relations between regions in topological spaces such as the real plane. We investigate the expressive power and computational complexity of logics obtained in this way. It turns out that our modal logics have the same expressive power as the two-variable fragment of first-order logic, but are exponentially less succinct. The complexity ranges from (undecidable and) recursively enumerable to Pi_1^1-hard, where the recursively enumerable logics are obtained by considering substructures of structures induced by topological spaces. As our undecidability results also capture logics based on the real line, they improve upon undecidability results for interval temporal logics by Halpern and Shoham. We also analyze modal logics based on the five RCC5 relations, with similar results regarding the expressive power, but weaker results regarding the complexity.

Carsten Lutz, Franz Baader, Enrico Franconi, Domenico Lembo, Ralf Möller, Riccardo Rosati, Ulrike Sattler, Boontawee Suntisrivaraporn, and Sergio Tessaris. Reasoning Support for Ontology Design. In Bernardo Cuenca Grau, Pascal Hitzler, Connor Shankey, and Evan Wallace, editors, In Proceedings of the second international workshop OWL: Experiences and Directions, November 2006. To appear.
Bibtex entry  Paper (PDF)

Abstract

The design of comprehensive ontologies is a serious challenge. Therefore, it is necessary to support the ontology designer by providing him with design methodologies, ontology editors, and automated reasoning tools that explicate the consequences of his design decisions. Currently, reasoning tools are largely limited to the reasoning services (i) computing the subsumption hierarchy of the classes in an ontology and (ii) determining the consistency of these classes. In this paper, we survey the most important tasks that arise in ontology design and discuss how they can be supported by automated reasoning tools. In particular, we show that it is beneficial to go beyond the usual reasoning services (i) and (ii).

Rafael Peñaloza. Optimization of emptiness test of Buchi automata on infinite trees. Master's thesis, Dresden University of Technology, Germany, 2006.
Bibtex entry  Paper (PDF)

Abstract

Automata theory has proven to be a useful tool for solving decision problems, for example, the satisfiability problem in some logics. This approach consists basically in reducing the desired problem to the emptiness problem of automata. Unfortunately, this reduction leads in some cases to suboptimal methods. When this happens, it is usually possible to find properties in the specific automata that allow the emptiness test to be solved in an optimized manner. This path has been followed many times, but always done solely for the specific automata at the time. In this work general conditions are given, under which the emptiness test can be solved using only logarithmic space on the number of states. These conditions are later applied to prove that $\mathcal{ALC}$-satisfiability with respect to empty and acyclic TBoxes is in PSpace.

Baris Sertkaya. Computing the hierarchy of conjunctions of concept names and their negations in a Description Logic knowledge base using Formal Concept Analysis (ICFCA 2006). In Bernhard Ganter and Leonard Kwuida, editors, Contributions to ICFCA 2006, pages 73–86, Dresden, Germany, 2006. Verlag Allgemeine Wissenschaft.
Bibtex entry  Paper (PS)  Paper (PDF)

Abstract

In a series of previous work, we have presented how attribute exploration can be used in the bottom-up construction of DL knowledge bases to compute a concept lattice that is isomorphic to the subsumption hierarchy of all conjunctions of concept names occurring in a knowledge base, and the negations of these concept names. This work is a continuation in the line of the previous work, that makes a step towards more efficient computation of the mentioned hierarchy. Its specific accomplishment is reducing the number of questions asked to the expert and the number of objects produced during the computation of this hierarchy, thus speeding up the computation. Despite its simple nature, the approach speeds up the computation of this hierarchy drastically.

Anni-Yasmin Turhan, Sean Bechhofer, Alissa Kaplunova, Thorsten Liebig, Marko Luther, Ralf Möller, Olaf Noppens, Peter Patel-Schneider, Boontawee Suntisrivaraporn, and Timo Weithöner. DIG 2.0 – Towards a Flexible Interface for Description Logic Reasoners. In Bernardo Cuenca Grau, Pascal Hitzler, Connor Shankey, and Evan Wallace, editors, In Proceedings of the second international workshop OWL: Experiences and Directions, November 2006.
Bibtex entry  Paper (PS)  Paper (PDF)

Abstract

The DIG Interface provides an implementation-neutral mechanism for accessing Description Logic reasoner functionality. At a high level the interface can be realised as XML messages sent to the reasoner over HTTP connections, with the reasoner responding as appropriate. Key changes in the current version (DIG 2.0) include support for OWL 1.1 and well-defined mechanisms for extensions to the basic interface.

Anni-Yasmin Turhan, Thomas Springer, and Michael Berger. Pushing Doors for Modeling Contexts with OWL DL –a Case Study. In Jadwiga Indulska and Daniela Nicklas, editors, Proceedings of the Workshop on Context Modeling and Reasoning (CoMoRea'06). IEEE Computer Society, March 2006.
Bibtex entry  Paper (PS)  Paper (PDF)

Abstract

In this paper we present an integrated view for modeling and reasoning for context applications using OWL DL. In our case study, we describe a task driven approach to model typical situations as context concepts in an OWL DL ontology. At run-time OWL individuals form situation descriptions and by use of realization we recognise a certain context. We demonstrate the feasibility of our approach by performance measurements of available highly optimised Description Logics (DL) reasoners for OWL DL.

D. Walther, C. Lutz, F. Wolter, and M. Wooldridge. ATL is Indeed ExpTime-complete. Journal of Logic and Computation, 16(6):765–787, 2006.
Bibtex entry  Paper (PDF)

Abstract

The Alternating-time Temporal Logic (ATL) of Alur, Henzinger, and Kupferman is being increasingly widely applied in the specification and verification of open distributed systems and game-like multi-agent systems. In this paper, we investigate the computational complexity of the satisfiability problem for ATL. For the case where the set of agents is fixed in advance, this problem was settled at ExpTime-complete in a result of van Drimmelen. If the set of agents is not fixed in advance, then van Drimmelen's construction yields a 2ExpTime upper bound. In this paper, we focus on the latter case and define three natural variations of the satisfiability problem. Although none of these variations fixes the set of agents in advance, we are able to prove containment in ExpTime for all of them by means of a type elimination construction-thus improving the existing 2ExpTime upper bound to a tight ExpTime one.

home Back to the homepage of the Chair for Automata Theory.
Generated at Fri Mar 19 16:53:03 CET 2010.