The seventh QuantLA workshop (first workshop for 3rd generation scholarship holders) takes place October 7–11, 2019 at Burghotel Stolpen in Stolpen, Sachsen.
The hotel is reachable via bus from Dresden Hauptbahnhof: Bus line 261 in the direction of Neustadt / Sebnitz stops at Stolpen Ärztehaus from where it is a five minute walk to the hotel. The bus ride takes around 50 minutes.
Time Table
| Monday, Oct 7 | Tuesday, Oct 8 | Wednesday, Oct 9 | Thursday, Oct 10 | Friday, Oct 11 | |
| Session Chair | Manuel Bodirsky | Andreas Maletti | Anni-Yasmin Turhan | Karin Quaas | Sebastian Rudolph |
| 08:30 - 09:00 | Opening | ||||
| 09:00 - 10:00 |
Achim Blumensath |
Helmut Seidl Deciding Equivalence of Tree Transducers by Means of Precise Abstract Interpretation |
Gustav Grabolle |
Kevin Stier Pumping lemmas for weighted tree automata |
Frederic Dörband Rational Weighted Tree Languages with Storage |
| 10:00 - 10:30 | Coffee break | ||||
| Session Chair | Shima Asaadi | Erik Paul | Thomas Feller | Florian Starke | Danny Richter |
| 10:30 - 11:30 |
Sven Dziadek Greibach Normal Form and Simple Automata for Weighted ω-Context-Free Languages |
Luisa Herrmann |
Jakub Rydval |
Willi Hieke |
Filippo De Bortoli On the characterization of cardinality constraints in Description Logics |
| 11:30 - 12:00 |
Manfred Droste |
Heiko Vogler A Büchi-Elgot-Trakhtenbrot theorem for automata with MSO graph storage |
Franz Baader The Complexity of the Consistency Problem in a Probabilistic Description Logic with Aggregation Semantics |
Anni-Yasmin Turhan Ontology-mediated Probabilistic Model Checking |
Feedback & Farewell |
| 12:00 - 14:00 | Lunch break | ||||
| Session Chair | Lukas Schweizer | Christian Alrabbaa | Excursion | Caterina Viola | |
| 14:00 - 15:00 |
Jakob Piribauer |
Simon Knäuer Relation Algebras and CSPs |
Lena Schiffer Combinatory Categorial Grammars as Acceptors of Tree Languages |
||
| 15:00 - 15:30 |
Christel Baier |
Manuel Bordirsky |
Andreas Maletti |
||
| 15:30 - 16:00 | Coffee break | Coffee break | |||
| Session Chair | Franz Baader | Gerhard Brewka | Heiko Vogler | ||
| 16:00 - 16:30 |
Sebastian Rudolph |
Karin Quaas |
Gerhard Brewka Revisiting the Foundations of Abstract Argumentation: Semantics Based on Weak Admissibility and Weak Defense |
||
| 16:30 - 17:00 |
Erik Paul |
Thomas Feller Towards Decidability for Knowledge Representations by Model-Theoretic means |
Caterina Viola The power of linear programming for infinite-domain valued constraint satisfaction problems |
||
| 17:00 - 17:30 |
Shima Asaadi Automatic Extraction of Compositional Matrix-Space Models in Natural Language Processing |
Lukas Schweizer SPARQL Queries over Ontologies Under the Fixed-Domain Semantics |
Florian Starke Smooth digraphs modulo pp-constructability |
||
| 17:30 - 18:00 |
Danny Richter |
Christian Alrabbaa Explications of Description Logic reasoning |
Johannes Greiner Generic Combinations of Temporal Structures and Bloated Finite Structures |
||
Abstracts
Achim Blumensath: Regular Tree Algebras
I present recent developments concerning a very general algebraic theory for languages of infinite trees which is based on the category-theoretical notion of a monad. The main result isolates a class of algebras that precisely captures the notion of regularity for such languages. In particular, we show that these algebras form a pseudo-variety and that syntactic algebras exists.
Sven Dziadek: Greibach Normal Form and Simple Automata for Weighted ω-Context-Free Languages
TBA
Manfred Droste: Weighted automata and logics on graphs
Weighted automata model quantitative features of the behavior of systemsnand have been investigated for various structures like words, trees, traces, pictures, and nested words. In this talk, we present a general model of weighted automata acting on graphs, which form a quantitative version of Thomas' unweighted model of graph acceptors. We show that a suitable weighted MSO logic is expressively equivalent to weighted graph automata. As a consequence, we obtain corresponding Büchi-type equivalence results known from recent literature for weighted automata and weighted logics on words, trees, pictures, and nested words. Establishing such a general result has been an open problem for weighted logic for some time.
(Joint work with Stefan Dück.)
Jakob Piribauer: Variants of Stochastic Shortest Path Problems
In formal verification of probabilistic systems, we often deal with systems exhibiting non-deterministic and probabilistic behavior. Stochastic shortest path problems play an important role when analyzing quantitative aspects of such systems. For example, the worst-case expected termination time of a probabilistic program is the maximal expected termination time among all possible resolutions of the non-deterministic behavior. A stochastic shortest path problem precisely asks for the optimal resolution of non-deterministic choices to minimize or maximize the expected value of accumulated weight (e.g., time) before reaching some goal.
In this talk, we investigate variants of stochastic shortest path problems, in which the requirement to reach the goal almost surely is dropped. Formulated using Markov decision processes, one of the most prominent classes of models combining non-deterministic and probabilistic behavior, the main results are the following.
When restricting the weights to non-negative integers, the optimal values in the problems under consideration are computable in exponential time.
For arbitrary integer weights, on the other hand, the Skolem problem (Does a given linear recurrence sequence ever become 0?) is reducible to the problem of deciding whether the optimal value exceeds a threshold. This implies that a computation procedure for the optimal value or a decision procedure for the threshold problem of these variants of stochastic shortest path problems would settle the decidability of the Skolem problem which has been open for many decades.
Christel Baier: Probabilistic bisimulation with silent moves
Formal notions of bisimulation relations are a key concept of concurrency theory to equate, respectively distinguish processes according to the behaviour they exhibit when interacting with other processes, taking the stepwise behaviour of processes as a reference. Speaking roughly, bisimar processes can mutually simulate each other by mimicking their visible stepwise behaviour. While notions of strong bisimilarity rely on the assumption that all transitions are visible, a variety of weaker notions of bisimilarity have been proposed that abstract away from internal computations ("silent moves'' in the jargon of van Glabbeek). Analogous notions have been introduced for probabilistic automata and related models that share the idea that probabilistically bisimilar processes induce the same distributions over visible steps, and thus have the same observable quantitative behaviour.
The talk will first give a brief summary of classical results of concurrency theory on bisimulation relations with silent moves and their logical characterizations. The second part will report on analogous results in the probabilistic setting and recent results on the probabilistic bisimulation spectrum with silent moves.
Sebastian Rudolph: The Triguarded Fragment of First-Order Logic
Past research into decidable fragments of first-order logic (FO) has produced two very prominent fragments: the guarded fragment GF, and the two-variable fragment FO2. These fragments are of crucial importance because they provide significant insights into decidability and expressiveness of other (computational) logics like Modal Logics (MLs) and various Description Logics (DLs), which play a central role in Verification, Knowledge Representation, and other areas. In this paper, we take a closer look at GF and FO2, and present a new fragment that subsumes them both. This fragment, called the triguarded fragment (denoted TGF), is obtained by relaxing the standard definition of GF: quantification is required to be guarded only for subformulae with three or more free variables. We show that, in the absence of equality, satisfiability in TGF is N2ExpTime-complete, but becomes NExpTime-complete if we bound the arity of predicates by a constant (a natural assumption in the context of MLs and DLs). Finally, we observe that many natural extensions of TGF, including the addition of equality, lead to undecidability.
Erik Paul: Finite Sequentiality of Unambiguous Max-Plus Tree Automata
In this talk, we consider the decidability of the finite sequentiality problem for unambiguous max-plus tree automata. A max-plus tree automaton is a finite tree automaton which assigns real numbers to trees over a given alphabet. The transitions of a max-plus tree automaton each carry a weight from the real numbers. To every run of the automaton, a weight is associated by summing over the weights of the transitions which constitute the run. The weight of a tree is given by the maximum over the weights of all runs on this tree. A max-plus tree automaton is called unambiguous if there is at most one accepting run on every tree. The finite sequentiality problem asks whether for a given max-plus tree automaton, there exist finitely many deterministic max-plus tree automata whose pointwise maximum is equivalent to the given automaton. I will present a criterion to decide the finite sequentiality problem for unambiguous max-plus tree automata.
Shima Asaadi: Automatic Extraction of Compositional Matrix-Space Models in Natural Language Processing
TBA
Danny Richter: Bounded Model Checking of One-Counter Automata
We study the problem of bounded model checking (BMC): given an input formula F, a state-machine model A and some non-negative integer B, does there exist a computation of A that satisfies F and whose length does not exceed B? We investigate the computational complexity of BMC in the framework of one-counter automata and extensions of LTL, where (unbounded) model checking is known to be undecidable. Second, we show how to compute a completeness threshold for one-counter automata and certain simple formulas.
Helmut Seidl: Deciding Equivalence of Tree Transducers by Means of Precise Abstract Interpretation
This presentation reviews the construction of the earliest normal form for topdown tree transducers. It will indicate how this construction allows to decide equivalence of deterministic topdown tree transducers and how it can be used to decide whether a topdown tree transducer is functional.
The earliest normal form also opens up the way for decidability of equivalence for functional sequential tree-to-string transducers, as well as for
deterministic macro tree transducers, at least when they are basic and separated.
Interestingly, both the construction of the earliest normal form as well as it application to equivalence for classes of macro tree transducers rely on techniques borrowed from precise abstract interpretation.
Luisa Herrmann: Weighted Tree Automata with Storage
Due to a large number of upcoming new automaton models in the 60s of the previous century, Dana Scott and, later, Joost Engelfriet proposed a homogeneous point of view on automata theory. They enriched finite automata by an additional memory set abstracting from concrete storage mechanisms like pushdown or counter.
We take up this concept and apply it to weighted tree automata. Thus, in this talk we speak about weighted tree automata with storage as well as various results we obtained for this model or instantiations of it.
Heiko Vogler: A Büchi-Elgot-Trakhtenbrot theorem for automata with MSO graph storage
We introduce MSO graph storage types, and call a storage type MSO-expressible if it is isomorphic to some MSO graph storage type. An MSO graph storage type has MSO-definable sets of graphs as storage configurations and as storage transformations. We consider sequential automata with MSO graph storage and associate with each such automaton a string language. For each MSO graph storage type, we define an MSO logic which is a subset of the usual MSO logic on graphs. We prove a Büchi-Elgot-Trakhtenbrot theorem.
Simon Knäuer: Relation Algebras and CSPs
TBA
Manuel Bodirsky: Reducing Infinite-Domain CSPs to Finite-Domain CSPs
In this talk I present two fundamentally different techniques to reduce infinite-domain CSPs to finite-domain CSPs, and give many examples of CSPs that can be solved in polynomial time using these methods.
Karin Quaas: Temporal logics with constraints
I present an overview of recent approaches for solving the satisfiability problem for temporal logics (LTL, CTL*) with constraints. Such logics are parameterized by a concrete domain like (N,<) or the set of finite words with the prefix relation; simple constraints over the concrete domain form the atomic formulas of these logics.
Thomas Feller: Towards Decidability for Knowledge Representations by Model-Theoretic means
TBA
Lukas Schweizer: SPARQL Queries over Ontologies Under the Fixed-Domain Semantics
Fixed-domain reasoning over OWL ontologies is adequate in certain closed-world scenarios and has been shown to be both useful and feasible in practice. However, the reasoning modes hitherto supported by available tools do not include querying. We provide the formal foundations of querying under the fixed domain semantics, based on the principle of certain answers, and show how fixed-domain querying can be incorporated in existing reasoning methods using answer set programming (ASP).
Joint work with Sebastian Rudolph and Yao Zhihao, recently published at PRICAI.
Christian Alrabbaa: Explications of Description Logic reasoning
TBA
Gustav Grabolle: Linear dynamic logic, alternating automata, and weights
In 2013 Giuseppe De Giacomo and Moshe Vardi introduced linear dynamic logic. This logic uses the intuitive syntax of PDL, has good complexity properties, and extends the expressive power of LTL: De Giacomo and Vardi prove LDL and finite automata are equally expressive. This is done via alternating automata. In 2016 Manfred Droste and George Rahonis introduced a weighted version of LDL with weights taken from semirings.
In this talk I will present the continuation of this project: A weighted LDL version applicable to a variety of weight structures. Moreover, I will introduce a new adaptation of LDL into the weighted setting. This nLDL with weights taken from commutative semirings focuses on the intuitive syntax of LDL, it is more expressive than weighted LDL, and relates to weighted LTL as LDL relates to LTL. I will show that, similar to PDL, the depth of the question-mark operator entails a hierarchy on the expressive power of nLDL. To characterize nLDL, I will introduce n-level weighted finite automata and prove that they are as expressive as nLDL. Finally, I will demonstrate that equivalence of nLDL formulas with weights taken from the rationals is decidable: I show how n-level WFA can be translated into weighted alternating automata and give a decision procedure of zeroness for WAFA with weights taken from the rationals.
Jakub Rydval: User-Definable Concrete Domains
Concrete domains were introduced to description logics to enable defining concepts using predefined concrete objects and predicates. It is known that allowing general concept inclusions (GCIs) in knowledge bases renders reasoning with some concrete domains undecidable. In this talk, we present a generalisation of the description logic with concrete domains and GCIs from [1], extend the original undecidability result of Lutz for the concrete domain (IN; succ, 0), and use model theory to study the sufficient condition for decidability of reasoning with concrete domains and GCIs introduced by Lutz and Miličić [1].
[1] C. Lutz and M. Milicic, ''A Tableau Algorithm for Description Logics with Concrete Domains and General TBoxes,'' Journal of Automated Reasoning, vol. 38, p. 227-259, 2007.
Franz Baader: The Complexity of the Consistency Problem in a Probabilistic Description Logic with Aggregation Semantics
TBA
Kevin Stier: Pumping lemmas for weighted tree automata
TBA
Willi Hieke: Model transformation in Description Logics
Description logic reasoners compute inferences by finding an arbitrary model for a given knowledge base. For explanation purposes, models with particular properties are of interest -- for example small models. In order to obtain models with the desired property, we introduce a framework that captures relevant parameters for truth-preserving transformations of graph structures that yield models with such properties. We discuss concrete transformations in form of graph transductions applied to the DL setting and show that they generate bisimilar structures.
Anni-Yasmin Turhan: Ontology-mediated Probabilistic Model Checking
TBA
Lena Schiffer: Combinatory Categorial Grammars as Acceptors of Tree Languages
Combinatory Categorial Grammar (CCG) is an extension of categorial grammar and mildly context-sensitive, so it is efficiently parsable and reaches an expressiveness that is conjectured to be sufficient to describe natural languages. The basis for CCG is provided by a lexicon and a rule system. The lexicon assigns syntactic categories to the symbols of the input and the rule system describes how adjoining categories can be combined to eventually obtain a (binary) derivation tree. The seminal work by Vijay-Shanker and Weir showed weak equivalence of CCG, Tree-Adjoining Grammar (TAG), and Linear Indexed Grammar (LIG), i.e. they accept the same string languages. However, in a linguistic setting we are also interested in the underlying structure of an input sentence in the form of a constituency parse tree. For this purpose we define the tree language accepted by a CCG as a relabeling of its derivation trees.
In the first part of this talk I will give an introduction to CCG. Then I will present some results on their expressive power in terms of tree languages with a special emphasis on their relation to Simple Monadic Context-Free Tree Grammars (sCFTG).
Andreas Maletti: Tree Substitution Grammars
We investigate the expressive power of tree substitution grammars, which are popular grammar mechanisms in the area of parsing of natural languages. A tree substitution grammar is essentially a finite set of tree fragments together with a set of initial labels. It is well known that each local tree language can be generated by a tree substitution grammar and in turn each tree language generated by tree substitution grammars is regular. We show that class of tree languages generated by tree substitution grammars enjoys none of the standard Boolean closures, but at least all finite and co-finite tree languages are contained. In addition, we report on progress on the characterization of the class inside the regular tree languages.
Gerhard Brewka: Revisiting the Foundations of Abstract Argumentation: Semantics Based on Weak Admissibility and Weak Defense
TBA
Caterina Viola: The power of linear programming for infinite-domain valued constraint satisfaction problems
Given a set D (the domain), a valued constraint language over D is a set a finite set of functions f, also called cost functions, defined on (a subset of) D and having rational values. Given a valued constraint language \Gamma, the valued constraint satisfaction problem for \Gamma, VCSP(\Gamma), takes as input a set of variables V, a finite sum \phi of cost functions from \Gamma applied to the variables in V, and a rational number u; the computational task is to decide whether there exists an assignment of values from D for the variables in V such that the cost of the assignment is not greater than u (the cost of an assignment is the value of \phi in correspondence of the tuple obtained when applying the assignment to the variables).
When the set D is finite solving VCSP(\Gamma) for a given instance is computationally equivalent to finding the assignment for the variables with minimum cost. The computational complexity of the VCSP for languages over a finite domain has been extensively studied.
Every finite-domain VCSP has a natural Linear Programming relaxation, called the basic linear programming relaxation, BLP, and a milestone in the study of finite-domain VCSP is the result of Kolmogorov, Thapper, and Zivny [1] that characterises the finite-domain languages that are correctly solved (in polynomial time) by the BLP. Their characterisation is given in terms of algebraic properties of the valued constraint language.
We will give sufficient conditions for an infinite-domain valued constraint language \Gamma to be correctly solved (in polynomial time) by applying the BLP to a suitable substructure of \Gamma.
(joint work with Manuel Bodirsky and Marcello Mamino)
[1] V. Kolmogorov, J. Thapper, and S. Zivny. The power of linear programming for general-valued CSPs. SIAM J. Comput., 44(1):1–36, 2015.
Florian Starke: Smooth digraphs modulo pp-constructability
TBA
Johannes Greiner: Generic Combinations of Temporal Structures and Bloated Finite Structures
TBA
Frederic Dörband: Rational Weighted Tree Languages with Storage
TBA
Filippo De Bortoli: On the characterization of cardinality constraints in Description Logics
TBA
