The color coding means:

: all participate
: Doctoral students participate

Abstracts

Prof. Dr. Franz Baader: Welcome to QuantLA

Daniel Borchmann: Extracting Confident General Concept Inclusions from Finite Interpretations

Ontologies are an important tool in today's design of intelligent systems. However, their construction tends to be complicated and expensive, as it normally has to be conducted by human experts. An approach to circumvent this issue is to employ techniques of automatic ontology construction. In this talk we shall introduce such a technique developed by Baader and Distel that exploits a connection between the Description Logic EL and the field of Formal Concept Analaysis. We shall also give a short introduction to the basic notions of Description Logics and Formal Concept Analsysis. A fundamental assumption in this work is that the underlying data is free of errors, which in general does not hold in practice. We therefore shall discuss an approach to this problem based on Confident General Concept Inclusions.

Prof. Dr. Dietrich Kuske: A formal power series whose set of representations as (ℕ,max,+)-automata is undecidable

(ℕ,max,+)-automata are classical finite automata whose transitions are equipped with natural numbers. The "weight" of an accepting run is the sum of the natural numbers seen along the run, the "weight" of a word is the maximal weight of an accepting run for that word. In this way, the behavior of a (ℕ,max,+)-automaton is a function assigning natural numbers to words (i.e., a "formal power series").
In 1994, Krob showed that the equivalence problem for such automata is undecidable, a significantly simplified proof was found by Colcombet in 2010. Based on this proof, we show the strengthening expressed by the title of this talk.

Dr. Ulrich Fahrenberg: My Adventures with Semirings

I will give a personal account on three different applications which have led me into semiring theory. I never intended to work with semirings; indeed I feel that these applications almost have dragged me into it. Here are the culprits:
• Timed automata are a widely-used tool for modeling and verifying systems with timing information. The standard algorithms for timed-automata verifiation work with so-called zones, but it turns out that max-plus polyhedra provide a much nicer framework for this. This is how I learned about free semimodules over the max-plus semiring.
• Energy problems concern themselves with the question whether a system can run indefinitely given some initial energy. These have been formulated and solved in a variety of different formalisms, but it turns out that there is a quite natural common framework which generalizes most of this. This is using automata over the semiring of so-called energy functions and is the reason I learned about *-continuous Kleene algebras.
• Specification theories are used to reason about complex systems at specification level and are used for example in software product lines. They exist in a number of different incarnations, serving different but related purposes. Asking what really constitutes a specification theory, at its core, leads naturally to a theory of residuated semirings-without-equality.

Prof. Dr. Heiko Vogler: Statistical Machine Translation using formal models

In this talk I try to illustrate that the concepts of weighted tree automata and weighted tree transducers can be useful in statistical machine translation of natural languages.
My apologies: I will not provide a survey on natural language processing (NLP); also, the selection of the references is strongly biased by my personal taste and abilities.

Vitaly Perevoshchikov: Multi-weighted automata and multi-weighted MSO logic

Weighted automata are non-deterministic automata where the transitions are equipped with weights. They can model quantitative aspects of systems like memory or power consumption. The value of a run can be computed, for example, as the maximum, limit average, or discounted sum of transition weights. In multi-weighted automata, transitions carry tuples of weights and can model, for example, the ratio between rewards and costs, or the efficiency of use of some primary resource under some upper bound constraint on some secondary resource. The behavior of these automata cannot be described using semirings or even valuation monoids. Here, we establish a connection between multi-weighted automata and multi-weighted logics. For the case of finite and infinite words, we show that suitable weighted MSO logics and these new weighted automata are expressively equivalent.

Prof. Dr. Manfred Droste: Weighted Automata and Logics

Quantitative models and quantitative analysis in Computer Science are receiving increased attention. The goal of this talk is to investigate quantitative automata and quantitative logics. Weighted automata on finite words have already been investigated in seminal work of SchÜtzenberger (1961). 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. This concept soon developed a flourishing theory.
We investigate weighted automata and their relationship to weighted logics. For this, we present syntax and semantics of a quantitative logic; the semantics counts 'how often' a formula is true in a given word. Our main result, extending the classical result of BÜchi, shows that if the weights are taken from an arbitrary semiring, then weighted automata and a syntactically defined fragment of our weighted logic are expressively equivalent. A corresponding result holds for infinite words. Moreover, this extends to quantitative automata investigated by Henzinger et al. with (non-semiring) average-type behaviors, or with discounting or limit average objectives for infinite words.

Shiguang Feng: The descriptive complexity of revised Second-order Horn logic

Dr. Nathalie Bertrand: Determinizing timed automata

Timed automata are frequently used to model real-time systems. Essentially timed automata are an extension of finite automata with guards and resets of continuous variables (called clocks) evolving at the same pace. They are extensively used in the context of validation of real-time systems. One of the reasons for this popularity is that, despite the fact that they represent infinite state systems, their reachability is decidable, thanks to the construction of the region graph abstraction.
As for other models, determinization is a key issue for several validation problems, such as monitoring, implementability and testing. However, not all timed automata can be determinized, and determinizability itself is undecidable. After introducing timed automata, we will review existing approaches to get round their unfeasible determinization. To conclude we will expose a recent game-based algorithm which, given a timed automaton, produces either a deterministic equivalent or a deterministic over-approximation.

Mike Behrisch: Which clones are automatic?

Clones are sets of finitary functions f:Aⁿ → A, n ∈ ℕ, on a fixed set A that are closed under composition and contain all projections. Their importance in general algebra is reflected by the fact that the set of term functions arising from the fundamental operations of any universal algebra forms a clone on the carrier of the algebra. In fact, every clone can be obtainded in this way. Since a complete understanding of all universal algebras is unlikely to be ever possible, it has been a major theme in abstract algebra to study algebraic structures up to term equivalence, i.e. equality of their clones of term functions. In order to satisfactorily carry out this ambitious programme, substantial knowledge about the lattice of all clones on a given set would be desirable. Due to work by E. Post, the clone lattice is completely understood for sets A of cardinality at most two, in which case it has at most countably many elements. Since the 1950th it is known that there exist continuum many clones on a finite carrier set containing at least three distinct elements. However, apart from numerous partial results, e.g. on minimal and maximal clones, mathematicians are basically clueless w.r.t. understanding the global structure of the lattice of all clones, even on finite sets.
On the other hand, it is a prominent topic in theoretical computer science and automata theory to study structures having a description by finite state machines. Specifically, a first-order structure of finite type is called automatic (w.r.t. a fixed class of automata) if its carrier set and each of its fundamental relations and operations (understood via their graphs) can be written as the accepted language of some automaton from the given class. A structure is called automatically presentable if it is isomorphic to an automatic structure. Transferring basic results and constructions from automata theory, it can be shown that automatically presentable structures enjoy nice properties, such as, for instance, having a decidable model checking problem (possibly with parameters), a decidable first-order theory etc.
Every clone can be understood itself as an algebra on an infinite carrier set, having finitely many finitary (at most binary) fundamental operations. Lacking knowledge about the clone lattice motivates the search for those clones having automatic presentations in this sense. A first approximation to this question is to look for the borderline separating clones with decidable and undecidable first-order theory. In the talk we shall discuss conjectures concerning these two questions and ideas to prove them.

Priv.-Doz. Dr. Daniel Kirsten: Separating rank logics over different fields

Rank Logics were introduced by Grohe et al in 2009 as one significant step towards a logics which captures polynomial time. Rank logics are remarkably expressive, e.g., one can define reachability in undirected graphs in rank logics without involving fixed points. On the contrary, the research on limitations of rank logics turned out to be very difficult.
In the talk, we show that the expressive power of first order logics with rank operators over different cyclic fields is incomparable. For this, we solve a combinatorial problem concerning the ranks of sequences of matrices which was considered as extremely difficult by several research groups.

Thomas Weidner: Probabilistic Logic and Probabilistic Automata

We present a monadic second-order logic which is extended by an expected value operator and show that this logic is expressively equivalent to probabilistic automata for both finite and infinite words. We give possible syntax extensions and an embedding of our probabilistic logic into weighted MSO logic. We further derive decidability results which are based on corresponding results for probabilistic automata.

PD Dr. Sebastian Rudolph: Modeling Compositionality via Matrix-Space Models of Language

Vector space models (VSMs) of natural language map linguistic constructs (words, phrases, sentences, documents) into high-dimensional vector spaces, based on the statistical analysis of large bodies of text. The underlying motivation for this approach in computational linguistics is the assumption that semantic similarity can be approximated by metrics in such vector spaces. Indeed, VSMs have been successfully applied for semantic analysis and catgorization tasks and are widely deployed today, e.g. in the area of Information Retrieval, most notably Web search.
In the course of this development, the aspect of semantic compositionality has received increasing interest. The central question there is if and how vector representation of composite linguistic constructs (like sentences) can be computed from the vector representations of their constituents (like words). In the literature, a plethora of different vector operations have been proposed for that purpose.
In my talk, I will illustrate that these diverse aproaches but also certain symbolic grammar formalisms (like regular expressions) are naturally subsumed by a model that is based on matrix multiplication, dubbed Matrix-Space Model (MSM). Moreover, I will argue that the proposed model is plausible algebraically, neuro-cognitively as well as psychologically.

Festive QuantLA opening in Dresden

Prof. Dr. Torsten Schaub: Potassco, the Potsdam Answer Set Solving Collection

Answer Set Programming (ASP) is on the verge of leaving the academic ivory tower and becoming an interesting alternative to established declarative solving paradigms in many application areas.
This is due to its appealing combination of a highly expressive yet simple modeling language with high performance solving technology.
This talk gives an overview of the open source project Potassco, the Potsdam Answer Set Solving Collection, bundling tools for Answer Set Programming developed at the University of Potsdam.
Given that certain applications require extensions or even an integration with other computing paradigms in order to be successfully solved, we also discuss some extensions to ASP and elaborate upon the resulting systems.