The fourth QuantLA workshop (first workshop for 2nd generation scholarship holders) takes place from 19th to 23th of September 2016 at the hotel Erbgericht in Krippen, Bad Schandau. This years guest lecturers are Joanna Ochremiak from Universitat Polytècnica de Catalunya and Christof Löding from RWTH Aachen. Please find the schedule below. The slides are now internally available here.
Time Table
Course Programme
Joanna Ochremiak: Computation in sets with atoms
Orbit-finite sets with atoms, although usually infinite, can be finitely described and are therefore amenable to algorithmic manipulation. In this talk I will present an overview of a research project which aims at generalising various models of computation and classical computational problems to the setting of sets with atoms.
Manuel Bodirsky: The tractability conjecture for reducts of finitely bounded homogeneous structures
Reducts of finitely bounded homogeneous structures form a large class of infinite structures that can be seen as a generalisation of the class of all finite structures. Many results about finite structures, in particular in the context of the complexity of constraint satisfaction problems, can be generalised to this larger class. In this talk I will present a reformulation of a tractability conjecture for CSPs for this class in terms of polymorphisms, due to Barto and Pinsker (LICS 2016), and I will present a proof that the condition given in the tractability conjecture is decidable (under some Ramsey-theoretic assumptions that might hold in general for all reducts of finitely bounded homogeneous structures).
Lisa Hutschenreiter: PCTL model checking on parameterized DTMCs
Probabilistic model checking is a rather successful method that has been developed for the quantitative analysis of systems. Within the last few years it has become popular to consider parameterized versions of Markovian models for specifying families of systems that have the same graph structure, but vary in the precise transition probabilities. Methods for computing closed form solutions in terms of rational functions for reachability probabilities and expected rewards in parametric Markov chains have been presented in the literature and implemented in tools. However, several problems are still open. This concerns the complexity-theoretic status of model-checking (and related parameter-synthesis) problems for parametric Markov chains. Another challenge is the treatment of nested probability constraints in branching-time temporal logics.
When considering the model checking problem for probabilistic computation tree logic on parameterized discrete-time Markov chains two main problems occur: The coefficient matrix and vector in the linear equation system that stems from the until operator can contain parameters, and nesting of the probability operator results in the need for a parameter-dependant case analysis. While there exist algorithms and implementations for the first problem, the second one is usually avoided by prohibiting nesting.
In this talk I will present an algorithm that improves on the current ones used for solving parametric linear equation systems. Combining this algorithm with another one known from the existential theory of the reals I will also present a first algorithm for model checking nested probabilistic computation tree logic on parameterized discrete-time Markov chains.
Christel Baier: How much does it cost to reach the target, assuming it will not be missed?
Stochastic path problems are optimization problems for weighted structures with nondeterministic and probabilistic transitions. The typical task is to find a policy for resolving the nondeterministic choices maximizing or minimizing the expectation of a random variable. Many variants of stochastic path problems have been studied in the literature, using Markov decision processes or two-player stochastic game structures and finite- or infinite-horizon objectives. The talk reports on recent work on the task to maximize the conditional expected total weight until reaching a set of goal states in a given Markov decision process. The condition might be a reachability constraint (e.g. reaching the set of goal states) or some co-safety property.
Antoine Mottet: Reasoning with discrete time
Temporal reasoning is an area of artificial intelligence concerned with techniques for reasoning about events occurring in time. Typical queries one might want to answer are the form “Does there exist a scheduling of tasks T1,…,Tn that satisfies C”, where C is a set of constraints imposing conditions about the order in which the tasks can be executed. Depending on the set of constraints allowed in C (called the constraint language), and on whether time is understood to be continuous or discrete, the complexity of the problem of answering these queries varies. When time is continuous, Bodirsky and Kára showed that for every constraint language the problem of answering queries is in P or NP-complete. In my talk, I will present a similar dichotomy result for discrete time.
Linda Leuschner: Taming Bit-Flips - Probabilistic Model Checking for Integrity Checking Protocols
In a world of ever-increasing bit-flip rates there is a higher chance of errors affecting a program's instruction- or data-flow. Integrity checker try to harden programs against bit-flips by adding redundancy and performing regular checks and repairs. Due to the variety in error detection and correction mechanisms, there is a high number of integrity checkers. For evaluating the quality of a new integrity checking protocol, simulation-based error injection techniques are the de-facto standard. Unfortunately these methods can neither give a guarantee on the quality of the checker nor can they serve for a more complex analysis, e.g., investigating side effects of integrity checker malfunctions.
In this talk we present probabilistic model checking as a mathematically precise evaluation method for integrity checking protocols. The talk introduces a model covering a very wide range of integrity checking protocols and shows evalutional results of standard and complex performance measures. Furthermore, we report on problems and solutions arising when using probabilistic model checking in the real world.
Sascha Wunderlich: Greener Bits - Formal Analysis of Demand Response
Demand response is a promising approach to deal with the emerging power generation fluctuations introduced by the increasing amount of renewable energy sources fed into the grid. Consumers need to be able to adapt their energy consumption with respect to the given demand pattern and at the same time ensure that their adaptation (i.e., response) does not interfere with their various operational objectives. Finding, evaluating and verifying adaptation strategies which aim to be optimal w.r.t. multiple criteria is a challenging task and is currently mainly addressed by hand, heuristics or guided simulation.
In this talk we present a case study of a demand response system with an energy adaptive data center on the consumer side. We propose a formal model and identify significant properties and measures (e.g., expected energy consumption, average workload or total penalty for SLA violations) relevant to an adaptive consumer. Finally, we report on the experimental results of a quantitative system analysis carried out via probabilistic model checking.
David Müller: Deciding Probabilistic Emptiness for Deterministic Muller Automata with Generic Acceptance
Recently, a universal exchange format for ω-automata has been introduced: The Hanoi omega automata format. One interesting aspect is the new generic acceptance condition, a symbolic Muller condition, unifying Rabin, Streett and generalized versions of them.
Deterministic Muller automata with generic acceptance condition can be generated naturally by a product construction. In this talk we present how those automata fit into probabilistic model checking. Deciding positive probability for Markov chains can be done in P, whereas deciding whether the maximal probability is positive is NP-complete for Markov decision processes (MDP). Finally, we exploit the similarities between SAT solving and deciding positive probability in the MDP case, yielding a DPLL-based algorithm.
Christof Löding: Logic and Automata for Boundedness Problems
We consider logics and automata for expressing and verifying boundedness problems. As an illustration, consider (possibly infinite) transition systems in which the transitions can be annotated with actions for consuming one unit of a resource, or replenishing the stock of a resource. For given sets of initial and target vertices, a typical boundedness question would be whether there is a bound K for the size of the resource stock such that from each initial vertex it is possible to reach a target vertex without running out of resources. In this talk I will mainly focus on an extension of automatic structures and first-order logics for modelling and expressing such boundedness properties.
Heiko Vogler: EM-Training for Probabilistic Aligned Hypergraph Bimorphisms
We develop the concept of weighted aligned hypergraph bimorphism where the weights may, in particular, represent probabilities. Such a bimorphism consists of an weighted regular tree grammar, two hypergraph algebras that interpret the generated trees, and a family of alignments between the two interpretations. Semantically, this yields a set of bihypergraphs each consisting of two hypergraphs and an explicit alignment between them; e.g., discontinuous phrase structures and non-projective dependency structures are bihypergraphs. We present an EM-training algorithm which takes a corpus of bihypergraphs and an aligned hypergraph bimorphism as input and generates a sequence of weight assignments which converges to a local maximum or saddle point of the likelihood function of the corpus.
Stefan Dück: Weighted Automata and Logics for Operator Precedence Languages
In this talk, after presenting a short overview over my results on graphs, I will present recent work in the field of automata and logics for operator precedence languages (OPL) and weighted extensions thereof. Floyd introduced operator precedence grammars some time ago to define a powerful and practical subclass of deterministic context-free languages. In the last years, they found renewed interest thanks to desirable properties like local parsability and closure under boolean operations, i.e., they are closed under determinization.
After Alur and Madhusudan presented their flourishing theory of visibly pushdown languages (VPL) and nested words, it was only noted recently that VPL are indeed a strict subclass of OPLs. After this realization a complete theory of OPLs including an equivalent automata model and a characterization in terms of an MSO-logic was devised.
I will present ongoing work in generalizing results of this field to the weighted setting. In particular, we proved a weighted extension of a Büchi-like result for OPLs. This is joint work with Manfred Droste, Dino Mandrioli, and Matteo Pradella.
Johannes Greiner: Free combinations of countably-categorical structures
We provide two sufficient conditions for the tractability of the free combination of two constraint satisfaction problems. The first one is a version of Nelson and Oppens seminal result in terms of polymorphisms. The second one is an asymmetric criterion based on polymorphisms and automorphisms of the two structures respectively. Examples illustrating the results and open research questions will be included.
Caterina Viola: Valued Semi-Linear Constraints Satisfaction Problems
A Valued Constraint Satisfaction Problem (VCSP) is the computational problem of finding assignments to variables in a domain such that the sum of some given cost functions, specifying the constraints, evaluated at the values assigned to the variables is minimised. A semilinear VCSP is a VCSP where the underlying domain is ℚ, the set of rational numbers, and all the constraints are semilinear cost functions from ℚn → ℚ, that is, first-order definable over (ℚ; ≤, +, 1). Some results for finite domain VCSPs can be generalized for semilinear VCSPs. For semilinear VCSPs where the constraints are specified by only convex cost functions there is a polynomial-time minimisation algorithm as well as for VCSPs where the constraints are specified by only unary cost functions. Submodular cost functions are functions f : ℚn → ℚ such that for every x, y ∈ ℚn, f(x) + f(y) ≥ f(max(x, y)) + f(min(x, y)). We present a polynomial-time algorithm that solves restricted classes of semilinear submodular cost functions: unary functions, maximum of non-decreasing functions and binary functions that are minimum of a non-decreasing function and a non-increasing one. We also show why the characterisation of NP-hardness for VCSPs over finite domains does not apply to infinite-domain VCSPs. Finally, we will talk about the ongoing work to formulate a condition to characterise the hardness of semilinear VCSPs.
Johannes Osterholzer: Linear Context-Free Tree Languages and Inverse Homomorphisms
In this talk, I demonstrate why the class of linear context-free tree languages is not closed under inverse linear tree homomorphisms. The proof works by encoding Dyck words into a linear context-free tree language and showing that its preimage under a certain linear tree homomorphism cannot be generated by any context-free tree grammar. There is also a positive result: the linear monadic context-free tree languages are indeed closed under inverse linear tree homomorphisms.
Doreen Heusel: Weighted Tree Automata over Valuation Monoids
The topic of this talk are weighted automata which model quantitative aspects of systems like the average consumption of resources. In particular, we investigate the support of these weighted automata, i.e., the language of all words which are evaluated to a non-zero value. We will consider the support of several weighed automata models over different structures like words and trees. As weight structure we will resort to valuation monoids which enable us to cope with average and which form a very general class of weight structures including semirings. Moreover, we present a new class of weighted unranked tree automata over valuation monoids and give a logical characterization for them. These new weighted unranked tree automata are expressively equivalent to a weighted MSO logic for trees, this solves an open problem of Droste and Vogler. Finally we present a Kleene-type result for weighted ranked tree automata over valuation monoids.
Atefeh Babari: +ω-Picture Languages Recognizable by Büchi-Tiling Systems
In this paper we consider +ω-pictures, i.e., 2-dimensional pictures with a finite number of rows and an infinite number of columns. We extend conventional tiling systems with a Büchi acceptance condition and define the class of Büchi-tiling recognizable +ω-picture languages. We show that this class has the same closure properties as the class of tiling recognizable languages of finite pictures. We characterize the class of Büchi-tiling recognizable +ω-picture languages by generalized Büchi-tiling systems and by the logic EMSO∞, an extension of existential monadic second-order logic with quantification of infinite sets. The Büchi characterization theorem (stating that the ω-regular languages are finite unions of languages of the form L1 · L2ω, for regular languages L1 and L2), however, does not carry over from regular ω-languages to Büchi-tiling recognizable languages of +ω-pictures.
Erik Paul: A Feferman-Vaught Decomposition Theorem for Weighted MSO Logic
We investigate a weighted extension of the Feverman-Vaught Theorem. The classical Feferman-Vaught Theorem explains how to compute the truth value of a formula in a product or disjoint union of logical structures by reducing this computation to the computation of truth values of formulas in the corresponding factors. For the weighted extension, we consider a weighted logic similar to the one introduced by Droste and Gastin to describe weighted word automata. This is joint work with Manfred Droste and Vitaly Perevoshchikov.
Manfred Droste: Weighted linear dynamic logic
Giuseppe De Giacomo and Moshe Vardi introduced in 2013 a combination of propositional dynamic logic and LTL, called linear dynamic logic, which successfully combines the complexity properties of LTL and the expressive power of finite automata. We present results, from recent joint work with George Rahonis (GandALF 2016), on quantitative linear dynamic logic.
Luisa Herrmann: Weighted Automata with Storage
We investigate weighted automata with storage regarding particular closure properties and provide homomorphic and logical characterizations for the accepted classes of languages. We extend this automaton model to the case of an infinite input alphabet and show that this extension is powerful enough to capture symbolic visibly pushdown automata and weighted timed automata. Moreover, we provide an outlook for the further extension of our automata to the tree case and associated issues.
Pavlos Marantidis: Approximate Unification in the Description Logic FL0
Unification in description logics (DLs) has been introduced as a novel inference service that can be used to detect redundancies in ontologies, by finding different concepts that may potentially stand for the same intuitive notion. It was first investigated in detail for the DL FL0, where unification can be reduced to solving certain language equations. In order to increase the recall of this method for finding redundancies, we introduce and investigate the notion of approximate unification, which basically finds pairs of concepts that “almost” unify. The meaning of “almost” is formalized using distance measures between concepts. We show that approximate unification in FL0 can be reduced to approximately solving language equations, and devise algorithms for solving the latter problem for two particular distance measures.
Karin Quaas: Synchronizing Data Words for Register Automata
Register automata (RAs) are finite automata extended with a finite set of registers to store and compare data. We study the concept of synchronizing data words in RAs: Does there exist a data word that sends all states of the RA to a single state? For deterministic RAs with k registers (k-DRAs), we prove that inputting data words with 2k +1 distinct data, from the infinite data domain, is sufficient to synchronize. We show that the synchronizing problem for DRAs is in general PSPACE-complete, and it is NLOGSPACE-complete for 1-DRAs. For nondeterministic RAs (NRAs), we show that Ackermann(n) distinct data (where n is the size of RA) might be necessary to synchronize. The synchronizing problem for NRAs is in general undecidable, however, we establish Ackermann-completeness of the problem for 1-NRAs. Our most substantial achievement is proving NEXPTIME-completeness of the length-bounded synchronizing problem in NRAs (length encoded in binary). A variant of this last construction allows to prove that the bounded universality problem in NRAs is co-NEXPTIME-complete.
Maximilian Pensel: On the Development of Rational Nonmonotonic Reasoning in Description Logics
We use description logics (DL) in the field of knowledge representation and reasoning for its intuitive syntax and semantics as well as computational properties. DLs allow us to describe circumstances and relations within real world applications using concepts and roles and specifying axiomatic relations between them. In many scenarios however it is not sufficient to reason in a classical monotone way, especially when dealing with default assumptions which can potentially lead to inconsistent knowledge. There are many approaches to incorporate nonmonotonic reasoning into the formalism of description logics. Our focus so far lay in the investigation of existing approaches to utilize preferential semantics for DL and its stronger refinements, rational and relevant closure, as introduced by Kraus, Lehmann and Magidor for propositional logic. A discovered mismatch in the resulting inferences between the approaches by Casini and Giordano gives need to identify the source of this mismatch and finally form a well-defined formal semantics performing the appropriate rational reasoning in the DL setting. In this talk I will present an introduction and thorough overview of the current status of this endeavour.
Franz Baader: On cold coffee and syntactic sugar
That would give the meaning of the title away, so please come to the talk for more information.
Shima Asaadi: Automatic Extraction of Matrix-based Models of Language
In Natural Language Processing (NLP) there are different approaches for meaning representation of complex text structures, such as Vector Space Models (VSMs). A recently proposed approach which is an alternative to VSMs is Compositional Matrix Space Models (CMSMs). CMSMs are an elegant way to model compositional and distributional aspects of the language. These models employ matrices instead of vectors and make use of iterated matrix multiplication as the only composition operation. However, in practical cases, we require to automatically extract these models for NLP tasks. Therefore, methods for training such models should be developed e.g. by leveraging appropriate machine learning algorithms. For this purpose, we define a “graded matrix grammar” for CMSMs and we focus on grammar induction. Recently, Weighted Finite Automata (WFA) have received considerable research attention in NLP tasks. Herein, inspired by the definition of WFA and their wide applications in NLP, we show that there is a tight correspondence between CMSMs and WFA. Hence, we argue that the problem of learning CMSMs or the graded matrix grammar induction can be encoded as the prob- lem of learning a weighted automaton. Learning minimal WFA closely estimating rational power series, being an NP-hard problem, we are concerned with the best approximated solution using efficient algorithms.
Lukas Schweizer: Fixed-Domain Reasoning for Description Logics
After decades of fruitful research, description logics (DLs) have evolved into a de facto standard in logic-based knowledge representation. In particular, they serve as the formal basis of the standardized and very popular web ontology language (OWL), which also comes with the advantage of readily available user-friendly modeling tools and optimized reasoning engines. In the course of the wide-spread adoption of OWL and DLs, situations have been observed where logically less skilled practitioners are (ab)using these formalisms as constraint languages adopting a closed-world assumption, contrary to the open-world semantics imposed by the classical definitions and the standards. To provide a clear theoretical basis and inferencing support for this often practically reasonable "off-label use" we propose an alternative formal semantics reflecting the intuitive understanding of such scenarios. To that end, we introduce the fixed-domain semantics and argue that this semantics gives rise to an interesting new inferencing task: model enumeration. We describe how the new semantics can be axiomatized in very expressive DLs. We thoroughly investigate the complexities for standard reasoning as well as query answering under the fixed-domain semantics for a wide range of DLs. Further, we present an implementation of a fixed-domain DL reasoner based on a translation into answer set programming (ASP) which is competitive with alternative approaches for standard reasoning tasks and provides the added functionality of model enumeration.
Sebastian Rudolph: The Curse of Finiteness: Undecidability of Database-Inspired Reasoning Problems in Very Expressive Description Logics
Recently, the field of knowledge representation is drawing a lot of inspiration from database theory. In particular, in the area of description logics and ontology languages, interest has shifted from satisfiability checking to query answering, with various query notions adopted from databases, like (unions of) conjunctive queries or different kinds of path queries. Likewise, the finite model semantics is being established as a viable and interesting alternative to the traditional semantics based on unrestricted models. In this talk, we discuss diverse database-inspired reasoning problems for very expressive description logics (all featuring the worrisome triad of inverses, counting, and nominals) which have in common that role paths of unbounded length can be described (in the knowledge base or the query), leading to a certain non-locality of the reasoning problem. We show that for all the cases considered, undecidability can be established by very similar means. Most notably, we show undecidability of finite entailment of unions of conjunctive queries for a fragment of SHOIQ (the logic underlying the OWL DL ontology language), and undecidability of finite entailment of conjunctive queries for a fragment of SROIQ (the logical basis of the more recent and popular OWL 2 DL standard).
Anni-Yasmin Turhan: Answering Fuzzy Conjunctive Queries over Finitely Valued Fuzzy Ontologies
Fuzzy Description Logics allow to state that an object belongs to a concept with particular membership degree from the unit interval. Even for inexpressive DLs reasoning w.r.t.\ general TBoxes becomes undecidable. If one permits only finite sets of membership degrees, decidability can be regained and reasoning can be performed by a reduction to the classical case. We present a method to answer fuzzy conjunctive queries in this setting for the DL ALC that avoids the notorious exponential blow-up of the classical TBox.
Markus Ulbricht: Measuring Inconsistency in Answer Set Programs
We address the issue of quantitatively assessing the severity of inconsistencies in logic programs under the answer set semantics. While measuring inconsistency in classical logics has been investigated for some time now, taking the non-monotonicity of answer set semantics into account brings new challenges that have to be addressed by reasonable accounts of inconsistency measures. In this talk, we give an overview on existing approaches for the classical setting and our ongoing research on how we adapt them for answer set programming, in particular considering non-monotonicity.
Gerd Brewka: A Semantical Framework for Graph-based Argumentation
People often use graphs of various kinds to represent argumentation or decision making scenarios. In the talk we address the following question: is it possible to provide arbitrary (edge) labelled graphs with a well-defined model-theoretic semantics such that the graphs cannot only be used for visualization purposes, but also for automatic evaluation? We present a method that does exactly this. It is based on the definition of explicit acceptance conditions for nodes. These conditions are defined in terms of the multisets of labels of active links pointing to a node, where a link is active whenever its source node is considered true. This allows us to define the concept of a model of a graph and to generalize various notions Dung defined for his prominent argumentation frameworks.
