The fifth QuantLA workshop takes place from 18th to 22nd of September 2017 at the Hotel zum Bären in Altenberg, near the Czech border. This years guest lecturers are Thomas Schwentick from TU Dortmund and Thomas Eiter from TU Wien.
Travelling
The following two options describe the journey from Dresden to the Hotel as it is necessary to go through Dresden in any case. It is also an option to meet at Dresden Hauptbahnhof in small or large groups at a certain time in order to take the remaining trip together.
The closest station to the Hotel zum Bären is called Oberbärenburg and can be reached by the Bus 360 (may change numbers along the route, most of the time changing the bus is not required, check the links to the trip advisors for more detail) from Dresden Hauptbahnhof. The bus leaves almost hourly, for the schedule check either https://www.dvb.de/en-gb/ or https://www.bahn.com/en/view/index.shtml (departure and destination also accept an address). This trip takes around 1 - 1.5h depending on the stops the bus makes.
For an alternative (less recommended unless you really prefer trains) route you can go from Dresden to Heidenau (with the Train S1) and from Heidenau to Altenberg with the Städtebahn Sachsen. However, the station in Altenberg that you will arrive at is about 6km from the hotel. You can take the Bus 370 from Bahnhof Altenberg to the station Oberbärenburg. Incidentally, this is the same bus that departs from Dresden Hauptbahnhof and overall the train trip takes around the same time as the bus from Dresden. For specific schedules and connections use the links provided above.
In either case, it is a nice 9-10 minute walk from the final bus station to the Hotel zum Bären.
Social event
The social event of the workshop will take place on Wednesday afternoon (20 September 2017).There are 2 options to choose from.
Option 1: Summer toboggan run [1], this should be fun for anyone who does not feel fully grown up.
Option 2: Bergbaumuseum Altenberg [2], take a tour to learn something about the history of mining in Altenberg. Unfortunately, they only provide guided tours in German.
No matter which option you choose, we will walk to Altenberg together, and go back to Oberbärenburg by bus where we will have dinner at 19.00 as usual.
[1] http://www.sommerrodelbahn-altenberg.de
[2] http://bergbaumuseum-altenberg.de/engl.htm
Time Table
Course Programme
Caterina Viola: Submodular Semilinear Valued Constraint Satisfaction Problems
Valued CSPs (VCSPs) are an extension of CSPs capturing optimisation problems. The complexity of finite valued CSPs over finite domains was fully characterised by Thapper and Živný, in 2013. In particular, these VCSPs are either polynomial-time solvable or NP-hard. Submodular semilinear VCSPs are an interesting class of VCSPs over infinite domains. After presenting our achievements in characterising submodular semilinear functions syntactically, we will show an algorithm solving in polynomial-time the VCSP for binary functions f: ℚ2→ ℚ that are first-order definable over (ℚ;<,1,(αc)c ∈ ℚ), where αc denotes x↦ cx. We will conclude presenting a condition of NP-hardness for semilinear VCSPs.
Johannes Greiner: Free combinations of omega-categorical structures
In order to analyze the tractability of constraint satisfaction problems of omega-categorical structures, we introduce the notion of a free combination. The new notion describes a combination of the constraint satisfaction problem over a structure A with the constraint satisfaction problem over a structure B. In this talk, we provide a necessary and sufficient condition for the existence of a free combination of two omega-categorical structures and present a new classification result using the notion. Furthermore, we will give important properties of free combinations, show examples and connect to the status of last year.
Lisa Hutschenreiter: Parametric Markov Chains: PCTL Complexity and Fraction-free Gaussian Elimination
Parametric Markov chains have been introduced to model families of stochastic systems that rely on the same graph structure, but whose transition probabilities are specified by polynomial constraints. Among the tasks typically addressed in the analysis of parametric Markov chains are the computation of closed-form solutions for reachabilty probabilities and other quantitative measures. I will show that existing implementations for computing rational functions for reachability probabilities or expected costs in parametric Markov chains can be improved by using fraction-free Gaussian elimination. Furthermore, I will present a complexity-theoretic discussion of the model checking problem for parametric Markov chains and probabilistic computation tree logic (PCTL) formulas. This is joint work with Christel Baier and Joachim Klein.
Linda Leuschner: Quantitative Analysis of Redo-Based Fault-Tolerance Mechanisms
Ensuring a certain level of fault tolerance is of growing interest in the field of error-prone systems. Randomly occurring bit-flips change the memory state of programs, leading to crashes or unforeseen behavior. During quantitative analysis of fault tolerance techniques, resilience measures like meantime-to-failure or probabilities of silent data corruption, together with computational overhead are addressed to determine the quality of a fault tolerance mechanism. Typically, this analysis is performed by running simulations, which, of course, can not guarantee a certain level of fault tolerance.
David Müller: LTL to Deterministic Emerson-Lei Automata
In 2015, a universal exchange format for ω-automata has been introduced: The Hanoi omega automata format. One interesting aspect is the new Emerson-Lei acceptance, a symbolic Muller condition, unifying Rabin, Streett and generalized versions of them. However, existing translations generate always automata for a specific acceptance condition.
We introduce a new translation from linear temporal logic (LTL) to deterministic Emerson-Lei automata. The richer acceptance condition allows the constructions to shift complexity from the state space to the acceptance condition. Conceptually the construction is an enhanced product construction that exploits knowledge of its components to reduce the number of states. We identify two fragments of LTL, for which one can easily construct deterministic automata and show how knowledge of these components can reduce the number of states in the product. We extend this idea to a general LTL framework, where we can use arbitrary LTL-to-deterministic-automata-translators for parts of formulas outside the mentioned fragments. Furthermore, we show succinctness of the translation compared to existing construction. At last, we compare the sizes of the automata generated by our implementation, called Delag, with established tools like SPOT or Rabinizer, as well as their behavior in benchmarks for probabilistic model checking, one important application for deterministic ω-automata.
Mathias Ruggaard Pedersen: Reasoning About Bounds In Weighted Transition Systems
We propose a way of reasoning about minimal and maximal values of the weights of transitions in a weighted transition system (WTS). This perspective induces a notion of bisimulation that is coarser than the classic bisimulation: it relates states that exhibit transitions to bisimulation classes with the weights within the same boundaries. We propose a customized modal logic that expresses these numeric boundaries for transition weights by means of particular modalities. We prove that our logic is invariant under the proposed notion of bisimulation. We show that the logic enjoys the finite model property which allows us to prove the decidability of satisfiability and provide an algorithm for satisfiability checking. Last but not least, we identify a complete axiomatization for this logic.
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.
Sven Dziadek: A Nivat Theorem for Weighted Omega-Pushdown Automata
Recently, weighted omega-pushdown automata have been introduced by Droste, Ésik, Kuich. This new type of automaton has access to a stack and models quantitative aspects of infinite words. We propose a different automaton model. As a first result, we prove a Nivat theorem for these automata. This theorem states that the behaviors of weighted omega-pushdown automata are precisely the projections of very simple omega-series restricted to omega-context-free languages.
Markus Ulbricht: Strong inconsistency in nonmonotonic reasoning
Minimal inconsistent subsets of knowledge bases play an important role in classical logics, for instance for diagnosis and repair. For nonmonotonic reasoning, this notion is not as useful as consistent knowledge bases may contain inconsistent subsets. We introduce a more appropriate 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 hitting set duality generalizes to arbitrary logics if the strong notion of inconsistency is used. We also hint at possible applications of this notion and investigate the computational complexity of related decision and function problems.
Gerd Brewka: Weighted Abstract Dialectical Frameworks
Abstract Dialectical Frameworks (ADFs) generalize Dung's argumentation frameworks allowing various relationships among arguments to be expressed in a systematic and flexible way. We further generalize ADFs so as to accommodate arbitrary acceptance degrees for the arguments. This makes the framework of ADFs applicable in domains where both the initial status of arguments and their relationship are only insufficiently specified by Boolean functions. We define all standard ADF semantics for the weighted case, including grounded, preferred and stable semantics. We illustrate our approach using acceptance degrees taken from the unit interval and then show how numerous other valuation structures can be integrated. In each case it is sufficient to specify how the generalized acceptance conditions are represented by formulas, and to specify the information ordering underlying the characteristic ADF operator. In addition, we introduce generalized partial interpretations which allow for better approximations in the application of that operator. We also present complexity results for several problems related to weighted ADFs.
Maximilian Pensel: Deciding Subsumption in Defeasible EL⊥ with Typicality Models and beyond
In many scenarios involving human cognition and the evolution of knowledge, classical monotone Description Logics (DLs) cannot provide intuitive reasoning results. To express presumptive knowledge and still obtain useful results in light of contradicting special cases requires nonmonotonic semantics. In defeasible DLs (DDLs), default assumptions can be modeled using defeasible implications, statements that can be disregarded to circumvent a contradiction. While there are several approaches investigating nonmonotonic semantics for DDLs, some of the most recent attempts are insufficient w.r.t. quantified concepts. As a result of the underlying construction in these approaches defeasible information is fully neglected for quantified concepts, and thus many expected entailments are missing.
Anni-Yasmin Turhan: Temporal Query Answering in DL-Lite over Inconsistent Data
In ontology-based systems that process data stemming from different sources and that is received over time, as in context-aware systems, reasoning needs to cope with the temporal dimension and should be resilient against inconsistencies in the data. Motivated by such settings, this talk addresses the problem of handling inconsistent data in a temporal version of ontology-based query answering. We consider a temporal query language that combines conjunctive queries with operators of propositional LTL and extend to this setting three inconsistency-tolerant semantics that have been introduced for querying inconsistent description logic knowledge bases. We investigate their complexity for DL-LiteR temporal knowledge bases.
This is joint work with Camille Bourgaux.
Pavlos Marantidis: Weighted tree automata for approximate description logics
Unification in Description Logics (DLs) is an inference service that can be used to detect redundancies in ontologies, by finding different concepts that may potentially stand for the same intuitive notion. Recently, approximate unification has been introduced to increase the recall of classical unification, by finding whether concepts evaluate to “almost” the same notion. The notion of “almost” is formalised by concept comparison measures (CCMs), functions that take as input two concepts and output a number (the “distance" or “similarity” of the concepts).
In this talk, I will show how weighted automata working on infinite trees can be used to construct computable CCMs for the DL FL0 that are equivalence invariant w.r.t. general TBoxes. This is a first step towards employing such measures also in approximation approaches that are being investigated for other DLs.
Franz Baader: What QFBAPA can do for Description Logics
Considered from an abstract point of view, Description Logics (DLs) allow their users to state inclusion constraints between concepts (i.e., sets) and to state cardinality constraints for concepts and role successors. The constraints that can be formulated in DLs are usually of a very restricted form. We show that, by using the quantifier-free fragment of Boolean Algebra with Presburger Arithmetic (QFBAPA) to formulate constraints on sets and their cardinalities, we can considerably extend the expressive power without increasing the complexity of reasoning.
Sebastian Rudolph: Decidability of Conjunctive Queries for Description Logics with Counting, Inverses and Nominals
Description Logics (DLs) are Knowledge Representation formalisms with a great significance for Semantic Web technologies. For instance, the ontology specification languages OWL DL and its successor OWL 2 DL, standardized by the World Wide Web Consortium (W3C), are based on DL languages. Conjunctive queries constitute the standard querying paradigm for data bases and have in recent years attracted increasing interest in the area of logic-based knowledge representation. While decidability and computational complexity are mainly clarified for standard DL reasoning tasks (such as knowledge base consistency or axiom entailment), decidability of conjunctive query answering in OWL DL and OWL 2 DL is still an open problem. Over a comparatively long time, a major obstacle towards the solution of this problem was the intricate interplay of three modeling features: nominal concepts, inverse roles and cardinality constraints. In my talk, I will present results that, for the first time, establish decidability of a DL containing all three constructs. For a slightly restricted class of conjunctive queries (i.e., queries with only simple roles), our result also shows decidability in the logics that underpin OWL DL and OWL 2 DL.
Thomas Eiter: LARS Stream Reasoning and Temporal Logic
In this talk, we revisit the LARS framework for logic-based reasoning on streams and contrast it with temporal logic. While there are commonalities between LARS and LTL resp. TEL (temporal equilibrium logic), respectively, there are yet differences which are discussed. Furthermore, bridging between the formalisms is explored.
Karin Quaas: The complexity of Flat Freeze LTL
We consider the model-checking problem for freeze LTL on one-counter automata (OCAs). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter values of a run in registers so that they can be compared with one another. As the model-checking problem is undecidable in general, we focus on the flat fragment of freeze LTL, in which the usage of the freeze quantifier is restricted. Recently, Lechner et al. showed that model checking for flat freeze LTL on OCAs with binary encoding of counter updates is decidable and in 2NEXPTIME. In this paper, we prove that the problem is, in fact, NEXPTIME-complete no matter whether counter updates are encoded in unary or binary. Like Lechner et al., we rely on a reduction to the reachability problem in OCAs with parameterized tests (OCAPs). The new aspect is that we simulate OCAPs by alternating two-way automata over words. This implies an exponential upper bound on the parameter values that we exploit towards an NP algorithm for reachability in OCAPs with unary updates. We obtain our main result as a corollary.
This is joint work with Benedikt Bollig and Arnaud Sangnier, presented at CONCUR 2017.
Erik Paul: Decidability Results for Max-Plus Tree Automata and Monitor Logics for Quantitative Monitor Automata
In this talk, I present two results I have obtained during the past year. First, I talk about the decidability of the equivalence, unambiguity and sequentiality problems for finitely ambiguous max-plus tree automata. Second, I introduce a new logic called Monitor Logic which is expressively equivalent to Quantitative Monitor Automata.
Thomas Schwentick: Dynamic Complexity: Recent & Complex Updates
In most real-life databases data changes frequently and thus makes efficient query answering challenging. Auxiliary data might help to avoid computing query answers from scratch all the time. One way to study this incremental maintenance scenario is from the perspective of dynamic algorithms with the goal to reduce (re-) computation time.
Another option is to investigate it from the perspective of low-level parallel computational complexity [1] or parallelizable database queries [2]. As the "lowest" complexity class AC0 (with a suitable unifomity condition) and the core of the standard database query language SQL both coincide with first-order predicate logic, one naturally arrives at the question which queries can be answered/maintained dynamically with first-order predicate logic (DynFO).
The talk gives an introduction into dynamic complexity and presents and discusses recent results about Reachability, complex update operations and MSO-queries on structures of bounded tree-width [3,4,5].
[1] Sushant Patnaik and Neil Immerman. Dyn-FO: A parallel, dynamic complexity class. J. Comput. Syst. Sci., 55(2):199--209, 1997.
[2] Guozhu Dong and Jianwen Su. Incremental and decremental evaluation of transitive closure by first-order queries. Inf. Comput., 120(1):101--106, 1995.
[3] Samir Datta, Raghav Kulkarni, Anish Mukherjee, Thomas Schwentick, Thomas Zeume: Reachability is in DynFO. ICALP 2015.
[4] Thomas Schwentick, Nils Vortmeier, Thomas Zeume: Dynamic Complexity under Definable Changes. ICDT 2017.
[5] Samir Datta, Anish Mukherjee, Thomas Schwentick, Nils Vortmeier, Thomas Zeume: A Strategy for Dynamic Programs: Start over and Muddle through. ICALP 2017.
Christel Baier: Stochastic path problems
Stochastic path problems are a class of optimization problems for probabilistic weighted structures where the task is to find a policy for traversing the graph such that the probability for some weight-bounded property or the expected weight is maximal or minimal. Several types of stochastic path problems are surprisingly difficult when the weights can be negative or positive. The talk presents known and a few recent results on selected stochastic path problems.
Shima Asaadi: Learning Sentiment-Aware Word Representation in Compositional Matrix-Space Models
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 for word representations, Compositional Matrix-Space Models (CMSM) have been proposed. In such models, matrices instead of vectors are used as word representations and compositionality is realized via matrix multiplication. It has been shown that compositional matrix-space models are an elegant way to model compositional aspects of the language. The question, however, how to learn suitable word-to-matrix mappings has remained largely unexplored with few exceptions.
In this work, we investigate the problem of learning matrix representations of words. We present a gradient-based learning approach for compositional matrix-space models for the task of fine-grained sentiment analysis. We show that our approach, which learns the word matrices gradually in two steps, outperforms other approaches in terms of quality and computational cost.
Heiko Vogler: Weighted Regular Tree Grammars with Storage
We introduce weighted regular tree grammars with storage as combination of (a) regular tree grammars with storage and (b) weighted tree automata over multioperator monoids. Each weighted regular tree grammar with storage generates a weighted tree language, which is a mapping from the set of trees to the multioperator monoid. We discuss a Büchi-Elgot-Trakhtenbrot result for this class of weighted tree languages.
This is joint work with Zoltan Fülöp and Luisa Herrmann.
Daniel Gburek: Parallel composition of stochastic transition systems based on couplings
Cyber-physical systems and the Internet of Things raise various challenges concerning the modelling and analysis of large modular systems. Models for such systems typically require continuous state spaces, stochastics, and non-deterministic choices over an uncountable number of alternatives. In this talk we focus on a generic formalism called stochastic transition system. We present a novel parallel-composition operator for stochastic transition systems that is based on couplings of probability measures. Couplings yield a declarative modelling paradigm appropriate for the formalisation of stochastic dependencies that are caused by the interaction of components. Congruence results for our operator with respect to standard notions for simulation and bisimulation are presented where the difficulty is to prove the existence of specific couplings.
Sascha Wunderlich: Towards Automated Variant Selection for Heterogeneous Tiled Architectures
Systems based on heterogeneous tiled architectures promise great potential for high performance energy-efficient computing. Their hardware integrates many processing elements with very different characteristics, which allows them to accelerate various instructions. Compilers can generate tailor-made code variants that uses these instructions to complete computing tasks very fast and efficiently. To exploit this potential, advantageous resource allocation and scheduling policies are needed to select software variants and map them to the processing elements. However, since the state-space spanned by all these variants and strategies is huge, it is difficult to find the optimum efficiently with classical approaches like simulation.
In this talk, we will show the general feasibility of using probabilistic model checking to help with this problem. We present a tool chain that provides flexible and comfortable ways to specify whole model families for heterogeneous systems. We apply our method to the heterogeneous multi-processor Tomahawk platform and show that family-based analysis enables comparative studies, which can provide feedback for the design of heterogeneous hardware components, the choice of software variants and the creation of adaptive resource management and scheduling strategies.
Manfred Droste: On operations preserving recognizability of languages and weighted languages
As is well-known, classical operations like union, intersection, product, Kleene star, homomorphic image and homomorphic preimage preserve the recognizability of languages and, under suitable side conditions, also of weighted languages. Less well-known examples are given by the square root and by amplifying images of languages. We will consider these operations for weighted languages and show the power of algebra for combinatorial constructions of weighted automata.
Andreas Maletti: Multiple Context-free Tree Grammars and Multi-Component Tree Adjoining Grammars
Strong lexicalization is the process of turning a grammar generating trees into an equivalent one, in which all rules contain a terminal leaf. It is known that tree adjoining grammars cannot be strongly lexicalized, whereas the more powerful simple context-free tree grammars can. It is demonstrated that multiple simple context-free tree grammars are as expressive as multi-component tree adjoining grammars and that both allow strong lexicalization.
(joint work with Joost Engelfriet and Sebastian Maneth)
Manuel Bodirsky: Monotone Monadic SNP 1: classical results and applications
The logic MMSNP is a restricted fragment of existential second-order logic which allows to express many interesting queries in graph theory, database theory, and finite model theory. The logic was introduced by Feder and Vardi who showed that every MMSNP sentence is polynomially equivalent to a finite-domain constraint satisfaction problem (CSP); the clever probabilistic reduction was derandomized by Kun using explicit constructions of expander structures. Several authors have recently announced proofs that every finite-domain CSP is either in P or NP-complete; hence, the same is true for MMSNP.
We present a new proof of the complexity dichotomy for MMSNP. Our new proof has the advantage that it confirms a tractability conjecture by Pinsker and myself that we have made for a much larger class of computational problems. Another advantage is that it does not rely on the intricate expander constructions of Kun (but we do use the finite domain CSP dichotomy). Our approach is based on the fact that every MMSNP sentence can be effectively rewritten into a finite union of CSPs for countably infinite omega-categorical structures; moreover, by a recent result of Hubicka and Nesetril, these structures can be expanded to homogeneous structures with finite relational signature and the Ramsey property. This allows us to use the universal-algebraic approach to study the computational complexity of MMSNP.
In this first part of the talk we will give an introduction to MMSNP with many examples and the classical results, including the Feder-Vardi reduction to finite-domain CSPs, but also usages of MMSNP to classify the complexity of problems that arose in the context of descriptions logics (by Bienvenu, ten Cate, Lutz, Wolter). In the second part, Antoine presents our new analysis of MMSNP sentences using the universal-algebraic approach and Ramsey theory.
Joint work with Antoine Mottet.
Antoine Mottet: Monotone Monadic SNP 2: proof of the universal-algebraic dichotomy conjecture
The forbidden patterns problem of the set of vertex-coloured graphs {H1,...,Hk} is the decision problem of the form: given a finite graph G as input, is it possible to colour the vertices of G in a way that none of H1,...,Hk homomorphically maps to the resulting coloured graph. The logic MMSNP can be seen as a complexity class whose problems are forbidden patterns problems of finite sets of coloured relational structures. It was conjectured by Feder and Vardi that this complexity class exhibits a complexity dichotomy (i.e., that every forbidden patterns problem is in P or NP-complete). Feder and Vardi showed that every problem in MMSNP reduces in probabilistic polynomial-time to the CSP of a structure with finite domain, and Kun later derandomized this reduction. Thus, MMSNP and finite-domain CSPs are computationally equivalent.
Following up on Manuel's talk, I will present a completely new reduction from MMSNP to finite-domain CSPs that uses recent techniques and results from universal algebra, model theory, and Ramsey theory. This proves a stronger form of the Feder-Vardi-Kun result, and shows in particular that the Bodirsky-Pinsker tractability conjecture holds for all CSPs in MMSNP.
Stefan Dück: Weighted Automata and Logics on Hierarchical Structures and Graphs
In this talk, I present the main results of my thesis. I apply semirings and valuation monoids to define, study, and characterize weighted automata and weighted logics which are able to read structures with hierarchical information, and weighted automata and weighted logics operating on graphs. In particular, I study infinite nested words, operator precedence languages (OPL), and finite and infinite graphs.
I study different, suitable fragments of a general weighted logic for relational structures and show a transformation result between them, which establishes a direct connection between the assumptions on our weight structure and the expressive power of the weighted MSO-logic over this weight structure. Furthermore, I show Büchi-like results connecting weighted automata and weighted MSO for the respective classes of weighted languages. As a consequence, I obtain Büchi-type equivalence results known from the recent literature for weighted automata and weighted logics on words, trees, pictures, and nested words.
