The color coding means:

: all participate
: Doctoral students participate

Abstracts

Dr. Andreas Maletti: Pushing for weighted tree automata

A weight normalization procedure, commonly called pushing, is introduced for weighted tree automata (wta) over commutative semifields. The normalization preserves the recognized weighted tree language even for nondeterministic wta, but it is most useful for bottom-up deterministic wta (dwta), where it can be used for minimization and equivalence testing. In both applications a careful selection of the weights to be redistributed followed by normalization allows a reduction of the general problem to the corresponding problem for bottom-up deterministic unweighted tree automata. The new minimization procedure runs in time O(|M| log |Q|) for a dwta M with states Q, and the new equivalence test for two dwta M1 and M2 runs in time O(|M1| log |Q1| + |M2| log |Q2|), where Q1 and Q2 are the states of M1 and M2, respectively. This improves the previously best known run-times O(|M| |Q|) and O(|M1| |M2|), respectively.

Sascha Wunderlich: Games on a Class of Circulant Cayley Graphs

Graphs are omnipresent in game theory. The special class of Cayley graphs uses the elements of groups as nodes and the groups' generators as edges. Therefore such graphs inherit fundamental properties from their underlying groups. This allows to reason about their structure easily. On the other hand, basic graph theoretic concepts are describable in terms of groups here. For instance, it is possible to represent action (e.g. the movement of a token) on Cayley graphs using group arithmetic.
In this talk I present the results from my diploma thesis. They mainly concern the specific case of singleton Büchi-games on a subclass of Cayley graphs built on cyclic groups. However, these findings can be seen as a starting point to a more general algebraic approach to game analysis.

Sebastian Maneth: Determinacy and Rewriting of Top-Down and MSO Tree Transformations

Given a transformation between two data structures, a basic question is, what sort of information it preserves. We say that a query is "determined" by a (view) transformation, if the result to the query can be reconstructed from the result of the view. This notion of "view-query determinacy" has been studied by the database community. We consider the problem of deciding for two given tree transformations, whether one is determined by the other. If the view transformation is induced by a tree transducer that may copy, then determinacy is undecidable, even for identity queries. For a large class of non-copying views, namely compositions of functional extended linear top-down tree transducers with regular look-ahead, we show that determinacy is decidable, where queries are given by deterministic top-down tree transducers with regular lookahead or by MSO tree transducers. We also show that if a query is determined, then it can be rewritten into a query that works directly over the view and is in the same class as the given query. The proof relies on the decidability of equivalence for the two considered classes of queries, and on their closure under composition.

Prof. Paul Gastin: Festive QuantLA opening in Leipzig

David Müller: Symbolic Model Checking of Timed Automata

Model checking allows to test whether a system meets a specification. A specialisation, model checking real-time systems, relies on systems with timed behavior. Timed automata serve as system model, whereas timed CTL serves as specification.
In this talk I present how to check reachability and safety properties for timed automata. Therefore an abstraction of the timed behavior is needed. Since the number of clock zones for a given timed automaton can be infinite, normalisation ensures the termination of the reachability algorithm by drop or relieve unnecessary constraints. The normalisation from David Dill cannot be applied to timed automata with diagonal constraints, i.e. constraints of the form c - d < n, so Bengtsson introduced splitted normalisation. In this talk I will present his normalisation and show how it can be applied to symbolic model checking of timed automata.

Prof. Ralf Moeller: Logical Foundations for Interpreting Streams of Data Descriptions

Manually annotating the multimedia documents is a time-consuming and cost-intensive task. In this talk, a media interpretation agent is defined for automatically generating annotations for multimedia documents. Observations of the agent are given as surface-level information extracted by state-of-the-art media analysis tools. Based on background knowledge the agent interprets observations by computing high-level explanations. Observations and their explanations constitute the annotations of a media document. For this purpose, we investigate an abduction algorithm which computes explanations using a logic-based knowledge representation formalism. Multiple explanations might be possible for certain media content. Since the agent's resources for computing explanations are limited, we need to control the abduction procedure in terms of branching of the computation process and “depth” of computed results, while still producing acceptable annotations. To control the abduction procedure, we employ a first-order probabilistic formalism

Claudia Carapelle: Satisfiability of CTL^* with constraints

CTL^* is a popular and expressive temporal logic, interpreted over Kripke structures whose nodes are labeled with atomic propositions. CTL^* can be enriched with the addition of atomic constraints: variables are attached to the node labels of the Kripke structure, an interpretation will then map them to values of a chosen concrete domain A. These enriched CTL^*(A) formulas will be able to use predicates from the concrete domain to state relations between these variables. Chosen the appropriate domain, CTL^*(A) formulas can express quantitative properties that ordinary CTL^* formulas could only approximate through abstraction. We can refer directly to concrete values and describe how they change in time, with many possible applications in model checking. In this talk we will show a method to prove decidability of CTL^* formulas with constraints over any (negation closed) concrete domain with a countable set of predicates. We will then use this method to solve the open question of satisfiability for CTL^*(Z) formulas: it is decidable! (here Z is the concrete domain formed by the integers and an infinite set of predicates that allow to express equality, order, equality to a constant and modulo equivalence)

Prof. Carsten Lutz: Ontology-Based Data Access: A Study Through Disjunctive Datalog, CSP, and MMSNP

Ontology-based data access is concerned with querying incomplete data sources in the presence of domain-specific knowledge provided by an ontology. A central notion in this setting is that of an ontology- mediated query, which is a database query coupled with an ontology. In this talk, I consider several classes of ontology-mediated queries where the database queries are given as some form of conjunctive query and the ontologies are formulated in description logics or other relevant fragments of first-order logic, such as the guarded fragment and the unary-negation fragment. The aim is to characterize ontology- mediated queries in terms of more conventional database query languages, to study their descriptive complexity, and to derive relevant new results for ontology-based data access. Specifically, we show that ontology-mediated queries have the same expressive power as natural fragments of disjunctive datalog and establish close connections to constraint satisfaction problems (CSP) and their logical generalization, MMSNP formulas. These connections are then exploited to obtain new results regarding first-order rewritability, datalog-rewritability, and the query containment problem for ontology-mediated queries, and to study P/NP dichotomies for them. The presented material is joint work with Meghyn Bienvenu, Balder ten Cate, and Frank Wolter.

Prof. Manfred Droste: Weighted Automata

We give an introduction into the area of weighted automata. They consist of classical finite automata in which the transitions carry weights. These weights may model, e.g., the cost, the consumption of resources, or the reliability or probability of the successful execution of the transitions. We will present different weight structures like semirings, bimonoids, lattices, and also computations of behaviors of recent interest like average sum or discounted sum of costs. If time permits, we present a characterization of the possible behaviors by rational series. (This is course that was planned for the summer school.)

Marcel Lippmann: Temporalising Ontology-Based Data Access

Ontology-based data access (OBDA) generalizes query answering in databases towards deduction since (i) the fact base is not assumed to contain complete knowledge (i.e., there is no closed world assumption), and (ii) the interpretation of the predicates occurring in the queries is constrained by axioms of an ontology. OBDA has been investigated in detail for the case where the ontology is expressed by an appropriate Description Logic (DL) and the queries are conjunctive queries. Motivated by situation awareness applications, we investigate an extension of OBDA to the temporal case. As query language we consider an extension of the well-known propositional temporal logic LTL where conjunctive queries can occur in place of propositional variables, and as ontology language we use the prototypical expressive DL ALC. For the resulting instance of temporalized OBDA, we investigate both data complexity and combined complexity of the query entailment problem.

Prof. Piero A. Bonatti: Practical Nonmonotonic Description Logics

Specifications with exceptions are common in science, law, and business. Surprisingly, Description Logics (one of the major knowledge representation formalisms) do not support exceptions, despite their many, well engineered implementations. In this talk we point out some of the complexity sources that have been preventing practical support of exceptions and other nonmonotonic inferences. We argue that in some case complexity is caused by "abuse" of nonmonotonic contstructs. This led us to investigate "prototype oriented" nonmonotonic description logics. We will report experimental evidence that this approach leads to formalisms and engines that can handle large nonmonotonic knowledge bases in practice.

Shiguang Feng: Ehrenfeucht–Fraïssé games on weighted temporal logic

The Ehrenfeucht–Fraïssé game was first formulated in classical model theory, in which it is a useful tool to show that some properties are not definable in first-order logic. In finite model theory, the EF game and many of its variants for some extensions of FO logic are widely used to prove nonaxiomatizability results in the corresponding logics. This makes it a nice tool to capture the expressiveness of a logic. TPTL and MTL are two classical timed extensions of LTL. Bouyer and others showed that TPTL is strictly more expressive than MTL, which was a 20-year-old conjecture. We consider TPTL(Z) and MTL(Z) whose semantics are based on weighted words in which every point is assigned a natural number as its weight. We define a weighted version of the EF game on temporal logic. Using these games, we do the following:
(1) show that TPTL(Z) is strictly more expressive than MTL(Z).
(2) show that the until hierarchy and the constant hierarchy are strict for both MTL(Z) and TPTL(Z).
(3) provide an easier proof for Bouyer's result.
We also show that:
(4) The SAT problem for MTL(Z) is undecidable ( consequently also for TPTL(Z) ).
(5) The SAT problem for the future fragment of TPTL(Z) is decidable.

Internal organisational meeting

Andreas Ecke: Instance Query Answering for Concepts Relaxed by Similarity Measures

In Description Logic (DL) knowledge bases (KBs), information is typically captured by crisp concept descriptions. However, for many practical applications querying the KB by crisp concepts is too restrictive. A controlled way of gradually relaxing a query concept can be achieved by the use of similarity measures. To this end we formalize the task of instance query answering for crisp DL KBs using concepts relaxed by similarity measures. We identify relevant properties for the similarity measure and give first results on a computation algorithm.