The third QuantLA workshop takes place from 26th to 28th of August at the Seehotel Zeuthen in Zeuthen, Berlin/Brandeburg. Our guest lecturer is Birte Glimm.
Time Table
Course Programme
Birte Glimm: Tableau Algorithms and their Optimisations
Knowledge representation and management are elementary parts of intelligent systems. Classical database systems are not always suited since they are designed for homogeneous data with a static schema. Knowledge bases, on the other hand, can flexibly represent both data and schema. Languages used in knowledge representation are often based on Description Logics and allow for automated reasoning to make implicit knowledge explicitly available. Description Logics are decidable fragments of first-order logic and they are also the basis for the Web Ontology Language OWL, standardised by the World Wide Web consortium.
Automated reasoning in expressive Description Logics is mostly based on (variants of) tableau algorithms. In this talk I will first present the basics of Description Logics and tableau algorithms. I will then give an overview about recently developed optimisation techniques that yield significant performance improvements. This includes optimisations for preprocessing knowledge bases and for reasoning by combining tableau procedures with tractable saturation procedures for less expressive logics. The latter allows for a better pay-as-you-go behaviour of reasoning systems, when a knowledge bases only uses few language features that require the use of the computationally expensive tableau algorithm. Finally, I will present a novel extension to the tableau algorithm, namely nominal schemas, that allow a direct treatment of rule-like knowledge.
David Müller: Pseudodeterminism in the context of probabilistic model checking
Probabilistic model checking can be used for the qualitative and quantitative analysis of a system against a formal specification. In our context, the systems are typically modelled as Markovian models, e.g. Markov chains and Markov decision processes. For the specifications, we concentrate here on linear temporal logic (LTL). In the automata-theoretic approach, the LTL formula is converted into an omega-automaton and the analysis is carried out on the product construction of the system and automaton.
In contrast to the non-probabilistic setting, the probabilistic choices are incompatible with the direct use of a non-deterministic automaton for the formula. In the standard approach, the non-deterministic Büchi automaton obtained from the LTL formula is determinized, but this can lead to a double- exponential blow-up. There are approaches for Markov chain analysis against LTL with exponential runtime, which motivates the search for non-deterministic automata with restricted forms of non-determinism that make them suitable for probabilistic model checking (PMC).
In my status talk I will analyse two forms of pseudodeterministic automata: good-for-games automata and unambiguous automata. I show how good-for-games automata allow reasoning about the maximal probability of a Markov decision process satisfying an LTL formula. I will also discuss first results on Markov chain analysis with unambiguous Büchi automata. At last I will cover HOA generic acceptance.
Sascha Wunderlich: Greener Bits with Probabilistic Model Checking
Today, in a time when the internet is crucial, data centers are an important part of our infrastructure. They are well suited for decentralized storage and computation. However, they are also hungry for energy.
One possibility for quenching this hunger is to use local renewable energy sources like solar or wind. The advantage of this method is that it is not only relatively friendly for the environment, but also cheap. The disadvantage is that its availability wildly fluctuates depending on the season, time of day and most importantly the weather.
In this setting, it is desirable to adjust the scheduling of jobs in a data center according to the weather forecast, such that the energy demand adapts to the available green energy.
In this talk, we investigate how probabilistic model checking can be used to achieve this goal. Specifically, we will look at the modeling of the given scenario as a weighted Markov decision process and at the formulation of deadlines and other constraints as according specifications. We will then use existential probabilistic model checking and scheduler synthesis to extract an energy-efficient working plan.
Linda Leuschner: Model Checking Inter-Process Communication using Conditional Assume-Guarantee Reasoning
Random hardware faults, as they occur quite often in our computers, can have horrifying consequences. Therefore, it is a natural requirement to verify or analyze resilience mechanisms that try to minimize the effects of those faults. Model checking, a well-established automated verification method, is shown to work well for small instances of many algorithms. Nevertheless, traditional model checking techniques often fail for real world scenarios due to the state space explosion problem. Compositional methods try to cope with this problem by using the compositional structure that is inherent in most real world systems.
In this talk, a new probabilistic compositional model checking method using conditional probabilities and Bayesian rules is presented. We use this method for analyzing an inter process communication protocol and show that we are able to reduce model checking time and memory consumption significantly.
Oliver Fernandez Gil: Adding Threshold Concepts to the Description Logic EL: Acyclic TBoxes
We have recently introduced a new family of Description Logics (DLs) by adding threshold concepts to the lightweight DL EL. The semantics of these newly introduced concepts is based on the use of graded membership functions, which for each individual and concept yields a number in the interval [0,1]. We proved that for a specific such function, the complexity of reasoning in the resulting threshold logic alternates between NP and coNP (for the standard DLs reasoning tasks). However, knowledge in the form of a background set of axioms is not considered.
We take a step forward into this and extend our threshold logic towards acyclic terminologies. We will define acyclic TBoxes in our logic and show that reasoning with them becomes harder than with the empty terminology.
Andreas Ecke: Reasoning with Prototypes in the Description Logic ALC using Weighted Tree Automata
We introduce an extension to Description Logics that allows to define prototypes. To accomplish this, we use prototype distance functions, which assign to each element of an interpretation a distance, or dissimilarity, to the abstract prototype. Based on this prototype distance function, a new concept constructor can be used, which is interpreted as the set of all elements with a distance smaller than a given threshold. We show how weighted alternating tree automata (wata) over the non-negative tropical semiring of integers can be used to encode concepts and pointed interpretations as prototypes. Finally, we investigate the complexity of reasoning in ALCP(wata), which extends the Description Logic ALC with prototypes defined using wata.
Parvaneh Babari Ghorghi: Weighted Register Automata and Weighted Logic for Data Words
In this paper, we investigate automata models for quantitative aspects of systems with infinite data domains, e.g., the costs of storing data on a remote server or the consumption of resources (e.g., memory, energy, time) during a data analysis. We introduce weighted register automata on data words, study their closure properties and introduce a determinizable subclass of them. In our main result, we give a logical characterization of weighted register automata by means of weighted existential monadic second-order logic.
Vitaly Perevoshchikov: Logics for Weighted Timed Pushdown Automata
Weighted dense-timed pushdown automata with a timed stack were introduced by Abdulla, Atig and Stenman to model the behavior of real-time recursive systems. Motivated by the decidability of the optimal reachability problem for weighted timed pushdown automata and weighted logic of Droste and Gastin, we introduce a weighted MSO logic on timed words which is expressively equivalent to weighted timed pushdown automata. To show the expressive equivalence result, we prove a decomposition theorem which establishes a connection between weighted timed pushdown languages and visibly pushdown languages of Alur and Mudhusudan; then we apply their result about the logical characterization of visibly pushdown languages.
Johannes Osterholzer: A direct link between Tree-Adjoining and Context-Free Tree Grammars
The tree languages of tree-adjoining grammars are precisely those of linear monadic context-free tree grammars. Unlike the original proof, we present a direct transformation of a tree-adjoining grammar into an equivalent linear monadic context-free tree grammar.
Thomas Weidner: Model Checking Constraint LTL over Trees
Constraint automata are an adaptation of Büchi-automata that process data words where the data comes from some relational structure S. Every transition of such an automaton comes with constraints in terms of the relations of S. A transition can only be fired if the current and the next data values satisfy all constraints of this transition. These automata have been used in the setting where S is a linear order for deciding constraint LTL with constraints over S. In this paper, S is the infinitely branching infinite order tree T. We provide a PSPACE algorithm for emptiness of T-constraint automata. This result implies PSPACE- completeness of the satisfiability and the model checking problem for constraint LTL with constraints over T. This is joint work with Alexander Kartzow.
Doreen Heusel: Weighted Tree Automata and Regular Expressions over Valuation Monoids
Trees or terms are one of the most fundamental concepts both in mathematics and in computer science. Thus, weighted tree automata gained a lot attention during the last decades. Usually, the weight of a run is computed locally by a binary operation. Chatterjee, Doyen, and Henzinger presented a new approach for strings with real numbers as weights. The weight of a run is now determined by a global valuation function. An example of such a valuation function is the average of the weights. For strings, this idea was generalized by Droste and Meinecke to more general weight structures, called valuation monoids. Recently Droste, Götze, Märker, and Meinecke adapted this concept to weighted tree automata.
Here, we define rational expressions for trees over tree valuation monoids and show that rational tree series and formal tree series which are accepted by weighted tree automata are expressively equivalent over Cauchy unital tree valuation monoid. Cauchy unital tree valuation monoid allow us to decompose the Valuation function into a family of operations. We use these restrictions to simulate concatenations of tree series by direct automata-theoretic constructions. Thus we can give a constructive proof of the equivalence result.
Markus Teichmann: Regular Tree Languages and Context-Free Tree Languages
In the area of machine translation, formal languages are used to describe natural languages. It was shown that context-free string languages are not suitable to capture all linguistic features of natural languages. Hence, mildly context-sensitive languages are considered. Moreover, in natural language processing, it is often desirable to involve the structure of a sentence. Trees are one approach to explicitly represent the structure of a sentence. Context-free tree grammars (CFTGs) are powerful and promising devices to generate such trees. They allow for modeling various linguistic features, but come with high computational costs. Regular tree grammars (RTGs) are computationally favorable, but lack the descriptive power of CFTGs. Weighted extensions of both formalisms are used to disambiguate sentences and determine the grammaticallity of translations. Hence, it is worthwile to compare the expressiveness of (weighted) CFTGs and (weighted) RTGs.
In this talk, I present a decidable criterion that ensures that a CFTG yields a regular tree language together with a construction to transform this CFTG into a RTG which describes the same language. Furthermore, I outline how a weighted RTG can be used to approximate a weighted CFTG and thus obtain good computability while loosing as little information as possible.
Claudia Carapelle: Temporal Logics with Concrete Domains
Temporal logics are a very popular family of logical languages, used to specify properties of abstracted systems. Many extensions of temporal logics have been proposed in order to express more than just abstract properties.
In our work we study temporal logics extended by local constraints, which allow to express quantitative properties on words (also trees or Kripke structures) with the addition of data values from an arbitrary relational structure: a concrete domain. The constraints are local in the sense that they allow to compare data values at a fixed distance in the considered model.
We present some decidability and undecidability results for LTL and CTL* with local constraints, concentrating on concrete domains over the integers with order- and equality-constraints.
Shiguang Feng: The expressive power and path checking complexity of MTL and TPTL over data words
We consider the expressive power of MTL (metric temporal logic) and TPTL (timed propositional temporal logic) over non-monotonic data words. Using Ehrenfeucht–Frasse games for these two logic, we showed that TPTL is strictly more expressive than MTL, and the until hierarchy and the constant hierarchy are strict for both MTL and TPTL. Using reductions from the halting and instruction recurring problem of non-deterministic two counter machines, we showed that the satisfiability problem of MTL and TPTL is undecidable. This is even the case if we do not allow for propositional variables. We also consider the complexity of path checking problems for MTL and TPTL over non-monotonic data words. Precise complexity results are derived for MTL and TPTL on (in)finite data words and deterministic one-counter machines. Depending on the number of register variables and the encoding of numbers in constraints (unary or binary), the complexity is either P-complete or PSPACE-complete.
