The color coding means:

: all participate
: Doctoral students participate

Abstracts

Prof. Dr. Markus Lohrey: Algorithmic Theory of Automatic Structures

In the talk, I will give an overview of classical as well as more recent results on automatic structures, in particular their algorithmic theory. Automatic structures are finitely presented structures where the universe and all relations can be recognized by finite automata. In contrast to computable structures (where the universe and all relations have to be computable sets), automatic structures have some good algorithmic properties. The most important result in this context states that every automatic structure has a decidable first-order theory. This result has been extended to several more powerful logics, and complexity results for restricted classes of automatic structures have been shown. On the other hand, several important algorithmic problems are undecidable (and some of them are even located on high levels of the arithmetical and analytical hierarchy). Classical examples are reachability and the isomorphism problem.

Dr. Andreas Morgenstern: From LTL to symbolically Represented Deterministic Automata

Temporal logics like LTL are frequently used for the specification and verification of reactive systems. For verification, LTL formulas are typically translated to generalized nondeterministic Büchi automata so that the verification problem is reduced to checking the emptiness of automata. While this can be done symbolically for nondeterministic automata, other applications require deterministic automata, so that a subsequent determinization step is required. Unfortunately, currently known determinization procedures for Büchi automata like Safra’s pro- cedure are not amenable to a symbolic implementation.

In this talk, I'll show that this determinization step can be significantly improved for tool implementations by replacing Safra’s determinization by simpler determinization procedures.

In particular, we exploited (1) the temporal logic hierarchy that corresponds to the well-known automata hierarchy consisting of safety, liveness, Büchi, and co-Büchi automata as well as their boolean closures, (2) the non-confluence property of ω-automata that result from certain translations of LTL formulas. Both approaches lead to determinization procedures that are amenable to a symbolic implementation with BDDs or SAT-Solvers.

Alexander Heußner: Graph Rewriting based Approaches for Verifying Concurrent, Asynchronous Programs

Recently, new libraries and paradigms have been proposed to directly harness the power of today's ubiquitous multi-core platforms and to make the development of concurrent software more accessible to software engineering. But writing parallel code is a notriously difficult and error prone task, thus automatic verification becomes crucial in this setting. As a faithfull formal model of the techniques, which are applied in practice today, requires to include features like task parallelism, message and waiting queues, local and global data structures, as well as sophisticated causal entanglements, we also need to take a look behind "classical", infinite state models from automata theory and Petri nets.
In this presentation, we will discuss two examples of applying graph rewriting based approaches for modelling and verifying concurrent, asynchronous systems:
First, we present Recursive Communicating Processes (RCPS), a formal model inspired by Sockets-based, distributed applications. After briefly investigating the limits of this "classical" automaton-based model regarding simple model checking questions, we take a closer look on the reformulation of RCPS's semantics with the help of hyperedge replacement grammars. The latter allows us to finally overcome negative decidability results for temporal logic model checking by permitting the verification of MSO properties on the underlying event-structure.
Second, we present Queue-Dispatch Asynchronous Systems (QDAS), a formal model for asynchronous programs with waiting queues, inspired by Apple's Grand Central Dispatch. QDAS's semantics is directly expressed with the help of graph rewriting to grasp the model's intricacies. We give an outlook on the decidability frontier for simple verification questions, e.g., coverability, and emphasize QDAS's relationship to classical formalisms such as pushdown systems, Petri nets, and fifo systems.
We conclude with an outlook on on-going and future research.

Daniel Krähmann: Topological spaces and logic

Since the study of topological spaces is not part of a usual course in computer science we decided to give a small introduction to this field of mathematics and its applications in logic. For this purpose we introduce topological spaces and some selected concepts of topology with the goal to understand Tychonoff's theorem. We then use the obtained knowledge to prove the compactness theorem of propositional logic. At the end of the talk we mention other applications of topological methods in computer science.

Daniel Borchmann, Sascha Wunderlich: Beam Me Up! - LaTeX-Beamer For Those Who Already Know

In this talk, we address some of the prominent mistakes made in LaTeX-beamer slides. Additionally, we share some best practices and tricks to make life easier with beamer.

Radim Belohlavek: Formal concept analysis and fuzzy logic

We will provide an overview of past and recent developments in formal concept analysis (FCA) and related areas in a setting of fuzzy logic. In the setting of fuzzy logic, the yes/no-attributes of ordinary FCA are replaced by fuzzy attributes, i.e. attributes with values in a scale of degrees. The scales we employ conform to the structure of a residuated lattice which is used in modern fuzzy logic. We start with an overview of relevant issues in fuzzy logic. Then we provide selected results on the key structures and notions employed in FCA, including Galois connections, closure operators, concept lattices, completions, and attribute implications developed in a fuzzy setting. In the last part, we present some recent topics related to FCA, including factor analysis of matrices/relations with entries from scales.

Prof. Dr. Dr. h.c. Reinhard Wilhelm: Timing Analysis of Real-Time Systems

Hard real-time systems are subject to stringent timing constraints which are dictated by the surrounding physical environment. A schedulability analysis has to be performed in order to guarantee that all timing constraints will be met ("timing validation"). Existing techniques for schedulability analysis require upper bounds for the execution times of all the system's tasks to be known. These upper bounds are commonly called worst-case execution times (WCETs). The WCET-determination problem has become non-trivial due to the advent of processor features such as caches, pipelines, and all kinds of speculation, which make the execution time of an individual instruction locally unpredictable. Such execution times may vary between a few cycles and several hundred cycles.
A combination of Abstract Interpretation (AI) with Integer Linear Programming (ILP) has been successfully used to determine precise upper bounds on the execution times of real-time programs. The task solved by abstract interpretation is to compute invariants about the processor's execution states at all program points. These invariants describe the contents of caches, of the pipeline, of prediction units etc. They allow to verify local safety properties, safety properties who correspond to the absence of "timing accidents". Timing accidents, e.g. cache misses, pipeline stalls are reasons for the increase of the execution time of an individual instruction in an execution state.
The technology and tools have been used in the certification of several time-critical subsystems of the Airbus A380, the Airbus A350, and the M400. The AbsInt tool, aiT, is the only tool worldwide, validated for these avionics applications.

Parvaneh Babari: Weighted picture automata and weighted MSO logics for average and long-time behaviors

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. In 2006, in order to calculate the total density of the pictures, Ina M\"aurer established 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. Here, we investigate quantitative automata and quantitative logics which can model average density of pictures. For this purpose we take valuation monoids as the abstract model for the weight structures, and therefore some of our results do not need distributivity of multiplication over addition or commutativity or even associativity of multiplication. In addition, we show that suitable fragments of weighted MSO logics and these new weighted picture automata are expressively equivalent.

Martin Huschenbett: The Equational Theory of Aperiodic Monoids Is Decidable in Exponential Time

Due to a result by McCammond (Int. J. Algebra Comput., 2001) it is decidable whether all aperiodic monoids satisfy some given identity of omega-terms. The respective decision procedure works by computing normal forms, but unfortunately neither its worst-case running time nor the maximal size of the intermediate terms have been estimated. We pursue a different approach and solve the same problem by means of first-order definability of regular languages and an infinite Ehrenfeucht-Fraïssé game on omega-terms. In this way, we obtain an algorithm which decides whether a given identity of omega-terms holds in all aperiodic monoids and whose running time is exponential in the size of the omega-terms. As a byproduct we develop a framework which allows for seperating the bookkeeping involved in winning strategies for Ehrenfeucht-Fraïssé games on finite words from the actual strategy.

Prof. Dr. Stefan Woltran: Characteristics of Multiple Viewpoints in Abstract Argumentation

The study of extension-based semantics within the seminal abstract argumentation model of Dung has largely focused on definitional, algorithmic and complexity issues. In contrast, matters relating to comparisons of representational limits, in particular, the extent to which given collections of extensions are expressible within the formalism, have been under-developed. As such, little is known concerning conditions under which a candidate set of subsets of arguments are ``realistic'' in the sense that they correspond to the extensions of some argumentation framework for a semantics of interest. In this work we present a formal basis for examining extension-based semantics in terms of the sets of extensions that these may express within a single argumentation framework. We provide a number of characterization theorems which guarantee the existence of frameworks whose set of extensions satisfy specific conditions and derive preliminary complexity results for decision problems that require such characterizations.

Prof. Dr. Pietro Baroni: On the uses of numbers in abstract argumentation

Interest in the use of numbers in argumentation in general and, in particular, in the context of the formalism of abstract argumentation frameworks is gaining momentum in last years, with a variety of proposals appearing in recent literature where numbers are used in various different ways and sometimes with very different meanings, in spite of possible formal similarities. The lack of a reference framework, explicitly stated assumptions, and shared principles, makes difficult to assess and compare these proposals in a systematic way and also to point out some possibly overlooked potential lines of development for numerical argumentation.
The talk will present an ongoing work aimed at laying out a systematic classification of the uses and meanings of numbers in abstract argumentation, with focus on placing some prominent literature proposals in the picture and on discussing directions for future investigation.

David Müller: Probabilistic model checking with unambiguous automata

Model checking constitutes a formal approach of system verification. Classical model checking has the goal of determining whether a property from the safety-liveness spectrum holds, while probabilistic model checking analyzes a probabilistic system and aims to reason about the likelihood for properties.
Markov chains and Markov decision processes are often employed as base models in the setting of probabilistic model checking. On the specification side, common approaches use LTL, which induces an omega-regular language, or PCTL, a branching-time temporal logic.
In our approach we want to be able to specify properties over finite behavior by regular expressions. Since arbitrary NFA are not directly usable for probabilistic model checking, NFA are usually determinized yielding a DFA with an exponential blow-up. We want to avoid this determinization step and use unambiguous NFA instead. For a given MDP M and a regular expression f our method constructs an unambiguous NFA A for f, analyses the graph of M and the graph of A, and builds an inequality system out of M and A. Additionally we give some insights of our ongoing research and discuss some open problems.

Daniel Borchmann: The Stegorsaurus of Pseudo-Intents

Within the area of formal concept analysis the canonical base representes a classical example of a minimal base which can be described explicitly. Its definition involves the notion of pseudo-intents, a concept which up to today is not completely understood. In this talk we introduce pseudo-intents and the canonical base, and give experimental evidence about a correlation between the number of intents and the number of pseudo-intents of a randomly chosen formal context.

Dr. Michael Ummels: Computing Quantiles in Markov Reward Models

Probabilistic model checking mainly concentrates on techniques for reasoning about the probabilities of certain path properties or expected values of certain random variables. For the quantitative system analysis, however, there is also another type of interesting performance measure, namely quantiles. A typical quantile query takes as input a lower probability bound p and a reachability property. The task is then to compute the minimal reward bound r such that with probability at least p the target set will be reached before the accumulated reward exceeds r.
In the first part of this talk, we present our work on the complexity of quantile queries for until properties in discrete-time finite-state Markov decision processes with non-negative rewards on states. We show that qualitative quantile queries can be evaluated in polynomial time and present an exponential algorithm for the evaluation of quantitative quantile queries, which is based on linear programming.
In the second part of this talk, we sketch recent extensions of our work to more general quantile queries, and possible applications.