The first QuantLA workshop takes place from 9th to 13th of September in Tautewalde. Our guest lecturers are James Worrell and Frank Wolter.
Time Table
Course Programme
Frank Wolter: Modal Logics for Distance and Topology
A large variety of distinct formalisms for reasoning, directly or indirectly, about distance and topology have been developed in AI and CS. Examples include conditional logic and nonmonotonic reasoning, spatial reasoning, similarity reasoning, and metric temporal logic. In this talk I will present a modal logic framework covering large parts of these lines of research, thus enabling a comparison of distinct logics for distances and topology and a systematic investigation of their semantics, expressive power and complexity.
Linda Leuschner: Assume-Guarantee Verification for Probabilistic Systems
Model checking is a fully automatic approach for verifying system specifications. For systems consisting of several components, the size of the whole system can be exponential in the number of components. Therefore, classical model checking algorithms are often not applicable. Compositional model checking investigates methods for verifying the specications on the components without building the model of the whole system. One particular compositional approach is assume-guarantee verification. In assume-guarantee verification, a system component is supposed to interact with an abstract environment. The idea is to prove that the component fulfills a guarantee whenever the abstract environment meets a certain assumption. Proving that the actual environment in fact meets the assumption yields that the system consisting of environment and component satisfies the guarantee.
The talk summarizes the main principles of the assume-guarantee framework as investigated by Kwiatkowska et al. for Markov decision processes and action-based linear-time properties. Finally, we explain how this framework can be extended for state-based properties.
Parvaneh Babari: Weighted picture automata and weighted logics
First we give a basic introduction to the area of picture languages, which are a generalization of formal string languages to two dimensions. Picture languages have been intensively investigated by several research groups which led to a description of recognizable picture languages in terms of automata, sets of tiles, rational operations, or existential monadic second-order logic. We present the concept of weighted picture automata which are automata operating in a natural way on pictures and whose transitions carry weights; the weights are taken as elements from a given commutative semiring. The behavior of a WPA is a function which maps pictures over a finite alphabet to elements of the semiring. We call such functions picture series. In addition, we introduce the concept of a weighted MSO logic for pictures. The semantics of a weighted formula will be a picture series.
On the other hand, we present some equivalence results on weighted automata and weighted MSO logics on finite words for average and long-time behaviors. The problem is to investigate quantitative automata and quantitative logics which can model average density of pictures. For this, we wish to take valuation monoids as the abstract model for the weight structures.
Anni-Yasmin Turhan: Computing generalizations in the EL-family of DLs--approximative or exact
For DL knowledge bases computing generalizations of groups of concepts or individuals is a useful task. In general, such generalizations need not exist for knowledge bases written in the Description Logic EL. Methods for computing approximative solutions for generalizations in EL (with probabilities) and conditions under which exact solutions exist are investigated in this talk.
Doreen Götze: The Support of Nested Weighted Automata
Weighted automata form a classical model of quantitative automata. Recently, in connection with quantitative logics, a model of nested weighted automata was proposed and investigated by Bollig, Gastin, Monmege, and Zeitoun (ICALP 2010). In this paper, we wish to investigate the support of nested weighted automata, an open problem posed by Bollig et al. Our main result states that the support of nested weighted automata over zero-sum free, commutative strong bimonoids is recognizable. For this, we use methods of Kirsten (DLT 2009), in particular, his construction of finite automata recognizing the supports of weighted automata over zerosum free, commutative semirings. We also get an effective construction of a finite automaton recognizing the support of a given nested weighted automaton for zero-sum free, commutative strong bimonoids where Kirsten’s zero generation problem is decidable.
Oliver Fernandez Gil: Non-monotonic reasoning in Description Logics.
Non-monotonic reasoning has been widely studied in the last three decades and several formalisms have been proposed to deal with it, e.g. circumscription, default logic. Recently, research has been directed with the purpose to integrate non-monotonic reasoning into Description Logics. In this talk we consider some of the proposed solutions to accomplish such an integration. Specifically, we look at how knowledge can be represented and the complexity of different reasoning tasks. In addition, we mention some of the difficulties and limitations exhibited by the different approaches. Finally, we present some ideas of how to solve some of these problems and/or possible ways to extend the already existent results.
David Müller: Good-for-games automata in the context of probabilistic model checking
Model checking is a formal method to verify whether a system meets a specification. While the classical model checking approach attempts to assert that certain omegaregular properties of the safety-liveness spectrum hold for all or some executions, probabilistic model checking aims to reason about the likelihood for properties. A very prominent approach relies on a representation of the system by a finite-state probabilistic automaton and the specification by a formula of linear temporal logic (LTL). The standard approach for the computation of the probability for the LTL formula builds the product of the probabilistic automaton for the system and a deterministic automaton for the formula.
The deterministic automaton for an LTL formula can be obtained by transforming the formula to an non-deterministic Buchi automaton and determinise it afterwards. We use a special variety of Omega-automata, namely good-for-games Omega-automata, to avoid the determinisation process. To reason about the probability a given Markov chain satisfies an LTL formula, we build a product Markov decision process of the Markov chain and the good-for-games automaton corresponding to the formula. In addition we give some optimisations for the generation of good-for-games automata. We present our ongoing research to obtain good-for-games automata with a smaller state space or a smaller BDD representation.
Vitaly Perevoshchikov: Quantitative Logics and Automata on Infinite Timed Words
Weighted timed automata are a tool to model the quantitative aspects of real-time systems like consumption of memory, power or financial resources. The weights of runs in such automata are defined, for instance, as the average costs, or the sum of time-discounted costs.
We introduce a weighted relative distance logic on infinite timed words. This is a quantitative logic augmented with the possibility to assign weights to positions of a timed word. We show that our new logic is expressively equivalent to weighted timed automata with Büchi acceptance conditions. The translation process from formulas to automata and vice versa is effective.
We also discuss the problems to compute optimal weights of runs in weighted timed Büchi automata with discounting objectives. We show this problem to be solvable. This leads to decidability results for our logic with the discounting semantics.
Stefan Borgwardt: Fuzzy Description Logics with General Concept Inclusions
Description logics (DLs) are used to represent knowledge of an application domain and provide standard reasoning services to infer consequences of this knowledge. However, classical DLs are not suited to represent vagueness in the description of the knowledge. In this talk, we will consider fuzzy DLs, which can be used to reason about vague concepts.
Mainly two approaches have previously been used to reason in fuzzy DLs: tableau algorithms and reductions to classical reasoning problems. However, these methods often do not allow to derive optimal complexity bounds and may not work in the presence of general concept inclusion axioms (GCIs). Recently, it was shown that reasoning even becomes undecidable in some fuzzy DLs that allow GCIs. We generalize previous proofs of undecidability to larger classes of fuzzy DLs with GCIs, and develop reasoning algorithms for some decidable cases to obtain tight complexity bounds.
Sascha Wunderlich: Towards a framework for value accumulation in model checking
Systems often have behaviors that exhibit quantifiable aspects. It is desirable to verify specifications involving these aspects, for finite as well as infinite behaviors. The goal of multi-criterial quantitative model checking is to automate this process.
A specific challenge within this context is the handling of cost/reward accumulation for multiple criteria. One might ask for instance whether or not the total cost of a behavior fulfills some specific threshold condition, or what the energy utility ratio of a process is. To verify such properties one needs sufficiently expressive logics and appropriate models. Such tools have been researched in the past, however they do not base on a common syntactic or semantic framework. Such a framework would increase compatibility between these approaches and allow to venture of a common ground in the future.
In this talk we will obtain an overview of different techniques to formalize value accumulation for infinite behaviors. We will take a closer look at some of the more promising approaches and try to unify aspects of them to work towards a general framework.
Franz Baader: Verification of Golog Programs over Description Logic Actions
High-level action programming languages such as Golog have successfully been used to model the behavior of autonomous agents. In addition to a logic-based action formalism for describing the environment and the effects of basic actions, they enable the construction of complex actions using typical programming language constructs. To ensure that the execution of such complex actions leads to the desired behavior of the agent, one needs to specify the required properties in a formal way, and then verify that these requirements are met by any execution of the program. Due to the expressiveness of the action formalism underlying Golog (Situation Calculus), the verification problem for Golog programs is in general undecidable. Action formalisms based on Description Logic (DL) try to achieve decidability of inference problems such as the projection problem by restricting the expressiveness of the underlying base logic. However, until now these formalisms have not been used within Golog programs. In talk, I will introduce a variant of Golog where basic actions are defined using such a DL-based formalism, and show that the verification problem for such programs is decidable. This improves on our previous work on verifying properties of infinite sequences of DL actions in that it considers (finite and infinite) sequences of DL actions that correspond to (terminating and non-terminating) runs of a Golog program rather than just infinite sequences accepted by a Büchi automaton abstracting the program.
Andreas Ecke: Quantitative methods for similarity and generalization in Description Logics
Description Logics (DL) are a formalism used in the field of knowledge representation to describe and reason about concepts. The terminology, i.e., the relationships between different concepts are expressed in a TBox, individuals that instantiate those concepts are given as an ABox. There is a wide variety of similarity definitions in the field of DL, which compute the similarity between different TBoxes, between simple or complex concepts, between individuals or between elements of the interpretation domain using various methods. These similarity measures are used for different applications, like ontology matching, to enhance the expressiveness of modeling in DLs and much more. One notable connection exists between similarities and generalizations: Whenever a similarity measure is given, it can be used to generalize various things, like the inference services or even the concept descriptions itself. In this talk I will give an overview of similarity and generalizations in DLs, present my research of the previous year and explain which direction my future research will take.
Karin Quaas: Model Checking Timed One-Counter Systems
A timed one-counter system is a timed automaton extended with a counter ranging over the natural numbers. During the execution of a transition, the counter can be incremented, decremented or tested for zero. In this way, a timed one-counter system can also be regarded as an extension of a one-counter machine with clocks. By an easy extension of the classical region graph construction for timed automata, one can prove that the reachability problem for timed onecounter systems is decidable. Metric Temporal Logic (MTL, for short) is an extension of LTL used in the analysis of timed systems. In MTL, the temporal operators are labelled with time intervals constraining the point of time when a formula should hold. MTL formulas are evaluated over runs of timed automata. Ouaknine and Worrell proved in 2006, that MTL model checking problem for timed automata over finite timed words is decidable, albeit with non-primitive recursive complexity.
In this talk, I am going to present ongoing research work about the following problem: given a timed one-counter system A and an MTL-formula F, is there some run of A that satisfies F?
Claudia Carapelle: Satisfiability of CTL* with constraints
CTL* formulas can be enriched to express relations between variables whose value can range in a chosen concrete domain. Chosen the appropriate domain one can express quantitative properties that ordinary CTL* formulas can only approximate through abstraction. We can refer directly to concrete values and describe how they change in time, with many possible applications in model checking.
In this talk we show that satisfiability for CTL* with equality-, order-, and modulo- constraints over the concrete domain Z is decidable.
Markus Teichmann: Characterizing Tree Valuation Languages by Multioperator Weighted Tree Languages
Weighted tree languages can be a) recognized by weighted tree automata over tree valuation monoids, b) defined by monadic second order logic over tree valuation monoids, c) recognized by weighted tree automata over multioperator monoids, and d) defined by multioperator expressions. We show that the classes a) and b) are characterized by c) and d), respectively, using a special multioperator monoid.
Marcel Lippmann: Temporalised Description Logics for Monitoring Partially Observable Events
Daily life depends on complex hardware and software systems. In runtime monitoring, one (incompletely) observes the behaviour of the actual system in a structured way. This information is used to verify that the system has certain properties, which are formulated in a temporal logic, or to answer temporal queries to determine whether a certain situation has arisen. One approach to runtime monitoring is using temporalised Description Logics to formalise temporal properties and so-called ABoxes to capture incomplete observations of the system's behaviour.
Shiguang Feng: Ehrenfeucht–Fraïssé games on weighted temporal logic
The Ehrenfeucht–Fraïssé game is a useful tool to show that some properties are not definable in first-order logic. In finite model theory, the EF game and many of its variants for some extensions of FO logic are widely used to prove nonaxiomatizability results in the corresponding logics. This makes it a nice tool to capture the expressiveness of a logic. TPTL and MTL are two classical timed extensions of LTL. Bouyer and others showed that TPTL is strictly more expressive than MTL, which was a 20-year-old conjecture. We consider TPTL(Z) and MTL(Z) whose semantics are based on weighted words in which every point is assigned a natural number as its weight. We define a weighted version of the EF game on temporal logic. Using these games, we do the following:
- show that TPTL(Z) is strictly more expressive than MTL(Z).
- show that the until hierarchy and the constant hierarchy are strict for both MTL(Z) and TPTL(Z).
- provide an easier proof for Bouyer's result.
We also show that:
- The SAT problem for MTL(Z) is undecidable ( consequently also for TPTL(Z) ).
- The SAT problem for the future fragment of TPTL(Z) is decidable.
Mike Behrisch: Relational Structure Theory -- an introduction
In the talk we show how universal algebras such as e.g. semigroups, semirings, lattices etc. can be analysed using a relational localisation framework, called "Relational Structure Theory". We explain how to translate algebras into relational structures, and how to exploit their induced substructures in order to study the algebraic counterparts locally. In particular, we outline, how global properties can be transferred to the localisations, and how knowledge about sufficiently many local pieces can be used to infer results for the global structure. This leads us to a reconstruction property which exhibits deep relationships with categorical equivalences of varieties. If time permits we will also sketch applications in this direction.
Daniel Borchmann: General Concept Inclusions with High Confidence in Finite Interpretation
We present extensions on results on axiomatizing general concept inclusions enjoying a certain confidence in given finite interpretations. Among others, we show how bases of such confident GCIs can be directly inferred from bases of confident implications from a certain formal context. We also discuss experimental results on how bases of confident GCIs behave on real-world data. Furthermore, we give first insights into an attempt to provide an algorithm that allows for an interactive computation of bases of confident GCIs, allowing an external expert to distinguish between rare (but correct) counterexamples and real errors in the initial data.
Johannes Osterholzer: A Pushdown Machine for Context-Free Tree Translation
Synchronous context-free tree grammars (SCFTG) are applied for syntax-based translation of natural languages. They can be considered as context-free tree grammars where an input and an output tree are derived synchronously.
In the talk, the notion of pushdown extended top-down tree transducers (PDXTT) will be introduced. The class of transformations that are computed by linear and non-deleting PDXTT will be demonstrated to coincide with the class of transformations of simple SCFTG, which are a certain syntactic restriction of SCFTG.
Sebastian Rudolph: Flag & check: data access with monadically defined queries
We introduce monadically defined queries (MODEQs) and nested monadically defined queries (NEMODEQs), two querying formalisms that extend conjunctive queries, conjunctive two-way regular path queries, and monadic Datalog queries. Both can be expressed as Datalog queries and in monadic second-order logic, yet they have a decidable query containment problem and favorable query answering complexities: a data complexity of P, and a combined complexity of NP (MODEQs) and PSpace (NEMODEQs).
We show that (NE)MODEQ answering remains decidable in the presence of a well-known generic class of tuple-generating dependencies. In addition, techniques to rewrite queries under dependencies into (NE)MODEQs are introduced. Rewriting can be applied partially, and (NE)MODEQ answering is still decidable if the non-rewritable part of the TGDs permits decidable (NE)MODEQ answering on other grounds.
Stefan Dück: Weighted Automata and Logics for Infinite Nested Words
Nested Words introduced by Alur and Madhusudan are used to capture structures with both linear and hierarchical order, e.g. XML documents, without losing valuable closure properties. Furthermore Alur and Madhusudan introduced infinite nested words and equivalent logics for both finite and infinite nested words, thus extending Büchi's theorem to nested words. In recent papers Droste and Pibaljommee generalized this ideas to weighted automata and weighted logics for nested words while Droste and Meinecke introduced weighted logics over valuation monoids for infinite words. It is the goal of this paper to introduce weighted automata over valuation monoids for infinite nested words and to characterize the emerging regular languages with an equivalent weighted logic.
Manfred Droste: Weighted logics for unranked tree automata
We define a weighted monadic second order logic for unranked trees and the concept of weighted unranked tree automata, and we investigate the expressive power of these two concepts, with the weights being computed in any semiring. We show that weighted tree automata and a syntactically restricted weighted MSO-logic have the same expressive power in case the semiring is commutative or in case we deal only with ranked trees, but, surprisingly, not in general. This demonstrates a crucial difference between the theories of ranked trees and unranked trees in the weighted case. If time permits, we will also consider recent extensions of the weight structures to valuation monoids. These contain all semirings, but also average computations of real numbers as weights, recently considered by Henzinger and others.
Gerhard Brewka: Towards Reactive Multi-Context Systems
Among the challenges faced by the area of knowledge representation (KR) are the following ones: firstly, knowledge represented in different knowledge representation languages needs to be integrated, and secondly, certain applications have specific needs not typically fulfilled by standard KR systems. What we have in mind here are applications where reasoners, rather than being called by the user in order to answer some specific query, run online and have to deal with a continuous stream of information. In this paper we argue that multi-context systems (MCS) are adequate tools for both challenges. The original MCS approach was introduced to handle the integration problem in a principled way. A later extension to so-called managed MCS appears to provide relevant functionality for the second challenge. In this talk we review both MCS and managed MCS and discuss how the latter approach needs to be further developed for online applications.
Thomas Weidner: Probabilistic ω-Regular Expressions
We introduce probabilistic ω-regular expressions which are an extension to classical regular expressions with semantics taking probabilities into account. The main result states that probabilistic ω-regular expressions are expressively equivalent to probabilistic Muller-automata. To obtain better decidability properties we introduce a simple subclass of our expressions with decidable emptiness problem.
