It is possible to subscribe to a daily updated calendar that contains appointments from the table below using the following URIs1:
- For all seminars: http://www.math.tu-dresden.de/~mottet/cal/quantla-ss-2017.ics
- For all large seminars (PIs): http://www.math.tu-dresden.de/~mottet/cal/quantla-ss-2017-no-student.ics
How to subscribe to calendars may differ between applications, for the Mac OS Calendar App go to File -> New Calendar Subscription... and supply one of the given URIs.
The color coding means:
: all participate
: Doctoral students participate
: next seminar
Please find the abstracts below the schedule and note that some of the slides are made available here, internally.
1 This has been made possible by Antoine Mottet.
Abstracts
Barnaby Martin: Introduction to Quantified Constraints
We introduce the Quantified Constraint Satisfaction Problem (QCSP) as a modelling paradigm for non-monotone and dynamical problems. We recall the Boolean QCSP whose best-known case is Quantified Boolean Formulas (QBF), before concentrating on the general non-Boolean case. QCSPs are in general Pspace-complete and we will search for islands of tractability in the complexity seascape, where this complexity drops to NP, P or below.
Paul Gastin: Analysing timed systems using tree automata
Timed systems, such as timed automata, are usually analyzed using their operational semantics on timed words. The classical region abstraction for timed automata reduces them to (untimed) finite state automata with the same time-abstract properties, such as state reachability. We propose a new technique to analyze such timed systems. The main idea is to consider timed behaviors as graphs with matching edges capturing timing constraints. As an example, we develop the technique on timed pushdown systems. We show that their behaviors are graphs of bounded tree-width. Hence, they can be interpreted in trees opening the way to tree automata based techniques which are more powerful than analysis based on word automata. The technique is quite general and applies to many timed systems.
This is joint work with S. Akshay and S. Krishna from IIT Bombay, the extended abstract appeared in CONCUR 2016.
Dietrich Kuske: Hanf locality of counting extensions of first-order logic
We introduce a logic that extends first-order logic by counting, integer variables, and by numerical predicates. This logic can be viewed as joint generalization of various counting logics that have been studied in the literature.
We obtain a locality result showing that every formula of this logic can be transformed effectively into a formula in Hanf normal form that is equivalent on all finite structures of fixed bounded degree. A formula is in Hanf normal form if it is a Boolean combination of formulas describing the neighbourhood around its tuple of free variables and arithmetic sentences with numerical predicates over atomic statements describing the number of realizations of a type with a single center.
From this locality result, we infer the following applications:
- The Hanf-locality rank of first-order formulas of bounded quantifier alternation depth only grows polynomially with the formula size.
- The model checking problem for a natural fragment of our logic on structures of bounded degree is fixed-parameter tractable.
- The query evaluation problem for fixed queries from the fragment over fully dynamic databases of bounded degree can be solved efficiently: there is a dynamic algorithm that can enumerate the tuples in the query result with constant delay, and that allows to compute the size of the query result and to test if a given tuple belongs to the query result within constant time after every database update.
(These results are joint work with Nicole Schweikardt.)
Markus Ulbricht: The Complexity of Inconsistency
Minimal inconsistent subsets of knowledge bases play an important role in classical logics, for instance for diagnosis and repair. It turns out that for nonmonotonic reasoning a stronger notion is needed. We introduce such a notion, called strong inconsistency. It turns out that -in an arbitrary logic, monotonic or not- minimal strongly inconsistent subsets play a similar role as minimal inconsistent subsets in classical reasoning. In particular, the well-known classical duality between hitting sets of minimal inconsistent subsets and maximal consistent subsets generalizes to arbitrary logics if the strong notion of inconsistency is used.
After giving necessary preliminaries, we mainly focus on the computational complexity of various related reasoning problems. In particular, we compare usual inconsistency and strong inconsistency, since the latter is more involved in general. Since the notion of strong inconsistency is tailored for nonmonotonic frameworks, we will always distinguish between monotonic and nonmonotonic logics. It will, however, turn out that the theoretical worst-case complextiy of deciding (minimal) strong inconsistency is quite well-behaving in most cases.
Stefan Dück: Hanf's Lemma and Automata on Infinite Graphs
We study Hanf's Lemma and an extension to it featuring an additional existential quantifier for infinite structures. We show how to use this result to prove a Büchi-like connection between graph automata and logics for infinite graphs. Using valuation monoids, a very general weight structure able to model computations like average or discounting, we extend this result to the quantitative setting. This gives us the first general results connecting automata and logics over infinite graphs in the qualitative and the quantitative setting.
Mahsa Shirmohammadi: Minimal probabilistic automata have to make irrational choices
In this talk, we answer the question of whether, given a probabilistic automaton (PA) with rational transition probabilities, there always exists a minimal equivalent PA that also has rational transition probabilities. The PA and its minimal equivalent PA accept all finite words with equal probabilities.
We approach this problem by exhibiting a connection with a longstanding open question concerning nonnegative matrix factorization (NMF). NMF is the problem of decomposing a given nonnegative n×m matrix M into a product of a nonnegative n×d matrix W and a nonnegative d×m matrix H. In 1993 Cohen and Rothblum posed the problem of whether a rational matrix M always has an NMF of minimal inner dimension d whose factors W and H are also rational. We answer this question negatively, by exhibiting a matrix for which W and H require irrational entries. As a corollary we obtain a negative answer to the question on rationality of minimal probabilistic automata.
This talk is based on two papers in ICALP 2016 and SODA 2017.
Pavlos Marantidis: Weighted tree automata in Approximate Description Logics
Recently introduced problems in Description Logics (DLs) require the use of concept comparison measures. In this talk, we will briefly review these problems, show how concepts in the DL FL0 can be represented by infinite trees, and finally introduce and demonstrate how weighted automata working on aforementioned trees can be used to compute concept comparison measures.
Maximilian Pensel: Fixing Rational Reasoning for Quantification in Defeasible EL⊥
While Description Logics (DLs) are well-designed formalisms for knowledge representation and reasoning, their classical semantics are often insufficient in areas concerning human cognition such as reasoning under assumptions and tolerating inconsistencies. Defeasible Description Logics (DDLs) extend DLs with defeasible concept inclusions (DCIs) and nonmonotonic semantics. DCIs are implications that can (and should) be used for reasoning as long as they are not contradicted by more specific or strict knowledge. Reasoning in DDLs often employs rational or (the stronger) relevant closure according to the widely accepted postulates for propositional rational reasoning. Previous approaches to adapt these postulates to DDLs were short-sighted w.r.t. DL quantification. If in DDLs with quantification a defeasible subsumption relationship holds between concepts, this relationship can also hold if these concepts appear in existential (or value) restrictions. Such nested defeasible subsumption relationships were not detected by earlier reasoning algorithms - neither for rational nor relevant closure.
In the first part I will present recent results resolving this problem for rational reasoning in defeasible EL⊥. Our construction uses typicality models that extend classical canonical models by domain elements that individually satisfy different amounts of consistent defeasible knowledge. In the second part I will present a generalisation of the typicality model approach that allows us to obtain the stronger relevant closure without the mentioned issue.
This session will be the rehearsal of a short conference talk and a (medium) workshop talk.
Stefano Bistarelli: Semiring-based constraint solving and argumentation
In the talk we will recall some basic notions of classical Constraint Satisfaction Problems (CSPs) and Argumentation Frameworks (AFs). Then the semiring structure is introduced to order to deal with over-constrained problems, preferences, and fuzziness in both CSPs and AFs. Soft CSPs and Soft AFs are introduced and solution and semantics discussed in a new frameworks. In particular, we will analyze Arc consistency for semiring-based CSPs and both strong and relaxed version of weighted defense for semiring-based AFs. Finally a web-based tool for solving argumentation problem using CSPs is presented.
Shima Asaadi: Gradual Learning of Matrix-Space Models of Language for Sentiment Analysis
Learning word representations to capture the semantics and compositionality of language has received much research interest in natural language processing. Beyond the popular vector space models, matrix representations for words have been proposed, since then, matrix multiplication can serve as natural composition operation. In this talk, we investigate the problem of learning matrix representations of words. We present a learning approach for compositional matrix-space models for the task of sentiment analysis. We show that our approach, which learns the matrices gradually in two steps, outperforms other approaches and a gradient-descent baseline in terms of quality and computational cost.
Lukas Schweizer: Not too Big, Not too Small...Complexities of Fixed-Domain Reasoning in First-Order and Description Logics
We consider reasoning problems in description logics and variants of first-order logic under the fixed-domain semantics, where the model size is finite and explicitly given. It follows from previous results that standard reasoning is NP-complete for a very wide range of logics, if the domain size is given in unary encoding. In this paper, we complete the complexity overview for unary encoding and investigate the effects of binary encoding with partially surprising results. Most notably, fixed-domain standard reasoning becomes NEXPTime for the rather low-level description logics ELI and ELF (as opposed to EXPTime when no domain size is given). On the other hand, fixed-domain reasoning remains NEXPTime even for first-order logic, which is undecidable under the unconstrained semantics. For less expressive logics, we establish a generic criterion ensuring NP-completeness of fixed-domain reasoning. Amongst other logics, this criterion captures all the tractable profiles of OWL 2.
Emmanuelle Dietz: From Logic Programming to Human Reasoning
This talk will be the rehearsal of a PhD defense.
Victor Lagerqvist: Constraint satisfaction problems, algebra and kernelization
A kernelization algorithm for a computational problem is a procedure which compresses an instance into an equivalent instance whose size is bounded with respect to a complexity parameter. For the constraint satisfaction problem (CSP), there exist many results concerning upper and lower bounds for kernelizability of specific problems, but it is safe to say that we lack general methods to determine whether a given problem admits a kernel of a particular size. In this seminar we will look at algebraic techniques to the problem of characterizing the kernelization limits of NP-hard CSP problems. We will see that a finite-domain CSP problem has a kernel with a linear number of constraints if it can be embedded (via a domain extension) into a CSP which is preserved by a Maltsev operation. In the complementary direction, we give indication that this condition might be a complete characterization for Boolean CSPs with linear kernels, by showing that an algebraic condition that is shared by all problems with a Maltsev embedding is also necessary for the existence of a linear kernel, unless the polynomial-time hierarchy collapses.
Marco Kuhlmann: On the Complexity of CCG Parsing
We study the parsing complexity of Combinatory Categorial Grammar (CCG) in the formalism of Vijay-Shanker and Weir (1994). As our main result, we prove that any parsing algorithm for this formalism will necessarily take exponential time when the size of the grammar, and not only the length of the input sentence, is included in the analysis. This result sets the formalism of Vijay-Shanker and Weir (1994) apart from weakly equivalent formalisms such as Tree-Adjoining Grammar (TAG), for which parsing can be performed in time polynomial in the combined size of grammar and input sentence. Our proof highlights important differences between the formalism of Vijay-Shanker and Weir (1994) and contemporary incarnations of CCG.
Tobias Heindel: From Stochastic Graph Transformation to Quantitative Transduction of Circuit Diagrams
Domain specific graph transformation systems (GTS) for bio-chemical modeling and analysis of the corresponding continuous-time Markov chains (CTMC) is an active research field. Graphs are used to model possible states (i.e., multi-sets of structured molecules) and local rules describe the interaction of reactive groups of molecules, which suffices to specify the global stochastic behavior. Numerical integration of the time evolution of virtually all models of practical relevance is possible, but notoriously costly; for general GTSs, there are even open problems concerning the computable analysis of the underlying CTMCs. Only a quick overview of results, work in progress, and the relation to verification of CTMCs will fit the allotted time.
Besides the common use of graphs as abstraction of system states, graphs can function as syntax, very much like terms over a signature—a point of view that has proven successful in the study of quantum systems, relying on circuit diagrams as syntax. As both graphs and circuit diagrams can be seen as elements of generalized monoids, it is only natural to study transduction and related topics of formal language theory. A first example is transduction of directed acyclic graphs to a flow relation, which already contains all ingredients for weighted transducers of graph-like structures, thus opening a promising research direction of quantitative automata theory for generalized monoids.
Viktor Kunčak: Reasoning about Multisets and their Sizes
I will describe an algorithm for deciding satisfiability of constraints that involve sets and their cardinalities. Our first result is membership in NP for the satisfiability problem of quantifier-free constraints involving set algebra operations and integer linear arithmetic on cardinalities of sets. The result relies on an integer generalization of the Caratheodory theorem. I will show that, using bounds on semilinear sets for quantifier-free Presburger arithmetic, the result also generalizes to quantifier-free constraints on multisets, where elements can repeat. The algorithms can be extended to also support fractional measures. For finite sets of integers, it is possible to also permit min and max operations. Finally, the algorithms can also be incorporated into SMT solvers.
The talk is based primarily on the joint work with Ruzica Piska.
Main references:
[1] http://lara.epfl.ch/~kuncak/papers/KuncakRinard07TowardsEfficientSatisfiabilityCheckingBoolean.html
[2] http://lara.epfl.ch/~kuncak/papers/PiskacKuncak08LinearArithmeticwithStars.html
Additional references:
[3] http://lara.epfl.ch/~kuncak/papers/KuncakETAL10OrderedSetsinCalculusofDataStructures.html
[4] http://lara.epfl.ch/~kuncak/papers/SuterETAL11SetswithCardinalityConstraintsin.html
