DFG-Graduiertenkolleg Mathematische Logik und Anwendungen

Graduiertenkolloquium SS2007

Vorträge

• 7.05.2007
  Herr Dr. Felix Klaedtke
  Don't Care Words with an Application to the Automata-based Approach for Real Addition Abstract
  

• 21.05.2007
  Herr Prof. Georg Lausen
  Adding Constraints to RDFS Abstract
  

• 11.06.2007
  Herr Prof. Wolfgang May
  MARS: Modulare Aktive Regeln im Semantic Web Abstract
  

• 16.07.2007
  Herr Dr. Yijia Chen
  Subexponential Time and Fixed-Parameter Tractability Abstract
  

Abstracts

• Don't Care Words with an Application to the Automata-based Approach for Real Addition
  
  
  As already pointed out by Büchi, automata can be used to decide certain first-order theories of linear arithmetic, like the first-order theory over the reals with addition and the ordering. Reals are represented as infinite words, and the automata are recursively constructed from the formulas. This automata-based approach for representing and manipulating sets of reals has also applications in infinite state model checking. However, analogous to BDDs to represent finite sets, the sizes of the automata are an obstacle in the automata-based set representation.
  
  In this talk, I will show how so-called "don't cares sets" for BDDs can be generalized to languages as a means to reduce the automata sizes and how "don't care words" can be used to build a more efficient automata-based decision procedure for real addition. A general result about don't care words is that the minimal weak deterministic Büchi automaton with respect to a given don't care set with certain restrictions is uniquely determined and can be constructed efficiently. Further, as a side result of this work, I will show that a certain class of Büchi automata can be determinized more efficiently by using the standard powerset construction for finite word automata. This result improves the automata-based decision procedure for real addition further. We have implemented these improvements. Our implementation outperforms other state-of-the-art tools.
  
  This is joint work with Bernd Becker (Freiburg), Christian Dax (Zurich), and Jochen Eisinger (Freiburg).
  



• Adding Constraints to RDFS
  
  
  The goal of the Semantic Web is to support semantic interoperability between programs exchanging data on the web. To achieve this goal languages which provide semantic markup have been proposed. Prominent examples are RDF(S) and OWL-DL. The meaning of the underlying vocabulary of such languages typically is provided by an ontology. While RDF(S) allows only to build rather simple ontologies, OWL-DL allows to define more expressive ontologies. Whether or not this expressivity is needed depends on the requirements of the application being under consideration. Therefore both, RDF(S) and OWL-DL, have arguments in favor of them. We propose to enrich RDFS by constraints to be able to check the correctness of a given interpretation of an RDFS vocabulary. We demonstrate how keys and foreign key constraints defined with respect to a relational database schema can be expressed by our RDFS constraints such that exporting a relational database into RDF without loosing key information becomes possible. As a theoretical contribution we show that for an arbitrary set of constraints the satisfiability problem is undecidable.
  



• MARS: Modulare Aktive Regeln im Semantic Web
  
  
  In dem Vortrag wird ein im Rahmen der "Working Group I5: 'Evolution and Reactivity'" des EU NoE "REWERSE - Reasoning on the Web with Rules and Semantics" entwickelter Ansatz zur Beschreibung und Implementierung von Verhalten im Semantic Web beschrieben.
  
  Der Ansatz basiert auf dem Paradigma der Event-Condition-Action (ECA)-Regeln: Wenn ein bestimmtes Ereignis eintritt und eine Bedingung (die gegebenenfalls weitere Informationen aus Anfragen benötigt) erfüllt ist, soll eine bestimmte Aktion ausgeführt werden. Bei der Verwendung solcher Regeln im Semantic Web ist davon auszugehen, dass unterschiedliche Sprachen zur Beschreibung von Ereignissen, Anfragen und Aktionen zum Einsatz kommen und kombiniert werden. Es wird eine Ontologie aktiver Regeln sowie der darin verwendeten Sprachen vorgestellt, die diesen Anforderungen gerecht wird. Jede der verwendeten Sprachen wird durch ein oder mehrere autonome Knoten des Semantic Web unterstützt. Neben der Implementierung einer Infrastruktur auf Basis von XML und RDF soll dies in naher Zukunft auch Reasoning über Regeln und ihre Bestandteile ermöglichen.
  



• Subexponential Time and Fixed-Parameter Tractability
  
  
  Exponential complexity and parameterized complexity theories are two different approaches for a refined analysis of hard algorithmic problems. A central question of exponential complexity is whether 3-SAT is solvable in time 2^o(n), where n is the number of variables in the given 3-CNF formula. And in parameterized complexity a typical problem is whether we can decide if a graph G=(V,E) has a clique of size k in time f(k) |V|^O(1) for a computable function f, i.e., whether p-CLIQUE is fixed-parameter tractable.
  
  In every complexity theory, we can view the corresponding complexity world as a partial order with elements being the complexity classes, and the order relation being the inclusion relation. We show the partial order of exponential complexity is isomorphic to the partial order of parameterized complexity under the so-called "miniaturization mapping" M . Moreover we determine the preimage of the well known W-hierarchy under in exponential complexity world and prove that for various (classes of) problems their preimages coincide with natural reparameterizations which take into account the amount of nondeterminism needed to solve them. Our results have some interesting consequences, e.g.,
  
  (1) p-CLIQUE is fixed-parameter tractable if and only if there is an algorithm deciding whether a graph G=(V,E) has a clique of size k in time 2^{oeff(k ⋅ log |V|)} ⋅ |V|O(1).
  
  (2) If p-CLIQUE is fixed-parameter tractable, then there is an algorithm deciding whether a graph G=(V,E) has a clique of size k in time |V|^oeff(k).
  
  This is joint work with Jörg Flum and Martin Grohe.