Upper seminar "Theoretical computer science

In the advanced seminar "Theoretical Computer Science", employees, interested students and guests present current research work in the field of theoretical computer science.

Tuesday, 08.10.2024 Maurice Herwig

Using Shared Packed Parse Forests to compute all Minimal Corrections

The work deals with the efficient computation of all minimal corrections with respect to a minimality definition. The calculation can be divided into two independent phases. In the first phase, all corrections for a word and a context-free grammar are calculated. An adapted version of the Generalized Earley Parser is used for the calculation and the resulting corrections are stored in a Shared Packed Parse Forest. It is shown that the forest can be calculated for a word of length n in n^3 and contains all corrections that correct the word in the language of the grammar. The set of minimal corrections can then be filtered out from the set of all corrections using filters. This is presented as an example of a minimality definition.

Tuesday, 06.08.2024 Georg Siebert

Randomized Smoothing for Time-aware Robustness of Temporal Graph Neural Networks

Temporal Graph Neural Networks (TGNN) are used in many modern applications such as the detection of fake news in social networks or the prediction of traffic flow. One problem that arises in such applications is adversarial attacks, where attempts are made to change the input of the network so that its actual output changes. A security property that guarantees robustness against adversarial attacks is the Adversarial Robustness Property (ARP). In this master colloquium, we will therefore deal with ARPs for TGNNs. We will set up different ARPs for TGNNs, whereby an important component is the budget, which describes the changes to the temporal graph. Furthermore, we will see how an ARP for a TGNN can be proven with the Randomized Smoothing Framework. For the established ARPs, experiments were conducted on benchmark datasets in which an attempt was made to detect an ARP for a TGNN. We will conclude by looking at the setup and results of these experiments.

Thursday, 18.07.2024 and Thursday, 11.07.2024: Lukas Mentel

IC3 / PDR and SMT-LIB for Formal Verification of Embedded Systems

Bounded model checking in conjunction with k-induction is often used for symbolic model checking. IC3 ("Incremental Construction of Inductive Clauses for Indubitable Correctness") [1] represents an alternative to this approach and is certainly one of the most important innovations in this area in the last 15 years [2].
In this approach, a set of formulas is modified step by step with the aim of obtaining a (1-inductive) invariant.
In this talk, I will give an overview of IC3 and its extension Property Directed Reachability (PDR). Furthermore, I will present the progress of the implementation of IC3 and PDR based on the SMT-LIB standard for my master thesis.
[1] Bradley, A.R. (2011). SAT-Based Model Checking without Unrolling. In: Jhala, R., Schmidt, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2011. Lecture Notes in Computer Science, vol 6538. Springer, Berlin, Heidelberg. doi.org/10.1007/978-3-642-18275-4_7
[2] N. Een, A. Mishchenko and R. Brayton, "Efficient implementation of property directed reachability," 2011 Formal Methods in Computer-Aided Design (FMCAD), Austin, TX, USA, 2011, pp. 125-134.

Thursday, 27.06.2024: Sören Möller

Formal Reasoning about Dual Influences in Natural Sciences Experiments

As part of the advanced seminar, a simple calculus, the "Calculus of Influence", has already been presented to prove statements about the local behavior of partial, continuous functions. The calculus is based on experiments that describe the behavior of "variable A influences variable B". The question arose as to how this behaves when several variables jointly influence another variable.
In my project, I transferred the definitions to the use of two variables. The goal was to extend the completeness results to this new calculus that works with multiple variables. In this talk I will present the new model, the results obtained and the difficulties encountered.

Thursday, 16.05.2024: Georg Siebert

Randomized Smoothing for Time-aware Robustness of Temporal Graph Neural Networks

In the first part of the talk, we will give a short introduction to the Randomized Smoothing Framework (RSF), which allows to compute probabilistic, budget-based certificates for robustness properties of arbitrary classification models. We also introduce the Temporal Graph Neural Network model in the transition to Part 2.
In the second part, we discuss the recent work of Georg Siebert on the application of the RSF to TGNN models and benchmarks commonly used in practice. We will focus on first practical results and empirical conclusions.

Friday, 26.04.2024: Laurin Pöppe

Implementation of a translation of neural networks into I/O-equivalents Finite Automata

Neural networks are widely used for solving complex problems. However, the verification of properties and analysis of the behavior of neural networks remains a problem. One approach is to analyze them using automata theory. For this approach, a construction of a multi-track automaton from a neural network restricted to an activation pattern is presented.

Thursday, 15.2.2024: Martin Lange

Fixpoints in Modal Logic: Finite Convergence and Higher Order

Fixpoint iteration is the main tool for evaluating recursively defined properties in temporal specification languages like the modal mu-calculus Lmu. Finite convergence, i.e. the phenomenon of reaching a fixpoint after finitely many iterations only, is of particular interest for algorithmic properties of such logics.
The iteration of fixpoints of Lmu formulas trivially converges finitely on finite structures, but also clearly on (infinite) structures whose bisimulation quotient is finite. We start by reviewing the converse and present a (word) structure W on which all mu-calculus fixpoints converge finitely, even though that structure does not have a finite bisimulation quotient. We then introduce Higher-Order Fixpoint Logic HFL, an extension of Lmu in which formulas denote (higher-order) functions on sets of states of a transition system, with a type order such that Lmu is exactly HFL0, the set of HFL formulas only using functions of order 0.
HFL is interesting in this context because it is very easy to construct an HFL1 formula, i.e. using first-order functions, that does not converge finitely over W. Moreover, it introduces a hierarchy of classes of transition systems with finite convergence of (higher-order) fixpoints. It is not unreasonable to suspect this hierarchy to collapse at a low type level, but this is currently an open question. We will present some ideas on how to tackle this.
This is joint work with Florian Bruse and Marco Sälzer of the University of Kassel and Etienne Lozes of the Université Cote d'Azur.

Thursday 1.2.2024: Florian Bruse

The Calculus of Temporal Influence

We present the Calculus of Temporal Influence, a simple logical calculus that allows reasoning about the behavior of real-valued functions over time by making assertions that bound their values or the values of their derivatives. The motivation for the design of such a proof system comes from the need to provide the background computational machinery for tools that support learning in experimental subjects in secondary-education classrooms. The end goal is a tool that allows school pupils to formalise hypotheses about phenomena in natural sciences, such that their validity with respect to some formal experiment model can be checked automatically. The Calculus of Temporal Influence provides a language for formal statements and the mechanisms for reasoning about valid logical consequences. It extends (and deviates in parts from) previous work introducing the Calculus of (Non-Temporal) Influence by integrating the ability to model temporal effects in such experiments. We show that reasoning in the calculus is sound with respect to a natural formal semantics, that logical consequence is at least semi-decidable, and that one obtains polynomial-time decidability for a natural stratification of the problem.

Thursday, 18.1.2024: Martin Lange

Formal Reasoning about Influence in Natural Sciences Experiments

We present a simple calculus for deriving statements about the local behavior of partial, continuous functions over the reals, within a collection of such functions associated with the elements of a finite partial order. We show that the calculus is sound in general and complete for particular partial orders and statements. The motivation for this work is drawn from an attempt to foster digitalization in secondary-education classrooms, in particular in experimental lessons in natural science classes. This provides a way o formally model experiments and to automatically derive the truth of hypotheses made about certain henomena in such experiments.

Thursday, 11.1.2024: Adrian Wurm

Investigation of reachability problems in neural networks with CSP methods

We analyze verification problems for neural networks such as: Given a description of admissible inputs and outputs as instances of linear programs, is there an admissible input whose output is also admissible? And does this apply to all admissible inputs?
We use the theory of constraint satisfaction problems (CSP) as a framework. We show how our problems can be described using CSPs and how results about decision problems in the context of CSPs are helpful to answer the above network questions for a number of different activation functions.

Thursday, 9.11.2023: Marco Sälzer

Sound and Complete Verification for Safe Deep Learning

The far-reaching success of applications based on neural networks has led to their use in safety-critical areas such as driver assistance systems or applications for early disease detection, which creates the necessity for reliable safety certificates. The utmost goal regarding such certificates would be a somehow efficient sound and complete verification of relevant safety properties. However, the highly parametrized blackbox nature of neural networks makes it difficult to give clear answers under which circumstances this goal is possible.

In this talk, we address this problem from the perspective of complexity and computability. We discuss various decision problems related to the sound and complete verification of neural network (based) models.
Starting with classical feedforward neural networks (FNN), we quickly find that most FNN verification problems are NP- or coNP-complete. For more recent models like Graph Neural Networks (GNN) or Transformers the situation is not quite so clear. We present relevant verification problems of such models that are undecidable, clearly indicating that sound and complete verification can only be achieved in carefully restricted settings. We discuss such settings and present first results and conjectures about corresponding complexity bounds. In the end, we close with a summary of the many open questions that must necessarily be answered to understand the role of sound and complete verification for safe deep learning.

Tuesday, 31.10.2023: Jan Heinemeyer

Hypothesis verification in biology: Extension and connection of the Calculus of Influence to a teaching/learning system for hypothesis verification

The lecture deals with the extension of the teaching/learning system for hypothesis verification (iLL) by the Calculus of Influence (CoI). In this talk, a function for translating hypotheses into Calculus statements will be presented. Furthermore, the limitations of this translation will be discussed and an insight into possible extensions of the hypotheses will be given. Finally, the structured process for setting up an experiment will be presented.

Thursday, 12.10.2023: Jana Klitzsch

Certifiable Adversarial Robustness for GNNs

Verification is needed to ensure that machine learning methods are safe. Graph Neural Networks (GNNs) include different models for either node or graph classification. The goal of adversarial robustness verification is to certify, given the network and graphs, whether 'similar' graphs are classified in the same way. There are different definitions for similarity in graphs. There are different types of certificates, each with advantages and disadvantages. A specific white-box certificate is presented in more detail, which uses linear programming.

Thursday, 28.9.2023: Eric Alsmann

On the Undecidability of the Output Reachability Problem for Transformer Sequence Classifiers

Transformer models have revolutionized natural language processing, achieving remarkable performance in a variety of tasks. However, as they become increasingly integral to critical applications, ensuring their reliability and trustworthiness is becoming more and more important.
This thesis addresses the challenging problem of verifying transformer models. We establish the undecidability of the output reachability problem for transformer sequence classifiers, highlighting the complexities arising from their massive parameter counts and complex structures. We also show that a restricted version of this problem is NP-complete, and discuss another decidability result for models with limited precision.

Tuesday, 5.9.2023: Laurin Pöppe

Formalization of a correctness proof in the context of NN-verification in Isabelle/HOL

In the project, a formalization for neural networks in the theorem prover Isabelle/HOL was developed.
This was used to verify the correctness of a reduction of 3-SAT to the reachability problem of neural networks, from which it follows that this reachability problem is NP-hard.
The talk will discuss the approach and the problems as well as solutions in the implementation of the project and finally discuss a recently published, different implementation of neural networks in Isabelle/HOL.

Thursday; 17.8.2023: Lukas Mentel

IC3 / PDR meets SMT-LIB

Bounded model checking in conjunction with k-induction is often used for symbolic model checking. IC3 ("Incremental Construction of Inductive Clauses for Indubitable Correctness") [1] represents an alternative to this approach and is certainly one of the most important innovations in this area in the last 15 years [2].
As the name implies, a set of formulas is modified step by step in order to obtain a (1-inductive) invariant.
In this presentation, an overview of IC3 and its variant PDR will be given. In addition, an implementation approach based on the SMT-LIB standard will be presented.

[1] Bradley, A.R. (2011). SAT-Based Model Checking without Unrolling.
In: Jhala, R., Schmidt, D. (eds) Verification, Model Checking, and
Abstract Interpretation. VMCAI 2011. Lecture Notes in Computer Science,
vol 6538. Springer, Berlin, Heidelberg.
doi.org/10.1007/978-3-642-18275-4_7
[2] N. Een, A. Mishchenko and R. Brayton, "Efficient implementation of
property directed reachability," 2011 Formal Methods in Computer-Aided
Design (FMCAD), Austin, TX, USA, 2011, pp. 125-134.

Thursday, June 1, 2023: Georg Sieberg

GeNNifier - Verification on Graph Neural Networks (GNNs)

Verification of neural networks (NNs) can be used to ensure that they fulfill certain specifications. A subgroup of NNs are graph neural networks (GNNs), which accept graphs as input. Although there are individual verification algorithms for the verification of GNNs, they do not use a standardized format to work on GNNs. A standardized format for NNs is the Open Neural Network Exchange (ONNX) format. This makes it possible to display NNs independently of common machine learning (ML) frameworks (e.g. Pytorch or Tensorflow). However, the ML frameworks do not fully support the export of GNNs to ONNX. Furthermore, structural information is lost when exporting the GNN.
The aim of the master project is to develop a tool that creates an ML framework-independent representation, which should serve as a basis for verification procedures of GNNs. The Python tool "GeNNifier" was developed for this purpose. This offers a high-level representation of GNNs based on JSON, which can be used to create configurations of GNNs. Such a configuration can be read by "GeNNifier" and processed further via an interface in a verification algorithm.
The Naive Output Reachability Verification (NORV) algorithm was implemented in "GeNNifier" in order to test the usability of "GeNNifier" for verification procedures. This method works on Message Passing Neural Networks (MPNN), which are a form of GNNs.
The NORV algorithm converts an MPNN into several Feedforward NNs (FNN). A verification procedure for the output reachability problem is then successively applied to the FNNs created until a solution is found. The implementation in "GeNNifier" covers the algorithm up to the conversion of the MPNN into an FNN. The generated FNNs are output in ONNX format to support the widest possible number of verifiers.

Thursday, 25.5.2023: Eric Alsmann

An introduction to the architecture of transformer models and the limits of associated verification problems

Motivated by the success of generative language models such as GPT and Bard, my master thesis deals with theoretical limits in the verification of such models. The talk gives an introduction to the architecture of transformer models and the concept of self-attention.
Subsequently, different verification problems for transformers and their decidability will be discussed.
No special prior knowledge is required for the lecture.

Wednesday, 3.5.2023: John Hundhausen

A website construction kit for interactive lecture notes and worksheets

Modern web technologies make it possible to provide interactive visualizations, various exercises and even exercises that are automatically corrected as additional learning tools for students. In the Department of Theoretical Computer Science/Formal Methods, precisely this type of learning tool is being developed in various projects. Now these are not to be offered additionally, but integrated directly into the lecture notes and worksheets.
In order to investigate how exactly this can be implemented technically and conceptually, we have developed a prototype for a website construction kit for interactive lecture notes and worksheets. A special feature of the prototype is that new and existing learning tools can be easily added through a flexible plugin system.

Wednesday, 8.2.2023: Clemens Weiße

Frontend development of a reduction trainer for students

Clemens describes the reduction trainer, its components belonging to the frontend, the associated database and the communication between all components of the reduction trainer. He then demonstrates its use by way of example.

Thursday, 2.2.2023, Marco Sälzer

Expressibility of Graph Neural Networks Through the Lens of Formal Verification

In this talk I will give a brief overview of recent results on the expressive power of graph neural networks (GNN), neural models that compute functions over graphs. I will also relate these results to recent work by Martin Lange and myself on formal verification of GNN.

Thursday, 26.1.2023: Kathrin Lehmann

Tool-based learning in the context of computability theory: a backend prototype for automated verification of reductions

Thursday, 1/19/2023: Lars-Eric Marquardt

Formal Verification of Different Semantics for an Abstract Higher-Order Fixpoint Algebra in Isabelle/HOL

The topic of the thesis was the formal verification of different semantics for an abstract higher-order fixpoint algebra in Isabelle/HOL. Three different semantics for this algebra should be formalized and the equivalence of two of these semantics in Isabelle/HOL should be proved. Furthermore, it should be outlined to what extent a similar proof could also be given for the equivalence of the third semantics to one of the first two.

Thursday, 12.1.2023: Stefan Kablowski

Computing All Minimal Corrections for a Word to Match a Context-Free Description

The paper investigated how many different ways a given word can be paraphrased in a minimal way so that the result is in a given context-free language. In doing so, the concept of minimality should also be clearly defined.

Thursday, 15.12.2022: Martin Lange

will talk about the now completed proof of completeness in the already known "Calculus of
Influence".

Thursday, 1.12.2022: Janek Bürger

Student submission platform

In the project, a prototype web tool for the submission and automatic evaluation of student homework was created. The tool includes a lecturer page and a student page. On the lecturer side, new tasks with assessment criteria can be created, which are automatically assessed by integrated tools. On the student side, submissions can be made for these tasks. In addition, all submissions and assessments are stored in a database to make them available for statistical surveys, for example, export as a CSV file is available.

Thursday, 24.11.2022: Marco Sälzer

Because humans are bad teachers, neural networks don't understand NP severity!

Motivated by recent results from the field of "Neural Algorithmic Learning", i.e. the learning of classical algorithms by deep learning models, I will present work by Yehuda et al. and Sanchis et al. showing that the way we train neural networks (and ML models in general) leads to the fact that these models cannot learn NP-hard problems (or only pretend to do so). Note: The talk is self-contained, i.e. no special knowledge about machine learning is assumed.

Tuesday, 15.11.2022: Nicolai Fiege

Optimal Modulo Scheduling with SAT Solvers.

Modulo scheduling aims to accelerate loop calculations (for or while loops) by executing successive loop iterations in a nested manner. The first operation from iteration 2 is therefore executed before the last operation from iteration 1 has been completed, and so on. The task of a modulo scheduling algorithm is to assign an execution time to each operation of the loop body so that (1) the execution time of the loop is minimized, (2) data dependencies within the loop and (3) resource constraints are respected. The talk will show how we solve modulo scheduling using Boolean Satisfiability (SAT) solvers.

Thursday,10.11.2022: Luca Hertel

Connection of the FG learning tools to Moodle via LTI interface

Tuesday, 11.10.2022: Sören Möller

An Efficient Algorithm for Proof Search in the Calculus of Influence

The "Calculus of Influence" consists of rules that allow to prove hypotheses about systems that describe the influence of different variables on each other.
The aim of the work is to design an algorithm that uses these rules to prove such a hypothesis about a system. This algorithm should work efficiently, whereby the term "efficiency" is further specified in the thesis. Furthermore, the algorithm is implemented in Python in order to be able to carry out measurements and evaluate the efficiency using real problems. For this purpose, measurement data is used, which can be transformed into scalable systems in order to allow statements about the runtime behavior of the algorithm.

Friday, 14.10.2022: Shahla Rasulzade

On the modeling of biological influence experiments

Experimentation is a well-established learning mechanism in school subjects of natural sciences, for instance biology. For understanding the basics of experimental design and making logically consistent hypotheses, it is expected from pupils to have some background knowledge and concentrate themselves on their thoughts. But interaction with a teacher can distract a group of pupils from the thinking processes they should undergo in designing an experiment.
The introduction of digital learning tools can help to minimize such effects. We are working to create such a tool which can model influence experiments and provide to check their correctness by a simple proof system. I will present our model language and proof rules for influence experiments.

Wednesday, 31.8.2022: Rüdiger Ehlers

Natural Colors of Infinite Words.

While finite automata have minimal DFAs as a simple and natural normal form, deterministic omega-automata do not currently have anything similar. One reason for this is that a normal form for omega-regular languages has to speak about more than acceptance - for example, to have a normal form for a parity language, it should relate every infinite word to some natural color for this language. This raises the question of whether or not a concept such as a natural color of an infinite word (for a given language) exists. We show how the natural color of a word can be defined purely based on an omega-regular language, and show how this natural color can be traced back from any deterministic parity automaton after two cheap and simple automaton transformations. Afterwards, we show how this natural color provides a canonical representation for every ?-regular language.

Tuesday, 5.4.2022: Lars-Eric Marquardt

Isabelle: A theorem prover

Theorem provers are tools that can be used to prove the correctness of programs. Compared to model checkers and SAT solvers, theorem provers offer a high degree of interactivity. "Machine-checked formal proofs lead to reliable programs and are the basis for fully specified mathematics.
This talk will give a small insight into the theorem prover Isabelle.

Thursday, 3.3.2022: Martin Lange

A Proof System for Statements about Influence in Biological Experiments

In biological school experiments, pupils are often required to form hypotheses about the influence relation between variables occurring in these experiments. In the context of our efforts to digitise such experiments, we have created a modelling framework for such experiments and hypotheses where influence is characterised by the existence of partial functions on real numbers. I will present a simple proof system for correctness of hypothesis statements in such experiments. Soundness of this systems seems to be established, but completeness and decidability of proof search are currently open. I will sketch some ideas on how to establish these as well. This is joint work with Shahla Rasulzade.

Thursday, 17.2.2022: Marco Sälzer

Reachability is NP-Complete Even for the Simplest Neural Networks

In this talk, we investigate the complexity of the reachability problem for (deep) neural networks: does it compute valid output given some valid input? It was recently claimed that the problem is NP-complete for general neural networks and conjunctive input/output specifications. We repair some flaws in the original upper and lower bound proofs. We then show that NP-hardness already holds for restricted classes of simple specifications and neural networks with just one layer, as well as neural networks with minimal requirements on the occurring parameters.

Thursday, 16.12.2021: Shahla Rasulzade

Modeling biological experiments

Our study is about the creation of a digital learning tool which can model a particular kind of experiments in school subjects of natural sciences, like biology. It is developed by using formal methods.
Our aim is to provide two frameworks for formal modeling, in other words to develop two different experiment models. The first one is an axiomatic approach, where the correctness of hypotheses is reduced to the problem of proof search. The second one is concerned with operational approach, where the correctness of hypotheses is reduced to model checking.

Wednesday, 24.11.2021: Martin Lange

Temporal Logic with Recursion

We introduce extensions of the standard temporal logics CTL and LTL with a recursion operator that takes propositional arguments. Unlike other proposals for modal fixpoint logics of high expressive power, we obtain logics that retain some of the appealing pragmatic advantages of CTL and LTL, yet have expressive power beyond that of the modal μ-calculus or MSO. We advocate these logics by showing how the recursion operator can be used to express interesting non-regular properties. We also study decidability and complexity issues of the standard decision problems.

Wednesday, 10.11.2021: Maurice Herwig

Calculation of a weighting of regular languages

Results of his bachelor thesis

Thursday, 9.9.2021: Eric Alsmann

Inexpressibility Results for Propositional Dynamic Logic over Context-Free Programs

This thesis compares the expressibility of PDL over regular, visibly-pushdown and context-free languages, as well as the modal fixed-point logic vpFLC. Visibly Pushdown Fixpoint Logic with Chop (vpFLC) is a newly introduced decidable modal fixpoint logic that can express non-regular properties. It is shown constructively, using a concrete property, that vpFLC is genuinely more expressive than PDL over visibly-pushdown languages. Furthermore, the different PDL-based logics are constructively separated from each other. Finally, an overview of the different logics and their expressive power is given.

Thursday, 9.9.2021: Georg Siebert

On the way to the artificial teaching assistant: Learning grading schemes for finite automata with GNNs

In this talk, we investigate to what extent deep learning techniques are able to grade student homework assignments. Specifically, we consider the following question: Can we model a multi-valued homework grading scheme for the topic "non-deterministic finite automata" using neural networks? We present the graph neural network model suitable for this task and describe the process from the definition of an evaluation scheme and the formulation of a suitable classification task to the design and execution of corresponding experiments. Finally, we discuss our results for a concrete such homework assignment and give an outlook on possible next steps.

Monday, 5.7.2021: Lukas Mentel

Detection and Elimination of Constants to Strengthen k-Induction

A major problem when using formal methods in practice is the great complexity of the verified systems. By simplifying the input for model checkers and similar tools, the time required can be significantly reduced. In this paper, a technique is described to identify variables that have a constant value and thereby speed up the verification process.

Friday, 19.3.2021: Marco Sälzer

On Finite Convergence of the Modal Mu-Calculus

In this talk we investigate a word-structure with infinite bisimulation quotient that guarantees finite convergence of all fixpoints definable in the modal mu-calculus. The talk does not require too much background in this area of research as we focus on understanding the result, why it is of interest and what its implications for the modal mu-calculus are. Furthermore, we take a short look at how to prove this finite convergence property and encourage a discussion to gain deeper insights.

Thursday, 5.3.2020: Martin Lange

Existential Length Universality

We study the following natural variation on the classical universality problem: given a language L(M) represented by M (e.g., a DFA/RE/NFA/PDA), does there exist an integer l ≥ 0 such that Sigma^l ⊆ L(M)?
In the case of an NFA, we show that this problem is NEXPTIME-complete, and the smallest such l can be doubly exponential in the number of states. This particular case was formulated as an open problem in 2009, and our solution uses a novel and involved construction.
In the case of a PDA, we show that it is recursively unsolvable, while the smallest such l is not bounded by any computable function of the number of states.
In the case of a DFA, we show that the
problem is NP-complete, and e^sqrt( n log n)(1+o(1)) is an asymptotically tight upper bound for the smallest such l, where n is the number of states.
Finally, we prove that in all these cases, the problem becomes computationally easier when the length l is also given in binary in the input: it is polynomially solvable for a DFA, PSPACE-complete for an NFA, and co-NEXPTIME-complete for a PDA.

Wednesday, 5.2.2020: Stefan Göller

Stefan will continue his talk"On regularity of pushdown automata and related problems"

Wednesday, 22.1.2020: Stefan Göller

On regularity of pushdown automata and related problems

I will introduce a few problems on pushdown automata I am and have been working on. On particular, I plan to discuss in more depth a recent result with Pawel Parys: The problem if a pushdown system is bisimulation equivalent to some (unspecified) finite system is elementarily decidable, improving a previously known Ackermann upper bound. The plan is to give two black board talks on this topic.

Friday, 22.11.2019: Martin Lange

From the modal mu-calculus to HFL

I will outline the development of fixpoint logics with expressive power beyond the modal mu-calculus, including Fixpoint Logic with Chop (FLC), Non-regular Propositional Dynamic Logic, and Higher-Order Fixpoint Logic.

Friday, 25.10.2019: Marco Sälzer

will give a short talk about an on-the-fly model checking algorithm for HFL.

Friday, 18.10.2019: Adrian Sturm

will present the results of his master thesis.

Monday, 02.09.2019: Benedikt Hruschka

Implementation of an Interactive Model Checker for First-Level Logic over Automatic Structures

will present the results of his master thesis.

Tuesday, 16.07.2019: Marco Sälzer

The question whether there are modal logic formulas, with a closure ordinal greater than omega was investigated by Marek Czarnecki. Here we recapitulate his work, focusing on creating a general understanding of how to build formulas with closure ordinal between omega and omega * 2. Furthermore, some related work is discussed to place the topic in current research.

Friday, 08.03.2019: Lars Marquardt and Lukas Mäntel

We will listen to two 30-minute talks by Lars Marquardt and Lukas Mäntel. Lars Marquardt will give a talk on "Brzozowski's derivatives" and Lukas Mäntel on "Quantifier elimination".

Friday, 18.01.2019: David Kronenberger

David Kronenberger will present the results of his Master's thesis titled "Capturing Bisimulation-Invariant Complexity Classes by Polyadic Higher-Order Fixpoint Logic" in an accompanying Colloquium.

Friday, 02.11.2018: Lara Yörük

Proposal for a modeling language for scientific experiments

The aim of my dissertation is to develop a framework for modeling various scientific experiments, which is to be used in schools.
The first step is to find a mathematical modeling language that can be used to create "modular" experiments. A hybrid system is to be generated from the created model to define the semantics of the experiments. I would like to present a proposal for such a modeling language for discussion in this talk.

Friday, 07.09.2018: Martin Lange

Martin will present a small tool for the upcoming logic course

Friday, 31.08.2018: Marco Sälzer

Neededness Analysis for Model Checking Properties Defined by Order-2 Fixpoints

Higher-Order Fixpoint Logic (HFL) extends the modal mu-calculus by a simply typed lambda calculus, and thus is able to express non-regular properties. In this talk, we present a model-checking algorithm for the second-order fragment HFL2, which achieves computational benefits by adopting neededness analysis. Furthermore, we will discuss optimizations of an actual implementation and currently existing drawbacks in the efficiency of the algorithm.

Tuesday, 03.07.2018: Florian Bruse

Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic

Higher-Order Fixpoint Logic (HFL) is an extension of the modal mu-calculus by a typed lambda calculus. As in the mu-calculus, whether the nesting of least and greatest fixpoints increases expressive power is an important question. It is known that at low type theoretic levels, the fixpoint alternation hierarchy is strict. We present classes of structures over which the alternation hierarchy of HFL-formulas at low type level collapses into the alternation-free fragment, albeit at increase in type level by one.

Friday, 13.04.2018: Florian Bruse

Fixed point stabilization on certain structure classes

In the course of our investigations on structure classes on which HFL fixed point definitions become stable after finitely many steps, it has turned out that the characterization of these class(es) is not so simple. We know that all structures with finite bisimulation quotient have this property, and we conjecture that for fixed maximal type-theoretic order, there exist genuinely larger classes on which all fixed points up to this order become stable after finitely many steps, but fixed points of higher order do not necessarily.
I will briefly say something about the context and then give a fixed structure of which we conjecture that all fixed points in formulas of modal my-calculus become stable after finitely many steps, but of which we know that there is an HFL[1] formula that only becomes stable from step omega.

Friday, 16.03.2018: Martin Lange

A small observation on the automata-theoretic decidability proof for Presburger arithmetic

Friday, 16.02.2018: Norbert Hundeshagen

Conjunctive grammars over one-element alphabets generate non-regular languages

Conjunctive grammars are an extension of context-free grammars by an explicit conjunctive operator. It is known that context-free grammars generate exactly the regular languages via one-element alphabets. It is reasonable to assume that this is also true for conjunctive grammars. In the talk, a result of A. Jez will show that the language {a^4^n | n>0} can be generated by a conjunctive grammar.

Friday, 01.12.2017: Florian Bruse

Fixed point alternation for HFL

A central question for fixed point logics is whether reciprocal entanglement of smallest and largest fixed points offers real added value or can always be eliminated. Fixed point alternation makes formulas notoriously difficult to understand and the model checking problem for the modal mü calculus, for example, contains the degree of alternation of a formula as input. For the mü calculus, for example, we know that it is generally not possible to remove fixed point alternation, but it is possible to remove it above the class of word structures.
In this talk, I will briefly introduce the topic and present the state of research on higher-order modal fixed point logic.

Friday, 01.12.2017: Daniel Kernberger

I will give a short talk about some work in progress and preliminary results on Ehrenfeucht-Fraissé games for Hybrid Branching-Time Logics.

Thursday, 02.11.2017: Etienne Lozes

Synchronizability of Communicating Finite State Machines is not Decidable

A system of communicating finite state machines is synchronizable [1,2] if its send trace semantics, i.e. the set of sequences of sendings it can perform, is the same when its communications are FIFO asynchronous and when they are just rendez-vous synchronizations. This property was claimed to be decidable in several conference and journal papers [1,2,3,4] for either mailboxes (all to 1) or peer-to-peer (one to one) communications, thanks to a form of small model property. We show that this small model property does not hold neither for mailbox communications, nor for peer-to-peer communications, therefore the decidability of synchronizability becomes an open question. We will close this question for peer-to-peer communications, and we will show that
synchronizability is actually undecidable.
This is a joint work with Alain Finkel. A draft version of the paper is available at https://arxiv.org/abs/1702.07213

Friday, 29.09.2017: Daniel Kernberger

The Fully Hybrid μ-Calculus

We consider the hybridization of the μ-calculus through the addition of nominals, binder and jump. Especially the use of the binder differentiates our approach from earlier hybridizations of the μ-calculus and also results in a more involved formal semantics. We then investigate the model checking problem and obtain ExpTime-completeness for the full logic and the same complexity as the modal μ-calculus for a fixed number of variables. We also show that this logic is invariant under hybrid bisimulation and use this result to show that - contrary to the non-hybrid case - the hybrid extension of the full branching time logic CTL∗ is not a fragment of the fully hybrid μ-calculus.

Friday, 22.09.2017: Orcun Yörük

Simon - A simulation tool for hybrid systems

This master thesis is about the simulation of hybrid systems. Hybrid systems describe both discrete and continuous behavior. Therefore, they are well suited for modeling state-based scenarios that are related to time. In order to simulate such systems, a tool was developed as part of this thesis using the platform-independent Java programming language, which represents the theoretical knowledge gained in a practical implementation. The resulting tool, called Simon, allows the correct simulation of hybrid systems.

Friday, 15.09.2017: Lara Yörük

SoPHY - A specification language for hybrid systems

This work contributes to the three topics of hybrid systems, modeling languages and educational software. The specification language for hybrid systems, SoPHY, is being developed. The aim of this language is to describe scientific experiments. These experiments are modeled in the form of hybrid automata. A simulation tool can then be developed on the basis of SoPHY, which is geared towards didactic use in the field of self-directed learning.

The specification language is easy to read and self-explanatory due to its close resemblance to experiments. It is also easy to process by computer, as its structure is adapted to the familiar JSON format. This facilitates its later use in software.

Friday, 01.09.2017: Milka Hutagalung

Topological Characterization of Multi-Buffer Simulation

Multi-buffer simulation is an extension of simulation pre-order that can be used to approximate inclusion of languages recognized by Büchi automata up to their trace closures. It has been shown that multi-buffer simulation with unbounded buffers can be characterised with the existence of a continuous function f that witnesses trace closure inclusion. In this paper, we show that such a characterization can be refined to the case where we only consider bounded buffers by requiring the function f to be Lipschitz continuous. This characterization only holds for some restricted classes of automata. One of the automata should only produce words where each letter does not commute unboundedly to the left or right. We will show that such an automaton can be characterised with a cyclic-path-connected automaton, which is a refinement of a syntactic characterization of an automaton that has a regular trace closure.

Friday, 25.08.2017: Florian Bruse

Space-Efficient Fragments of Higher-Order Fixpoint Logic

Higher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power reaches far beyond that of Monadic Second-Order Logic, achieved through an incorporation of a typed λ-calculus into the modal μ-calculus. Its model checking problem on finite transition systems is decidable, albeit of high complexity, namely k-EXPTIME-complete for formulas that use functions of type order at most k > 0. In this paper we present a fragment with a presumably easier model checking problem. We show that so-called tail-recursive formulas of type order k can be model checked in (k-1)-EXPSPACE, and also give matching lower bounds. This yields generic results for the complexity of bisimulation-invariant non-regular properties, as these can typically be defined in HFL.

Friday, 18.08.2017: Martin Lange

Model Checking CTL over Restricted Classes of Automatic Structures

Interpreting formulas over infinite-state relational structures whose states are words over some alphabet and whose relations are recognized by transducers is known under the term "automatic structures" in the world of predicate logic, or as "regular model checking" in formal verification. Both approaches use synchronized transducers, i.e. finite automata reading tuples of letters in each step. This is a strong transducer model with high expressive power leading to undecidability of model hecking for any specification language that can express transitive closure.

We develop conditions on a class of binary word relations which are sufficient for the CTL model checking problem to be computable over the class of automatic structures generated by such relations. As an example, we consider recognizable relations. This is an interesting model from an algebraic point of view but it is also far less expressive than those given by synchronized transducers. As a consequence of the weaker expressive power we obtain that this class satisfies the aforementioned sufficient conditions, hence we obtain a decidability result for CTL model checking over a restricted class of infinite-state automatic structures.

Friday, 21.07.2017: Norbert Hundeshagen

Kleene's theorem and (at least) one monoid on which it does not hold

Friday, 14.07.2017:

Parity games

Martin Lange - Positional determinacy of parity games

Denis Huseljic - Solving parity games by reduction to SAT

Marco Sälzer - Discrete strategy improvement

Florian Bruse - The fixed point iteration algorithm

Friday, 05.05.2017: Georg Zetsche

Boolean closed full trios and rational Kripke frames

It is a well-known phenomenon that languages classes induced by infinite-state systems usually lack decidability and closure properties that make regular languages pleasant to analyze. Most notably, nondeterministic infinite-state systems typically fail to be closed under Boolean operations. In visibly pushdown automata, one has closure under Boolean operations, but at the expense of restricting the employed input alphabets, meaning they are not closed under rational transductions.

This raises the question of whether there is some type of infinite-state system that enjoys closure under Boolean operations and rational transductions (and permits decidability of, say, the emptiness problem).

This talk demonstrates that this is not the case. It is shown that every language class that contains any non-regular language and is closed under Boolean operations and rational transductions already contains the whole arithmetic hierarchy (which significantly extends the recursively enumerable languages).

Wednesday, 29.03.2016: Arno Ehle

Automatisierte Beweise im Sequenzenkalkül-Trainer

The presentation "Automated Proof Search for the Sequent Calculus Trainer" summarizes the results of the Master Thesis "Proof Search in the Sequent Calculus for First-Order Logic with Equality" by Arno Ehle. The Sequent Calculus Trainer is a program that is designed to support students in studying the sequent calculus. As an introduction, we will shortly demonstrate the Sequent Calculus Trainer, the feature set of it in the past and what was still missing to support student even better. The main part of the presentation is about the automated proof search. We will discuss the most important problems for doing automated proof search in the sequent calculus and show some solutions used in the master thesis. The last part is a live demonstration of the Sequent Calculus Trainer, where we present the new features that are base on the results of the master thesis.

Friday, 24.02.2016: Thao Nguyen

Formal verification of mobile robot protocols

Mobile robot networks emerged in the past few years as a promising distributed computing model. Existing work in the literature typically ensures the correctness of mobile robot protocols via ad hoc handwritten proofs, which, in the case of asynchronous execution models, are both cumbersome and error-prone. The authors propose a formal model to describe mobile robot protocols operating in a discrete space i.e., with a finite set of possible robot positions, under synchronous and asynchronous assumptions. The authors translate this formal model into the DVE language, which is the input format of the model-checkers DiVinE and ITS tools, and formally prove the equivalence of the two models. They then verify several instances of two existing protocols for variants of the ring exploration in an asynchronous setting: exploration with stop and perpetual exclusive exploration. For the first protocol they refine the correctness bounds and for the second one they exhibit a counterexample. For the second one, I also use the UPPAAL model checking tool to re-verify.

Friday, 04.11.2016: Kent Kwee

Ordered Restarting Automata: The Benefit of Patterns

While (stateless) deterministic ordered restarting automata accept exactly the regular languages, it is known that nondeterministic ordered restarting automata accept some languages that are not even growing context-sensitive.
In fact, the class of languages accepted by these automata is an abstract family of languages that is incomparable to the (deterministic) linear languages, the (deterministic) context-free languages, and the growing context-sensitive languages with respect to inclusion, and the emptiness problem is decidable for these automata. These results were derived using a Cut-and-Paste Lemma for nondeterministic ordered restarting automata that is based on Higman's theorem.
Here we extend the arguments used in that proof and introduce a new approach to actually derive a real Pumping Lemma for these automata. Based on this Pumping Lemma we then prove that the finiteness problem is also decidable for these automata, and that the only unary languages these automata accept are the regular ones.
Finally, we present a new and simplified proof for the fact that stateless ordered restarting automata only accept regular languages.

Friday, 15.07.2016: Daniel Kernberger

Model Checking for the Full Hybrid Computation Tree Logic

We consider the hybridizations of the full branching time logic CTL∗ through the addition of nominals, binders and jumps. We formally define three fragments restricting the interplay between hybrid operators and path formulae contrary to previous proposals in the literature which ignored potential problems with a formal semantics. We then investigate the model checking problem for these logics obtaining complexities from PSPACE-completeness to non-elementary decidability.

Friday, 08.07.2016: Qichao Wang

Weighted Restarting Automata as Language Acceptors

We use weighted restarting automata to define classes of formal languages by combining the acceptance condition of a restarting automaton with a condition on the weight of its accepting computations.
Specifically, we consider the tropical semiring and the semiring of regular languages over some finite alphabet. We show that by using the tropical semiring, we can avoid the use of auxiliary symbols.
Further, a certain type of (word-)weighted restarting automata turns out to be equivalent to non-forgetting restarting automata, and another class of languages accepted by (word-)weighted restarting automata is shown to be closed under intersection.

Friday, 01.07.2016: Kent Kwee

Ordered RRWW-Automata

It is known that the deterministic ordered restarting automaton accepts exactly the regular languages, while its nondeterministic variant accepts some languages that are not even growing context-sensitive.
Here we study an extension of the ordered restarting automaton, the so-called ORRWW-automaton, which is obtained from the previous model by separating the restart operation from the rewrite operation.
First we show that the deterministic ORRWW-automaton still characterizes just the regular languages. Then we prove that this also holds for the stateless variant of the nondeterministic ORRWW-automaton, which is obtained by splitting the transition relation into two parts, where the first part is used until a rewrite operation is performed, and the second part is used thereafter. Finally, we show that the nondeterministic ORRWW-automaton is even more expressive than the nondeterministic ordered restarting automaton.

Friday, 17.06.2016: Milka Hutagalung

Buffered Simulation Games

We consider simulation games played between Spoiler and Duplicator on two Büchi automata in which the choices made by Spoiler can be buffered by Duplicator in several buffers before she executes them on her structure. We show that they are useful to approximate the inclusion of trace closures of languages accepted by finite-state automata, which is known to be undecidable. We study the decidability and complexity and show that the game with bounded buffers can be decided in polynomial time, whereas the game with one unbounded and one bounded buffer is highly undecidable. If time permits, we also give a topological characterization of the games using the notion of continuous and Lipschitz continuous function.

Friday, 03.06.2016: Florian Bruse

Alternating Krivine Automata

Alternating Parity Krivine Automata (APKA) provide operational semantics to Higher-Order Modal Fixpoint Logic (HFL). APKA consist of ordinary parity automata extended by a variation of the Krivine Abstract Machine. We study their construction and show how any HFL-formula can be converted into an APKA. Time permitting, we also sketch hoe the number and parity of priorities available to an APKA form a proper hierarchy of expressive power as in the modal µ-calculus, which also induces a strict alternation hierarchy on HFL.

Friday, 15.04.2016: Martin Lange

Higher-Order Fixpoint Logic

Higher-Order Fixpoint Logic (HFL) is an extension of the modal mu-calculus by higher-order features, syntactically represented using a simply typed lambda calculus. Its formulas of order 0 form the modal mu-calculus and express properties of states in a transition system, i.e. predicates. Its formulas of order 1 express predicate transformers, i.e. mappings from predicates to predicates. Monotone predicate transformers form a complete lattice over any transition systems, thus a denotational semantics for fixpoint formulas over predicate transformers can be given. This principle easily extends to functions of higher order.
We will introduce the syntax and semantics of HFL and give some examples of properies expressible in HFL (but not in the mu-calculus) thus trying to give some intuition on how such formulas can be read and understood. We will survey some results known about the expressive power and complexity of HFL, most importantly that the model checking problem for the order-k fragment is complete for k-EXPTIME.

Friday, 27.11.2015: Martin Lange

LTL with Past: Expressiveness and Succinctness

We consider the linear-time temporal logic LTL enriched with temporal operators for the past, for example "since", "always in the past", "yesterday" etc.. A natural question concerns its expressive power compared to future-only LTL (which is known to be equi-expressive to first-order logic or star-free languages). We present Gabbay's Separation Theorem from which equi-expressiveness between LTL and LTL+Past on infinite words follows immediately.
The next question that arises with equi-expressive languages is that of succinctness: Gabbay's Separation Theorem gives a computable tranformation of formulas of LTL+Past to LTL which incurs a non-elementary blow-up. This indicates that some properties can be expressed more succinctly in LTL+Past than in LTL. On the other hand, it is known that satisfiability for both is just PSPACE-complete (which indicates that such a succinctness gap is, if it exists, not straight-forward to show). We then present a clever argument by Laroussinie/Markey/Schnoebelen who proved the existence of an exponential succinctness gap between LTL+Past and LTL.

Thursday, 17.11.2015: Jörg Kreiker

Java Generics

Thursday, 18.06.2015: Maxime Folschette

Some Methods and Results on Biological Regulatory Networks

Biological Regulatory Networks (BRNs) are a wide class of qualitative models used to represent biological processes. Since their formalization (Kauffman, 1969 & Thomas, 1973) some interesting methods have emerged, leading to well-known results in this domain. During this seminar, I will present some of the main results discovered on these models, while gradually focusing on my field of research, related to the use of formal methods to study the dynamics of BRNs.

Thursday, 11.06.2015: Kent Kwee

On Some Decision Problems for Stateless Deterministic Ordered Restarting Automata

Stateless deterministic ordered restarting automata accept exactly the regular languages, and it is known that the trade-off for turning a stateless deterministic ordered restarting automaton into an equivalent DFA is at least double exponential.
Here we show that the trade-off for turning a stateless deterministic ordered restarting automaton into an equivalent unambiguous NFA is exponential, which yields an upper bound of $2^{2^{O(n)}}$ for the conversion into an equivalent DFA, thus meeting the lower bound up to a constant. Based on the new transformation we then show that many decision problems, such as emptiness, finiteness, inclusion, and equivalence, are PSPACE-complete for stateless deterministic ordered restarting automata.

Wednesday, 28.05.2015: Norbert Hundeshagen

Sequent Calculus Trainer

We present the Sequent Calculus Trainer, a tool that supports students in learning how to correctly construct proofs in the sequent calculus for first-order logic with equality. It is a proof assistant fostering the understanding of all the syntactic principles that need to be obeyed In constructing correct proofs.
We also report on some empirical findings that indicate how the Sequent Calculus Trainer can improve the students' success in learning sequent calculus for full first-order logic.

Wednesday, 29.04.2015: Arno Ehle

Parity Games

This lecture deals with algorithms for parity games based on partial reductions to Büchi games. The term partial refers on the one hand to how much information can be obtained from the solution of a Büchi game and on the other hand to the principle of reduction itself. Three different approaches are explained in this regard. The first approach enables a partial reduction to Büchi games by rolling out cycles in sub-games, whereby a new game is generated in each case that has one less priority. The second and third approaches extend the Büchi algorithm with recursive calls on genuinely smaller subgames and solve the actual parity game by calling this extended Büchi algorithm several times. All algorithms were implemented in the project PGSolver and compared with each other on different game families.

Wednesday, 22.04.2015: Martin Lange

Language Inclusion

Deciding language inclusion between finite or Büchi automata is PSPACE-complete and therefore too complex for some practical purposes. One approach to circumvent the high complexity is to use simulation instead. It approximates language inclusion in the sense that simulation implies it but not vice-versa. On the other hand, simulation between finite or Büchi automata can be computed in polynomial (e.g. quadratic) time. Hence, simulation offers a decent alternative approach to solving language inclusion by trading in precision for efficiency.
In this talk we consider the case for a larger class of automata, namely visibly pushdown automata. Note that language inclusion is undecidable or pushdown automata but EXPTIME-complete for visibly pushdown automata. We show that here the situation is dramatically different: simulation is of course still just an approximation to language inclusion; however, it is also EXPTIME-complete.
This is joint work with Milka and Etienne.

Wednesday, 11.02.2015: Martin Lange

Model Checking for String Problems

Model checking is a successful technique for automatic program verification. We show that it also has the power to yield competitive solutions for other problems. We consider three computation problems on strings and show how the polyadic modal μ-calculus can define their solutions. We use partial evaluation on a model checking algorithm in order to obtain an efficient algorithm for the longest common substring problem. It shows good performance in practice comparable to the well-known suffix tree algorithm. Moreover, it has the conceptual advantage that it can be interrupted at any time and still deliver long common substrings.

Wednesday, 04.02.2015: Nobert Hundeshagen

A Hierarchy of Transducing Observer Systems

We mainly investigate the power of weight-reducing string-rewriting systems in the context of transducing observer systems. First we relate them to a special type of restarting transducer. Then we situate them between painter and length-reducing systems. Further we show that for every weight-reducing system there is an equivalent one that uses only weight-reducing painter rules. This result enables us to prove that the class of relations that is computed by transducing observer systems with weight-reducing rules is closed under intersection.

Wednesday, 28.01.2015: Arno Ehle

Model Checker

In this lecture, the project "Model Checker" will be presented, with reference to the task, the implementation and the results. The program "Model Checker" offers the possibility to interactively learn and deepen the connection between formulas of first-level predicate logic and their interpretations. A live demo is integrated into the lecture, which can incorporate suggestions from the audience.

Wednesday, 14.01.2015: Florian Bruse

The Canonical Model Technique for Modal Logic

Canonical models are a standard technique to establish completeness of a proof calculus for a modal logic. Successful construction of a canonical model implies compactness of the logic in question. We have a look at the technique for basic modal logic and how it has to be extended for some extensions, e.g., a fragment of PDL with intersection. If there is time, we also look how a similar technique works for non-compact logics.

Wednesday, 17.12.2014: Kent Kwee

On the Number of Roots of a Polynomial of Spanning Trees of a Graph

In this talk we introduce a polynomial associated to graphs and determine the number of roots over F_q. M. Kontsevich conjectured that this number is a polynomial in q, i.e. a polynomial in q independent of the characteristic p of the field F_q. This conjecture is wrong and we will present several methods for determining this number to see in which case it is a polynomial and in which it is not.

Wednesday, 10.12.2014: Maxime Folschette

Process Hitting

The representation and analysis of biological regulatory networks can be tackled with formal methods. My work focuses on the use and enrichment of the expressivity of the Process Hitting, a recently introduced formalism that allows to study large models (up to hundreds of components). This framework especially comes with an efficient reachability analysis which avoids the usual combinatorial explosion of the state graph computation.

Wednesday, 26.11.2014: Martin Lange

The strictness of the mu-calculus alternation hierarchy over the class of all structures

In this last talk on the modal mu-calculus we will show that the alternation hierarchy is in general strict, i.e. more fixpoint alternation yields more expressive power. Remember that on some classes of structures like finite or infinite words for example this is not the case.
The result was first established by Bradfield in 1996, and also independently by Lenzi in that year as well. The proof presented in this seminar is Arnold's - particularly nice one - from 1999 using Banach's Fixpoint Theorem. So most of the seminar will be spent talking about basic topology, namely complete metric spaces etc. The actual proof of the alternation hierarchy is then a simple diagonalization argument using the Fixpoint Theorem and the Walukiewicz formulas that express whether or not an arbitrary mu-calculus formula of bounded alternation holds on a given structure.

Wednesday, 19.11.2014: Stéphane Demri

Verification of Linear-Time Properties on Flat Counter Systems

Flat counter systems are integer programs in which the control graph satisfies the so-called flatness condition. Even though in full generality, the verification of integer programs is well-known to be undecidable (even for simple properties) in this talk we show that the model-checking problem for flat counter systems with Past LTL and arithmetical contraints on counters is NP-complete.
The proof technique to get the NP upper bound takes advantage of a stuttering theorem for (plain) Past LTL as well as properties about small integer solutions for quantifier-free Presburger formulae.
In time permits, results for extensions of LTL such as ETL, linear mu-calculus or CTL* shall also be discussed.
The talk is based on joint works with Amit Kumar Dhar and Arnaud Sangnier.

Wednesday, 12.11.2014: Martin Lange

The collapse of the mu-calculus alternation hierarchy on certain classes of structures

The goal of this little series on talks about the modal mu-calculus is to understand the phenomenon of fixpoint alternation. In this talk we will show that the alternation hierarchy collapses on certain classes of structures, namely those with no infinite paths and words. I.e. every formula is equivalent over such structures to one with "very little" fixpoint alternation.
The main motivation for such results is drawn from the two facts that fixpoint alternation
- makes it difficult to understand the properties expressed by formulas, and
- mainly determines the complexity of model checking: the currently best
algorithms are polynomial in the size of the structure and formula but exponential in its alternation depth.

Wednesday, 05.11.2014: Florian Bruse

The Fixpoint-Iteration Algorithm for Parity Games

It is known that the model checking problem for the modal μ-calculus reduces to the problem of solving a parity game and vice-versa. The latter is realized by the Walukiewicz formulas which are satisfied by a node in a parity game iff player 0 wins the game from this node. Thus, they define her winning region, and any model checking algorithm for the modal μ-calculus, suitably specialized to the Walukiewicz formulas, yields an algorithm for solving parity games. We study the effect of employing the most straight-forward μ-calculus model checking algorithm: fixpoint iteration. This is also one of the few algorithms, if not the only one, that were not originally devised for parity game solving already. While an empirical study quickly shows that this does not yield an algorithm that works well in practice, it is interesting from a theoretical point for two reasons: first, it is exponential on virtually all families of games that were designed as lower bounds for very particular algorithms suggesting that fixpoint iteration is connected to all those. Second, fixpoint iteration does not compute positional winning strategies. Note that the Walukiewicz formulas only define winning regions; some additional work is needed in order to make this algorithm compute winning strategies. We show that these are particular exponential-space strategies which we call eventually-positional, and we show how positional ones can be extracted from them.

Wednesday, 29.10.2014: Martin Lange

Introduction to the Modal Mu-Calculus

No Abstract

Friday, 12.09.2014 at 14:00: David Kronenberger

Comparing two different classes of deterministic recognizable picture languages

In this talk we compare two different definitions of deterministic recognizable picture languages. Furthermore, we examine closure properties of the corresponding classes of languages. The first definition of deterministic recognizable picture languages uses a domino tiling system to recognize a local picture by a deterministic process. The family of all languages that recognizes a picture in that way is abbreviated with DREC.
The second and completely different definition uses a tiling system to recognize a picture by proceeding from one corner to the diagonally opposite corner. Because of its procedure the class of all these languages are abbreviated with Diag-DREC. We show that Diag-DREC is not closed under intersection and union and DREC is closed under rotation and intersection. Furthermore, we show that the family of all two-dimensional deterministic online tessellation automata is a subset of DREC. Knowing that Diag-DREC is equal to the closure by rotation of the family of all two-dimensional deterministic online tesselation automata, we show that Diag-DREC is a proper subset of DREC.

Wednesday, June 25, 2014 at 10:00 a.m.: Etienne Lozes, University of Kassel

Capturing Bisimulation - Invariant Complexity Classes with Higher-Order Fixpoint Logic.

We consider Polyadic Higher-Order Fixpoint Logic (PHFL), a modal fixpoint logic that is obtained as the merger of Higher-Order Fixpoint Logic and the Polyadic $\mu$-Calculus, two formalisms which were originally introduced as expressive languages for program specification purposes. Polyadicity enables formulas to make assertions about tuples of states rather than states only. From Higher-Order Fixpoint Logic, PHFL inherits the ability to formalize properties using higher-order functions.

We consider PHFL in the setting of descriptive complexity theory: its fragment using no functions of higher-order is exactly the Polyadic $\mu$-Calculus, and it is known from Otto's Theorem that it captures the bisimulation-invariant fragment of the complexity class P. We extend this result by showing that certain other fragments of PHFL capture the bisimulation-invariant fragments of other important complexity classes. We first show that EXPTIME in this sense is captured by the fragment using at most functions of order 1. We also give characterizations of PSPACE and NLOGSPACE by certain formulas of these two fragments which can be regarded as having tail-recursive functions only.

While many characterizations of complexity classes in descriptive complexity theory have been obtained as extensions of logics with low expressive power, the work we present here introduces a logic of very high expressive power and characterizes complexity classes by fragments of this generic framework.

Wednesday, 04.06.2014 at 05:00: Thorsten Löbig

Investigation of the applicability of formal methods using the example of an infusion pump.

Model checking makes it possible to formally prove whether a system is a model of a given specification. It is also potentially possible to show the absence of certain error classes.
However, techniques from this area have so far hardly found their way into modern software development. The main reasons for this are the "state-space explosion" problem and the expert knowledge required to use these tools effectively.
In my bachelor thesis, I investigated the applicability of currently available model checkers in the context of a real large-scale software project (software for an infusion pump). In the talk I will present the results of my work and demonstrate the possibilities and limitations of the investigated model checkers with illustrative application examples.

Wednesday, 14.05.2014 at 10:00 am: Richard Petersen, University of Kassel

Growing Context-Sensitive Matrix Grammars

In the thesis, the matrix languages introduced by the Sironmoney's, are combined with the growing context-sensitive languages. We call this new class of picture languages the class of growing context-sensitive matrix languages. Furthermore, we examine some closure properties and we find out that the class of growing context-sensitive matrix languages is closed under union, column concatenation, column closure, column-morphism, inverse morphism and intersection with regular matrix languages. Thus, this class is an abstract family of matrices.

Wednesday, 07.05.2014 at 10:00 a.m.: Etienne Lozes, University of Kassel

Buffered Simulation Games for Büchi Automata

Simulation relations are an important tool in automata theory because they provide efficiently computable approximations to language inclusion. In recent years, extensions of ordinary simulations have been studied, for instance multi-pebble and multi-letter simulations which yield better approximations and are still polynomial-time computable.
In this paper we study the limitations of approximating language inclusion in this way: we introduce a natural extension of multi-letter simulations called buffered simulations. They are based on a simulation game in which the two players share a FIFO buffer of unbounded size. We consider two variants of these buffered games called continuous and look-ahead simulation which differ in how elements can be removed from the FIFO buffer. We show that look-ahead simulation, the simpler one, is already PSPACE-hard, i.e. computationally as hard as language inclusion itself. Continuous simulation is even EXPTIME-hard. We also provide matching upper bounds for solving these games with infinite state spaces.

Wednesday, April 30, 2014 at 10:00 a.m.: Qichao Wang, M.Sc., University of Kassel

Weighted Restarting Automata

Restarting automata have been introduced to model the linguistic technique of analysis by reduction, which is used for checking the correctness of a sentence of a natural language. In order to study quantitative aspects of restarting automata, we introduce the concept of a weighted restarting automaton. By looking at different semirings and different weight functions, various quantitative aspects of the behavior of restarting automata can be studied. In this presentation I describe the weighted restarting automaton in detail, present some examples, and state a few preliminary results on properties of weighted restarting automata.

Monday, March 24, 2013 at 10:00 a.m.: Daniel Kernberger, Uni Kassel

Weak alternating automata are not that weak

Automata on infinite words are used for specification and verification of nonterminating programs. Different types of automata induce different levels of expressive power, of succinctness, and of complexity. Alternating automata have both existential and universal branching modes and are particularly suitable for specification of programs. In a weak alternating automata the state space is partitioned into partially ordered sets, and the automaton can proceed from a certain set only to smaller sets. Reasoning about weak alternating automata is easier than reasoning about alternating automata with no restricted structure. Known translations of alternating automata to weak alternating automata involve determinization, and therefore involve a double-exponential blow-up. In this paper we describe a quadratic translation, which circumvents the need for determinization, of Büchi and co-Büchi alternating automata to weak alternating automata. Beyond the independent interest of such a translation, it gives rise to a simple complementation algorithm for nondeterministic Büchi automata.

Wednesday, 20.11.2013 at 10:00 am: Dr. Rüdiger Ehlers, Uni Kassel

Synthesis with Identifiers

We consider the synthesis of reactive systems from specifications with identifiers. Identifiers are useful to parametrize the input and output of a reactive system, e.g., to state which client requests a grant from an arbiter, or the type of object that a robot is expected to fetch.
Traditional reactive synthesis algorithms only handle a constant bounded range of such identifiers, although in practice, we might not want to restrict the number of clients of an arbiter or the set of object types handled by a robot a-priori. We first present a concise automata-based formalism for specifications with identifiers. The synthesis problem for such specifications is undecidable. We therefore give an algorithm that is always sound, and complete for unrealizable safety specifications.
Our algorithm is based on computing a pattern-based abstraction of a synthesis game that captures the realizability problem for the specification. The abstraction does not restrict the possible solutions to finite-state ones and captures the obligations for the system in the synthesis game. We present an experimental evaluation based on a prototype implementation that shows the practical applicability of our algorithm.

Monday, 14.10.2013: John McCabe-Dansted (University of Western Australia)

Model Checking for Compositional Models of General Linear Time

We address the problem of model checking temporal formulas with Until and Since over general linear time. General linear time allows us to capture continuous properties in applications such as distributed systems, natural language, message passing and AI modeling of human reasoning. Models are represented using a recently formalized compositional language. This language is closely related to a tableau method for general linear time. Given a model described in our model expression language and a temporal logic formula, the algorithm decides whether the formula is satisfied in the model. Like Linear Temporal Logic (LTL), the problem is PSPACE-complete and the time required is linear in the length of the model. We motivate this result by examining how some Zeno properties can be model checked, such as for a system that needs to interact with a Zeno environment.

Wednesday, 9.10.2013: John McCabe-Dansted (University of Western Australia)

Algorithms and Temporal Logics

Dr John McCabe-Dansted will present an overview of his work on logics for branching time and general linear flows of times. His thesis was on RoCTL*, and extension to the common branching time logic CTL* for reasoning about robustness. RoCTL* is no more expressive than CTL* but is shown to be exponentially succinct. Recent work has been on decision tableau for a weaker logics including BCTL* and Non-Local BCTL*.
The Non-Local tableau is used in ongoing work on automatic verification of rewrite rules with sample applications for crowd-sourcing and automatically generating rewrite rules. Other ongoing research includes a model checker of a recently specified language for expressing models for any satisfiable Real Temporal Logic formula, and potential extensions to Metric Temporal Logic.

Wednesday, 3.7.2013: Michael Falk and Etienne Lozes

Michael Falk: Fixed point iteration for solving parity games

In this talk the results of the bachelor thesis of the same name will be presented.

Etienne Lozes: On Decision Problems for Probabilistic Büchi Automata

This will be a talk based on the slides of Nathalie Bertrand. people.rennes.inria.fr/Nathalie.Bertrand/pba-lsv.pdf. I will try to understand most of that and present it. In short, Probabilistic Büchi Automata are Büchi automata where the non-determinism is replaced by a random choice. An infinite word thus defines a random infinite run. The word is accepted if the probability p that the infinite run is accepting is >0 (or =1, in some variants). We'll see how the class of definable languages compares to Büchi automata and which decision problems are decidable for this automaton model.

Wednesday, 27.03.2013, 11:30 am, Room WA1318: Milka Hutagalung (Uni Kassel)

Revealing vs. Concealing: More Simulation Games for Büchi Inclusion

We address the problem of deciding language inclusion between two non-deterministic Büchi automata. It is known to be PSPACE- complete and finding techniques that are efficient in practice is still a challenging problem. We introduce two new sequences of simulation relations, called multi-letter simulations, in which Verifier has to reproduce Refuter's moves taking advantage of a forecast. We compare these with the multi-pebble games introduced by Etessami. We show that multi-letter simulations, despite being more restrictive than multi-pebble ones, have a greater potential for an incremental inclusion test, for their size grows generally slower. We evaluate this idea experimentally and show that incremental inclusion testing may outperform the most advanced Ramsey-based algorithms by two orders of magnitude.This is a joint work with Martin Lange and Etienne Loze.

Wednesday, 06.03.2013, 11:00 a.m., Room WA1318: Manuel Vargas Guzmán (Uni Kassel)

Model-Checking Process Equivalences.

Process equivalences are formal methods that relate programs and system which, informally, behave in the same way. Since there is no unique notion of what it means for two dynamic systems to display the same behaviour there are a multitude of formal process equivalences, ranging from bisimulation to trace equivalence, categorized in the linear-time branching-time spectrum. We present a logical framework based on an expressive modal fixpoint logic which is capable of defining many process equivalence relations: for each such equivalence there is a fixed formula which is satisfied by a pair of processes if and only if they are equivalent with respect to this relation. We explain how to do model checking, even symbolically, for a significant fragment of this logic that captures many process equivalences. This allows model checking technology to be used for process equivalence checking. We show how partial evaluation can be used to obtain decision procedures for process equivalences from the generic model checking scheme. This is the work of two papers, a conference and an extended version, written together with Martin Lange, Etienne Lozes and myself.

Wednesday, 23.01.2013, 11:00 a.m., Room WA1318: Bahareh Badban (Uni Kassel)

Three-valued Abstraction-Refinement for Real-Time Systems.

The modeling of many real-life systems require dense time domains to reflect the fact that events may happen arbitrarily close to each other in actual applications. Timed automata have emerged for modeling such systems. It is our goal to improve scalability of real-time model checking through the development of a CEGAR-based framework based on three-valued logic. In general CEGAR indicates iterative refinement of over-approximated models based on the analysis of counterexamples until no more counterexamples can be found. Our aim is to develop a completely automatic predicate abstraction method for the verification of concurrent dense real-time systems. The idea of abstraction is to reduce dense timed automata into finite tractable size automata. With the intention of increasing the scalability of existing techniques, we have started to develop an algorithm which strengthens the automaton through discovering new hidden state invariants. A particular challenge lies in integrating various forms of inter-process communications into out algorithms. In a joint work with Martin Lange, we have extended the initial results further into a research proposal.

Wednesday, 14.11.2012, 11:00 a.m., Room WA1318: Martin Lange (Uni Kassel)

Branching Time? Pruning Time!

The full branching time logic CTL* is a well-known specification logic for reactive systems. Its satisfiability and model checking problems are well understood. However, it is still lacking a satisfactory sound and complete axiomatization. The only proof system known for CTL* is Reynolds' which comes with an intricate and long completeness proof and, most of all, uses rules that do not possess the subformula property.
We consider a large fragment of CTL* which is characterized by disallowing certain nestings of temporal operators inside universal path quantifiers. This subsumes CTL+ for instance. We present infinite satisfiability games for this fragment. Winning strategies for one of the players represent infinite tree models for satisfiable formulas. These can be pruned into finite trees using fixpoint strengthening and some simple combinatorial machinery such that the results represent proofs in a Hilbert-style axiom system for this fragment. Completeness of this axiomatization is a simple consequence of soundness of the satisfiability games. (Joint work with Markus Latte.)

Wednesday, 11.7.2012, 11:00 a.m., Room WA1318: Bahareh Badban (Uni Kassel)

A Reduction System for Creating Semi-linear Parikh Images of Regular Expressions.

In this talk I will present a reduction system for regular expressions. The reduction system works like this: for any regular expression regex, it creates a semi-linear representation of the Parikh image of the language of regex. We prove that the reduction system always terminates in a state where the resulting most-reduced expression readily yields this semi-linear representation.

Wednesday, 20.6.2012, 11:00 am, Room WA1318: Etienne Lozes (Uni Kassel)

Separation Logic .

Part Two : Expressivity and Complexity. In this talk, we'll introduce several decision problems with regard to separation logic, and show how a solution to them is helpful for verifying heap-manipulating programs with more or less amount of automation. While discussing these problems, it will be interesting to consider expressiveness issues, and to look at the extension of Separation Logic to arbitrary graph, called Spatial Logic for Graphs. We'll try to give a complete overview of the results, in particular connections with (monadic) second-order logic, and explain which decision procedures are used in existing tools.

Wednesday, 13.6.2012, 11:00 a.m., Room WA1318: Etienne Lozes (Uni Kassel)

Separation Logic .

Hoare-Floyd logic is a well-known proof system for programs based on so-called Hoare triples of the form {A} p {B}, meaning "if program p can assume A as it starts, it ensures B as it stops". Separation Logic is an extension of Hoare-Floyd logic for reasoning about programs. The main ingredient of separation logic is a second-order connective called separating conjunction: A*B asserts that the state is composed of two disjoint parts, one satisfying A, the other satisfying B. This connective yields a new reading of a Hoare triple {A} p {B}: "if p can consume A as it starts, then it has enough resources to run safely, and it produces B as it stops". Less than ten years after its theoretical foundation, Separation Logic starts to prove, through impressive automatic tools, to be a successful approach for checking large low-level C code (Apache, Linux,...), and to nicely handle lots of small but intricate concurrent algorithms (e.g. lock-free concurrent data structures). The logical foundations, expressiveness issues, and decision procedures, have been much clarified since 2000. However, for all of these aspects and others, Separation Logic is still a very active field of research.
Part One : Foundations. In this talk, we'll introduce the general problem of the verification of heap-manipulating programs, we will define a simple programming language and the core of separation logic's proof system. We'll illustrate it on several examples of standard but subtle algorithms for recursive data structures, with often a great gain of conciseness and readability with respect to other formalisms. We'll discuss semantics issues, as well as ways of formally proving that a well-proved program has some nice properties.

Wednesday, May 30, 2012, 11:30 a.m., Room WA1318: Waled Almakhawi (Uni Freiburg / Hodeidah Uni, Yemen)

Landmarks into Directed Model Checking.

Model checking considers the task to check if a given system description satizes a given property. In case of erroneous systems, a counterexample is returned. Numerous studies have been done to nd ecient techniques that can nd error states in the system model state space in an ecient manner. Large system models have a huge number of states in their state space such that it is very costly to enumerate the entire state space. Therefore, it is highly required to find guidance informations that can tackle the problem of large state spaces. Directed model checking uses methods that can direct the search process towards error states. It uses the notion of heuristic functions to nd the way in which the states should be ordered during the state space traversal to nd an error state fast. In this thesis, we introduce the notion of landmarks to directed model checking. Landmarks have been originally introduced in AI planning. They provide additional information's that can be integrated beside the heuristic function. Landmarks are specific formula that must be achieved on the way to every error state. We will show how landmarks can be extracted and ordered, and how we can use these orderings to foster up the search and to recommend to the model checker what is better to take in the next step to go towards the error state. We have implemented our approach into the mcta model checker. Our experiments show that sometimes performance improvements can be obtained.

Wednesday, 2.5.2012, 11:00 am, Room WA1318: Martin Lange (Uni Kassel)

Parity Games: Theory, Practice, Applications

Parity games are 2-player games played on a (usually finite) directed graph in which each node has a priority. The winner of an infinite play is determined by the parity of the maximal priority occurring infinitely often in the play. This seemingly arbitrary concept captures all sorts of other winning conditions, namely all that can be expressed as an omega-regular set of plays. It also comes with nice algorithmic properties as well as a rich theory, even though the exact computational complexity of the solving problem for parity games remains unknown to date. In this talk I will start by giving an overview of the state-of-the- art in the theory of parity games and explain why the problem of solving such games lies at the heart of many problems in the area of formal methods, most notably satisfiability checking and program synthesis problems. I will also present PGSolver - a tool that aims at solving parity games efficiently in practice - and show some (surprising?) discrepancies between its behavior in practice and theoretical predictions. I will conclude with on overview of potential further work in the area of parity game solving with a particular focus on applications of a certain extension of parity games, namely stair-parity games.

Wednesday, 8.2.2012, 14:00, Room WA1318: Norbert Hundeshagen (Uni Kassel)

Characterizing the Rational Functions by Restarting Transducers

The rational relations are the well known class of relations that are defined as the rational subsets of the product of two monoids. This talk focusses on a proper subset of these relations, the rational functions. Here we characterize these functions and some of their proper subclasses by certain types of deterministic restarting transducers with window size one. Thereby a restarting transducer is a restarting automaton that is equipped with an output function.

Wednesday, 1.2.2012, 14:00, Room WA1318: Friedrich Otto (Uni Kassel)

On Centralized PC Grammar Systems with Context-Sensitive Components

It is known that in returning mode centralized PC grammar systems with context-sensitive components only generate context-sensitive languages. In the literature it is claimed that this result extends to centralized PC grammar systems with context-sensitive components that work in nonreturning mode. Here, however, we show that the class of languages that are generated by centralized PC grammar systems with context-sensitive components working in nonreturning mode coincides with the complexity class NEXT.

Wednesday, 23.11.2011, 14:00, Room WA1318: Peter Cerno (Charles University Prague)

Clearing Restarting Automata

Restarting automata were introduced as a model for analysis by reduction, which is a linguistically motivated method for checking correctness of a sentence. We propose a new restricted version of restarting automata called clearing restarting automata with a very simple definition but with interesting properties with respect to their possible applications. Although clearing restarting automata recognize even some non-context-free languages, they do not recognize all context-free languages. Therefore we also introduce an extended model, called the delta-clearing restarting automata, which is able to recognize all context-free languages. We also mention some open problems and possible directions of the future research in this area.

Wednesday, 9.11.2011, 14:00, Room WA1318: Martin Lange (Uni Kassel)

Size-Change Termination and Emptiness for Alternating Parity Automata

In the automata-theoretic framework, finite-state automata are used as a machine model to capture the operational content of temporal logics. Decision problems like satisfiability, subsumption, equivalence, etc. then translate into questions on automata like emptiness, inclusion, language equivalence, etc. Linear-time temporal logics like LTL, PSL and the linear-time mu-calculus have relatively simple translations into alternating parity automata, and this automaton model is closed under all Boolean operations with very simple constructions. Thus, the typical decision problems for such linear-time temporal logics reduce relatively simply to the emptiness problem for alternating parity automata. In this paper we present a method for deciding this emptiness problem without going through intermediate automaton models like nondeterministic ones. The method is a direct adaptation of the size-change termination principle which was originally used to decide termination of abstract functional programs.

Wednesday, 19.9.2012, 14:00, Room WA1318: Bahareh Badban (Uni Kassel)

Exact Incremental Analysis of Timed Automata with an SMT-Solver.

Timed automata as acceptors of languages of finite timed words form a very useful framework for the verification of safety properties of real-time system. Many of the classical automata-theoretic decision problems are undecidable for timed automata, for instance the subsumption or the universality problem. In this paper we consider restrictions of these problems: universality for deterministic timed automata and subsumption of a nondeterministic one by a deterministic one. We show that these problems are polynomial-time equivalent to the emptiness problem of nondeterministic timed automata, i.e.\ PSPACE-complete. We then advocate the use of SMT solvers for the exact incremental analysis of timed automata via these problems. We stratify these problems by considering domains of timed words of bounded length only and show that each bounded instance is NP-complete. We present some experimental data obtained from a prototypical implementationq measuring the practical feasibility of the approach to timed automata via SMT solvers.

Wednesday, 13.7.2011, 11:00 a.m., Room WA1318: Norbert Hundeshagen (Uni Kassel)

Characterizing the Regular Languages by Nonforgetting Restarting Automata

The restarting automaton is a machine model that is motivated by the technique of analysis by reduction from linguistics. Basically it can be seen as an extension of finite state automaton. It is well known that some types of restarting automata with window size one compute exactly the regular languages. This talk focuses on the these types of automata additionally equipped with the nonforgetting property. The main result shows that the monotone variants of the nonforgetting restarting automata with window size one characterize the regular languages.

Wednesday, 13.7.2011, 11:30 a.m., Room WA1318: Marcel Vollweiler (Uni Kassel)

Pushdown Automata with Translucent Pushdown Symbols

Pushdown automata with translucent pushdown symbols are presented. Such a device is a pushdown automaton $M$ that is equipped with a {`transparency relation'}~$\tau$. In a transition step, $M$ does not read (and replace) the topmost symbol on its pushdown store, but the topmost one that is only covered by translucent symbols. We prove that these automata accept all recursively enumerable languages. Then we concentrate on pushdown automata with translucent pushdown symbols that work in real-time or in quasi-real-time. We compare the corresponding language classes to other classical complexity classes, and we study closure properties for these language classes.

Wednesday, 22.6.2011 and 29.6.2011, 11:00 a.m., Room WA1318: Martin Lange (Uni Kassel)

Tableaux(-Like) Decision Procedures for Temporal Logics

Temporal logics are modal logics over infinite flows of time. They form important tools for the specification of program behavior. Their satisfiability problems therefore form the algorithmic essence of consistency checks for logical specifications of correct program behavior.
Temporal operators usually have elegant characterizations in terms of fixpoint solutions to certain recursive equations. This often makes the evaluation of temporal formulas in Kripke structures relatively simple using fixpoint iteration techniques. It also introduces very particular difficulties for deciding satisfiability: one has to ensure that iterations corresponding to least fixpoint constructs are well-founded.
In this tutorial we will review basic temporal logics and tableau-based methods for their satisfiability problems. We will illustrate the problems arising with a mixture of least and greatest fixpoint constructs in such tableaux and discuss known solutions as well as related and open questions in this area.
The tutorial will be held at an introductory level. No particular knowledge about temporal logics will be required. However, participant will be expected to have some knowledge and logic in general. Some knowledge on automata theory will be helpful but is not essential.

Wednesday, 15.6.2011, 11:00 a.m., Room WA1318: Bahareh Badban (Uni Kassel)

Towards an Automated Predicate Abstraction of Dense Real-Time Automata

Real-time requirements, in particular on meeting hard real-time bounds, play an important role in the design of concurrent, embedded real-time systems. In many application areas, such as transportation, process control or medical automation, those systems are safety-critical, i.e., their malfunctioning may entail the loss of life. Efficient verification technology is hence a crucial desideratum for the real-time system design process. Due to the inherent complexity that these systems possess, manual verification approaches are impractical.
To scale the existing verification strategies to the analysis of real-life systems engaging time with realistic size, our goal is to create an automatic abstraction-based verification approach for concurrent dense real-time models. In the course of verification of a system it is realized that many important properties of real-time designs are in fact safety properties. Safety properties can be chacked using reachability analysis of the real-time model. Therefore, in our investigations we will focus on solving this class Our aim is to develop a completely automatic predicate abstraction method for the verification of concurrent dense real-time systems. The idea of abstraction is to reduce the dense timed automata into finite tractable size automata. With the intention of increasing the scalability of existing techniques, we have started to develop an algorithm which first investigates for idle transitions imposed from hidden state invariants. A particular challenge lies in catering for various forms of inter-process communications. Based on the initial results a project proposal is now being developed.

Wednesday, June 1, 2011, 11:00 a.m., Room WA1318: Friedrich Otto (University of Kassel)

Cooperating distributed systems of stateless deterministic restarting automata with window size one

The restarting automaton is a machine model that is motivated by the technique of analysis by reduction from linguistics. It consists of a finite-state control and a flexible type with end markers and a read/write window of a fixed size. This talk focuses on the weakest model of the restarting automaton: the so-called R-automaton with a read/write window of size one (R(1)-automaton for short). It is well-known that R(1)-automata accept exactly the regular languages, while stateless deterministic R(1)-automata just accept regular languages of a very restricted form. Accordingly, we combine a finite number of such automata into a cooperating distributed system (CD-system) of stateless deterministic R(1) automata. These CD-systems only accept languages with semi-linear Parikh images, but they turn out to be quite powerful, as they accept all rational trace languages. In fact, the rational trace languages (and even the context-free trace languages) can be characterized in terms of certain CD-systems of stateless deterministic R(1)-automata. If the components of these CD-system are not required to be stateless, then these systems are strictly more expressive, as then they even accept some languages that are not semi-linear.

Tuesday (!), 22.2.2011, 10:15 a.m., Room WA1318: Markus Latte (LMU Munich)

Separation Results for XCTL

XCTL[A] is an extension of CTL which refines the temporal until and release operators with formal languages in A. In this way, XCTL can express non-regular properties, in contrast to CTL. For regular, visibly pushdown and deterministic context-free languages, the separation of the respective XCTL can be proven by automata-theoretic techniques. However, these techniques introduce non-determinism on the automata side. As non-determinism is also the difference between DCFL and CFL, these techniques seem to be inappropriate to separate XCTL[DCFL] from XCTL[CFL]. Nevertheless, we show the separation of DCFL from CFL for the EF/AG-fragment of XCTL.

Friday (!) 21.1.2011, 10:15 am, Room WA1318: Etienne Lozes (RWTH Aachen)

From Spatial Logics to Separation Logic

Spatial Logics were introduced by Cardelli and Gordon in the early 2000s, and were first devoted to the specification of mobile processes . They were then extended to static structures, including XML documents and graphs. Almost at the same time, Separation Logic was popularized by Reynolds' 2002 Lics invited paper, and up to today increases its influence in many researches, both from theory and very practical aspects. In this talk, I will try to survey the theoretical aspects of my work (I will skip the more practical ones I have been involved in these last years), with a shift of interest from Spatial Logic towards Separation Logic. I will present the expressivity, decidability, and complexity results for several spatial and separation logics, extended or not by temporal constructs.

15.12.2010, 15:15, Room WA1318: Norbert Hundeshagen (Uni Kassel)

Transducing by Observing

Most of the computational models developed in recent years have been motivated by biochemical processes. Many of these machinisms follow the well-known black-box concept: an input is directly transformed into an output, which is the result of the computation and provides information about the computational power. The observer systems at the center of this lecture use a different approach: of interest is not only the product of such a system, but the change of the system itself. The computational power of different language generating or accepting systems has already been investigated in this context. This concept is extended here to include observer systems that compute transductions.

1.12.2010, 15:15, Room WA1318: Martin Lange (Uni Kassel)

Bounded model checking and analysis of context-free grammars

Many problems about context-free grammars are undecidable, e.g. ambiguity, universality, subsumption, equivalence, etc.. However, if these are restricted to words of maximal length, they are typically in NP or coNP. Example: The restricted universality problem takes as input a context-free grammar and a number k in unary coding and decides whether there is a word of length at most k that is not generated by the grammar. If you successively increase the parameter k, you naturally obtain a semi-decision procedure for the original problem.
A similar technique - but "only" a reduction of PSPACE to NP - is used in bounded model checking. In addition, we make use of the fact that problems in NP can often be solved well by SAT solvers.
In this talk, we first introduce bounded model checking and then show how this technique can be applied to the above problems to obtain even usable semi-decision methods in practice.

10.11.2010, 15:00, Room WA2104: Jan Hoffmann (LMU Munich)

Analyzing Sorting Algorithms with Resource Aware ML

Recently we developed an automatic amortized analysis to compute polynomial resource bounds for first-order functional programs at compile time. Its basis is a type system that augments types with resource annotations.
The analysis system has been implemented in the programming language Resource Aware ML. Our experiments showed that it efficiently computes precise time and heap bounds for many typical programs.
In this talk I will demonstrate the implementation by computing worst-case bounds for the sorting algorithms quick sort and insertion sort. To illustrate pros and cons, I compare our automatic analysis to a manual analysis of the algorithms in a popular textbook.
For more information see the web page of the project: raml.tcs.ifi.lmu.de