Advanced seminar "Theoretical Computer Science"
The content on this page was translated automatically.
In the advanced seminar “Theoretical Computer Science,” employees, interested students, and guests present on current research in the field of theoretical computer science.
Wednesday, August 26, 2026 Nicolai Fiege
Optimizing Constant Matrix Multiplication Circuits is NP-complete
--
Friday, July 17, 2026 Lars-Eric Marquardt
On the Relative Expressiveness of HyperLTL and the Polyadic μ-Calculus
Hyperproperties generalize trace properties by making assertions not only about individual executions of a system but also relating multiple executions of a system. They are relations between traces rather than sets. Hyperproperties have garnered sustained interest in security engineering, where ordinary trace properties are too weak to specify (un)desired system behavior, such as noninterference.
The most prominent logic for hyperproperties is HyLTL, which extends LTL with explicit trace quantification and trace variables. Rabe et al. studied its computational complexity and model-theoretic properties and also briefly compared it to established non-standard temporal logics such as the polyadic μ-calculus. This lesser-known logic extends the modal μ-calculus with indexed propositions and modalities and is interpreted as tuples of states of a system. This step is reminiscent of the transition from temporal logics to hyperlogics and allows for the expression of non-interference. Given this, it is reasonable to ask whether the polyadic μ-calculus already possesses sufficient expressive power to express interesting hyperproperties.
This thesis reports on further investigations into the expressive power of logics for hyperproperties, specifically the relationship between HyLTL and the polyadic μ-calculus. We show that properties expressed in the alternation-free fragment of HyLTL can also be expressed in the polyadic μ-calculus. We establish the existence of a family of properties definable in the polyadic μ-calculus that are not definable in HyLTL. Furthermore, by reexamining the proof of PSPACE and EXPSPACE hardness, respectively, for fragments of HyLTL with small quantifier alternation depth, we provide simple patterns of HyLTL formulas that cannot be expressed in the polyadic μ-calculus.
Friday, July 10, 2026 Norbert Hundeshagen
Correcting Deterministic Finite Automata for Didactic Feedback
Motivated by educational applications, we study the problem of computing all corrections that transform a finite automaton into one that recognizes a given regular language L. We show that for deterministic finite automata, the set of all corrections can be finitely characterized as a regular tree language. The construction is based on a tree encoding of all deterministic finite automata that recognize L, which is extended to correction trees that make individual corrections and their induced edit operations explicit. Based on closure properties of regular tree languages, we introduce so-called filters for selecting corrections that satisfy didactic constraints, enabling the derivation of individualized feedback from student submissions.
Friday, July 3, 2026 Florian Bruse
Bisimulation-Invariant Nondeterministic Time-
Bisimulation-invariant complexity deals with problems for which bisimilar inputs are always either both yes-instances or both no-instances. For example, NFA non-universality is bisimulation-invariant, whereas the class of even-sized structures is clearly not. Otto (99) characterizes the bisimulation-invariant fragment of PTIME as exactly those problems that can be formalized in the polyadic μ-calculus. This adds a new perspective to descriptive complexity theory, as this characterization circumvents the “order problem,” which has so far made it difficult to characterize classical PTIME in terms of a logic.
Since Otto’s result, characterizations of both the exponential-time hierarchy and the exponential-space hierarchy in terms of (higher-order) modal fixpoint logics have been found. With the exception of a special result for NLOGSPACE, all these characterizations concern deterministic classes, which leaves open the question of, for example, bisimulation-invariant NP. There are obvious characterizations of this class, for example as a syntactic fragment of the characterization of bisimulation-invariant PSPACE, or by adding nondeterminism externally to the polyadic modal mu-calculus. None of these characterizations fit naturally and robustly into the framework of characterizations of bisimulation-invariant complexity classes via (higher-order) modal fixpoint logics.
In this talk, I provide an overview of the above efforts and report on efforts to find a natural characterization of bisimulation-invariant NP within this framework.
Friday, June 26, 2026 Sören Möller
Verification of Hypotheses in Natural Science Experiments
We present a proof calculus for the formal verification of hypotheses about relationships in natural science experiments. The soundness of the calculus is proved; completeness is discussed. Finally, possible extensions are outlined, including the integration of SMT solvers as well as richer means of expression for statements about such experiments.
Friday, June 19, 2026 Igor Semezies
Temporal-Spatial Logics over Quasi-Temporal Graphs
--
Friday, May 8, 2026 Lowejatan Noori
Words and Temporal Graphs: Comparing the Expressive Power of State Space Models and Recurrent Neural Networks
This talk compares the expressive power of graph state space models and recursive temporal graph neural networks on temporal graphs. The comparison is conducted using two-dimensional product logics that combine temporal reasoning over time with modal reasoning over graph neighborhoods. The project shows that diagonal-gated graph state space models can capture a counting-enhanced product logic, while recursive temporal graph neural networks can express a richer logic with temporal recursion. These results reveal a structural separation between the two architectures and mirror known expressiveness gaps between state space models and recurrent neural networks over words.
Friday, April 24, 2026 Daniel Engelmann
From Text to Automata: Fine-Tuning Local Large Language Models for NFA Construction
My talk addresses the question of whether a local LLM can be fine-tuned to construct NFAs from natural-language descriptions. First, I’ll explain why choosing a suitable base model was problematic and why I ultimately decided on Qwen as the baseline. Next, I’ll discuss my data pipeline, focusing in particular on the difference between the first and second generators and why the latter is more closely aligned with student assignments. I then present the fine-tuning process using LoRA/QLoRA as well as the evaluation setup. Finally, I discuss the results on a 100-task benchmark (automatically generated) and the smaller exam/student split (manually created), as well as the open problems and limitations of the approach.
Thursday, March 5, 2026 Tobias Stuhldreier
User-Driven Error Correction for Context-Free Languages
For a context-free grammar (target language) and a word that typically does not belong to the language of the grammar, the set of all valid corrections can be computed using a generalized error-correction parser. These corrections consist of sequences of deletion, replacement, and insertion operations that transform the word into a word of the target language.
As part of this bachelor’s thesis, we investigated how exactly one correction can be selected from the set of all possible corrections using a user-driven question-and-answer process. To this end, an algorithm was developed that, based on user input, systematically traverses the underlying data structure storing all corrections to determine a unique correction. Building on this approach, the error-correction parser was extended so that it is no longer necessary to first compute all corrections in full; instead, a specific correction is selected step by step via user input already during the parsing process.
Thursday, January 22, 2026 Martin Lange
Relative Regularity of Tree Languages
I will introduce the concept of relative regularity of tree languages (unranked, unsorted, infinite) and present some specific languages L_d and P_d for d=1,2,..., such that a proof of the non-regularity of L_d relative to P_d would imply bounds on the expressive power of the polyadic mu-calculus. This is ongoing joint work with Florian Bruse.
Thursday, December 11, 2025 Cedric Kollenberg
How can “good” instances be generated?
In many areas of computer science, example instances must be generated. Often, there is the constraint that these must be generated randomly and must satisfy certain properties in order to be considered “good” instances. If the application domain of the instances is fixed, specialized applications can be used for this purpose. The difficulty arises when the domains from which the instances are to be generated need to remain flexible. This requires a universal approach.
One option is to use SAT solvers. The idea involves transforming a problem-specific data structure into a propositional logic formula. This formula not only encodes the structure of the data but also captures the conditions that the instances must satisfy. If models exist for the generated formula, they are transformed back into objects and can be output.
This results in a universal application for generating “good” instances.
Thursday, December 4, 2025 Florian Bruse
The Modal Mu-Calculus on Uniformly Recurrent Words
In [B./Sälzer/Lange], we showed that the modal mu-calculus enjoys finite convergence of fixpoints on a purposefully constructed infinite word w, which has an infinite bisimulation quotient. Finite convergence means that all fixpoint definitions in a given formula are equivalent to some finite unfolding. Hence, w behaves much like a finite structure with respect to the mu-calculus, even though it is infinite and not eventually periodic.
In this talk, we show that all uniformly recurrent words possess this property of finite convergence. Uniform recurrence means that for all subwords, there is a bound such that the subword either never occurs again or occurs again at most after this bound. In fact, uniform recurrence characterizes the finite convergence of mu-calculus fixpoints: if a word has finite convergence of fixpoints, it must be uniformly recurrent.
This convergence result for uniformly recurrent words also implies MSO decidability over uniformly recurrent words, since MSO can be translated into the mu-calculus over infinite words. This is not new, as Semenov (1984) showed that the MSO theory of the natural numbers with < and a uniformly recurrent unary predicate P is decidable. Our result, however, has a much more accessible proof.
This is joint work with Fabian Lehr.
Thursday, November 27, 2025 Ashkan Kiafard
A Neurosymbolic Model Checker for First-Order Logic over Graphs
Thursday, August 21, 2025 Daniel Engelmann
LLM-based evaluation of automata construction tasks - On the automated detection of learning difficulties
Struggle detection involves identifying the optimal moment to support students as they attempt to solve a specific problem, thereby promoting their learning progress.
For simple programming tasks, the most effective approaches currently available are based on determining a distance between a student’s current attempt at a solution and a model solution, calculated using LLM embedding. By tracking the evolution of this distance (or changes in lines of code) and comparing it with existing data on how other students’ distances evolved for the same task, it is possible to determine whether a student is having difficulty with the task.
This thesis investigates the extent to which this approach can be applied to exercises involving the construction of finite automata. To this end, various configurations of LLM embedding are compared with conventional distance measures on regular languages, as well as with expert evaluations. The advantages and disadvantages of using embedding for struggle detection are also identified.
Thursday, July 31, 2025 Lars-Eric Marquardt
HyperCTL*: a logic for hyperproperties
This talk provides an overview of HyperCTL*, a branching-time logic for hyperproperties. Hyperproperties generalize trace properties by relating multiple executions of a system, enabling the expression of security-related properties such as noninterference. We introduce HyperCTL* as an extension of CTL* with explicit path variables and quantification over multiple paths. Next, we present an automata-theoretic model-checking algorithm that translates HyperCTL* formulas into alternating Büchi automata. Finally, we show that the satisfiability problem for HyperCTL* is Σ₁²-complete, placing it well beyond the analytical hierarchy in terms of undecidability.
Friday, July 4, 2025 Martin Lange
Metric Linear-Time Temporal Logic with Strict First-Time Semantics
We introduce strict first-time semantics for the Until operator from linear-time temporal logic, which makes assertions not just about some future moment but about the first time in the future that its argument should hold. We investigate Metric Linear-Time Temporal Logic under this interpretation in terms of expressive power, relative succinctness, and computational complexity. While its expressiveness does not exceed that of pure LTL, there are properties definable in this logic that can only be expressed in LTL using exponentially larger formulas. Yet, we show that the complexity of the satisfiability problem remains PSPACE-complete, which contrasts with the EXPSPACE-completeness of Metric LTL. The motivation for this logic stems from a study of the expressive power of State Space Models, a recently proposed alternative to the popular transformer architectures in machine learning.
Friday, June 13, 2025 Jana Melani Klitzsch
Model Checking Metric First-Order Temporal Logic over Dynamic Graphs
Dynamic graphs are used in many fields, such as social network analysis and epidemiology. With the growing relevance of machine learning, there are also more learning methods designed for dynamic graphs. Since safety and ethical use are important when applying such models, formal verification is one way to achieve these goals, at least in part. To do this, however, we need a way to formally describe and verify properties of dynamic graphs.
In my bachelor’s thesis, I focused specifically on model checking for dynamic graphs. For this, I used Metric First-Order Temporal Logic (MFOTL) to describe the properties we are verifying. For model checking, I define two different model-checking problems. One that verifies whether a given dynamic graph satisfies a property, and one that verifies whether the graph could satisfy the property if we add further time steps to the graph. In addition, I also define a bounded SAT problem for these properties.
The main part of the work consists of reducing all these decision problems to the Boolean SAT problem and proving the correctness of this reduction.
I also wrote a proof-of-concept implementation to test how quickly these problems can be decided using the reduction.
Finally, I also provide an outlook on the directions in which further research based on this work could proceed.
Thursday, May 8, 2025 Ahmad Lowejatan Noori
Analysing the Expressive Power of State-Space Models via RASP Programs
State-Space Models (SSMs) offer an efficient alternative to transformers. They follow a linear recurrence, allowing information from sequential input data to be selectively passed on or overwritten. From a formal perspective, these models can be regarded as language acceptors, whereby their expressive power is described by the set of accepted formal languages. In this work, we use our RASP variants Lin-C-RASP and Lin-RASP to characterize the expressive power. Lin-C-RASP programs are equivalent to an extension of Pure-Past LTLf by linear inequalities over counter terms that count the satisfying positions of a word prefix by prefix. Lin-RASP is equivalent to Pure-Past LTLf. To link these results to SSMs, we translate Lin-C-RASP programs into SSMs, where each statement in the program corresponds to a layer in the SSM. In this way, we obtain lower bounds for SSMs with respect to the aforementioned temporal logics and the language classes they recognize. Since the translation is polynomial, the PSPACE-hardness of the satisfiability or non-emptiness problem for SSMs follows from the satisfiability problem of PLTLf formulas. Finally, we consider a less restricted variant of SSMs and show that Lin-C-RASP programs with modular predicates can also be embedded.
Thursday, April 24, 2025 Sören Möller
Categorizing Functions in Natural Science Experiments
In my work, I investigate experiments modeled by sets of functions that describe dependencies between variables (e.g., the influence of 'air pressure' on 'boiling point of water' or the relationship between ‘time’ and ‘bacterial growth rate’).
The central question is whether a specific hypothesis can be derived from a general description of such an experiment, which encompasses a potentially infinite number of possible experiments.
The goal of this work is to enable the automated validation of hypotheses about these experiments with as few restrictions as possible.
To this end, I am developing a categorization of these experiments based on local information and analyzing the conditions necessary for the correctness of this approach. A key part of this work involves investigating how this local information is propagated through function compositions.
This makes it possible to consider all possible classes of experiments that match a given description.
This turns the validation of hypotheses into a finite search problem.
Friday, April 11, 2025 Robin Weber
An investigation of natural-language reduction descriptions for their implementability by an LLM
Friday, February 27, 2025 Nathanael Schmidt
An extension of the DiMo tool to support other data types - Using words as an example
The DiMo tool allows users to describe parameterized propositional logic formulas and then check them for satisfiability, universality, or semantic equivalence for parameter values from a given domain. However, DiMo has so far only supported integers as a data type for parameters. From the perspective of the problems to be modeled, however, it makes sense to be able to use other data types as well, such as words or graphs. Therefore, in this work, words were added to DiMo as a data type, along with associated operations such as concatenation and access to individual characters of a word. Furthermore, it is now possible to use regular expressions to describe sets of words that can be used as domains of definition for parameters or as iteration sets in generalized conjunctions.
Thursday, January 23, 2025 Ahmad Lowejatan Noori
Translating Star-Free Counter Automata into State Space Models
Large language models (LLMs), such as GPT, are advanced AI systems designed to understand and generate human-like text. They are powered by Transformers, a neural network architecture renowned for its ability to model long-range dependencies in sequences through so-called self-attention mechanisms. State-space models, such as Mamba, present a compelling alternative to Transformers and provide efficient representations for sequential data. They use continuous state representations and linear recurrence, which are highly efficient and scalable. In general, an input word, embedded as real-valued vectors, is fed into the state-space model. For each embedded input token, the model computes a hidden state via linear recurrence, where encoded information can be overwritten or propagated. These states are normalized and serve as input for a neural network that can either perform classification tasks or predict the next token. A common approach to understanding the capabilities of such models is through the lens of automata and language classes. This thesis elaborates on the results from the work of Sarrof, Veitsman, and Hahn regarding the recognition of star-free languages by SSMs. These results are extended by adding a counter property. We introduce star-free counter automata, which are equivalent to deterministic finite-state automata with the addition of a counter and a specific restriction on states. This restriction limits acceptance to star-free regular languages within the class of regular languages. However, by including the counter, these automata can still accept languages outside the class of regular languages. The thesis presents a specific method for translating a given star-free counter automaton into a state-space model such that the automaton’s language acceptance and the model’s recognition are equivalent.
Monday, January 13, 2025 Sören Möller
Categorizing Functions in Natural Science Experiments
In my thesis, I examine experiments modeled by sets of functions that describe relationships between variables (e.g., the influence of a on b and the influence of d on c).
The central question is: Can one infer a specific hypothesis from a general description of an experiment that encompasses an infinite number of possible experiments?
To answer this question, I categorize the infinite number of possible experiments into equivalence classes to reduce the search space to a finite range. A key aspect here is the composition of functions: From the functions for the variables (a,b), (b,c), and (a,d), (d,c), a function for (a,c) can be derived that must match in both directions. The search procedure must therefore be able to take such relationships into account, rather than simply generating functions for each pair of variables independently, which would each only match the descriptions locally.
Thursday, December 19, 2024 Lukas Mentel
PDR and SMT2 for Formal Verification of Embedded Systems
Bounded model checking in conjunction with k-induction is frequently used for symbolic model checking. IC3 (“Incremental Construction of Inductive Clauses for Indubitable Correctness”) [1] offers an alternative to this approach and is certainly one of the most important innovations of the past 15 years in this field [2].
In this approach, a set of formulas is modified step by step with the goal of obtaining a (1-inductive) invariant.
In this talk, I will present the results of my master’s thesis. Following a brief introduction to IC3 and its extension PDR (“Property Directed Reachability”) [2], I will present the results of a prototypical implementation of IC3/PDR based on the SMTLIB standard.
[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.https://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.
Tuesday, October 8, 2024 Maurice Herwig
Using Shared Packed Parse Forests to Compute All Minimal Corrections
This work deals with the efficient computation of all minimal corrections with respect to a minimality definition. The computation can be divided into two independent phases. In the first phase, all corrections for a word and a context-free grammar are computed. A modified version of the Generalized Earley Parser is used for the computation, and the resulting corrections are stored in a Shared Packed Parse Forest. It is shown that the forest for a word of length n can be computed in O(n³) and contains all corrections that correct the word in the language of the grammar. From the set of all corrections, the set of minimal corrections can then be filtered out using filters. An example of a minimality definition is presented.
Tuesday, August 6, 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 detecting fake news on social networks or predicting traffic flow. One problem that arises in such applications is adversarial attacks, in which an attempt is made to alter the network’s input so that its actual output changes. A security property that guarantees robustness against adversarial attacks is the Adversarial Robustness Property (ARP). In this master’s colloquium, we will therefore focus on ARPs for TGNNs. We will formulate various ARPs for TGNNs, with the budget—which describes the changes to the temporal graph—being a key component. Furthermore, we will see how an ARP for a TGNN can be proven using the Randomized Smoothing Framework. Experiments were conducted on benchmark datasets for the proposed ARPs, with the aim of proving an ARP for a TGNN. We will conclude by examining the design and results of these experiments.
Thursday, July 18, 2024, and Thursday, July 11, 2024: Lukas Mentel
IC3 / PDR and SMT-LIB for Formal Verification of Embedded Systems
Bounded model checking in combination with k-induction is frequently used for symbolic model checking. IC3 (“Incremental Construction of Inductive Clauses for Indubitable Correctness”) [1] offers an alternative to this approach and is certainly one of the most important innovations of the past 15 years in this field [2].
In this approach, a set of formulas is modified step by step with the goal of obtaining a (1-inductive) invariant.
In this talk, I will provide an overview of IC3 and its extension, Property Directed Reachability (PDR). Furthermore, I will present the progress made in implementing IC3 and PDR based on the SMT-LIB standard for my master’s 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, June 27, 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”—was already introduced to prove statements about the local behavior of partial, continuous functions. The calculus is based on experiments that describe the behavior “Variable A influences Variable B.” This raised the question of how this behavior changes when multiple variables jointly influence another variable.
In my project, I extended the definitions to include the use of two variables. The goal was to generalize the completeness results to this new calculus, which operates with multiple variables. In this talk, I will present the new model, the results obtained, and the difficulties encountered along the way.
Thursday, May 16, 2024: Georg Siebert
Randomized Smoothing for Time-Aware Robustness of Temporal Graph Neural Networks
In the first part of the talk, we provide a brief introduction to the Randomized Smoothing Framework (RSF), which allows for the computation of probabilistic, budget-based certificates for robustness properties of arbitrary classification models. In addition, as a transition to Part 2, we will introduce the model of Temporal Graph Neural Networks.
In the second part, we will discuss Georg Siebert’s current work on applying the RSF to commonly used TGNN models and benchmarks in practice. Here, we will focus on initial practical results and empirical conclusions.
Friday, April 26, 2024: Laurin Pöppe
Implementation of a Translation of Neural Networks into I/O-Equivalent Finite Automata
Neural networks are widely used to solve complex problems. However, verifying properties and analyzing the behavior of neural networks remains a challenge. One approach is analysis 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, February 15, 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 such as the modal mu-calculus Lmu. Finite convergence—that is, the phenomenon of reaching a fixpoint after only finitely many iterations—is of particular interest for the 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 begin by reviewing the converse and presenting 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 using only functions of order 0.
HFL is interesting in this context because it is very easy to construct an HFL1 formula—i.e., one 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 that this hierarchy collapses 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é Côte d’Azur.
Thursday, February 1, 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 designing such a proof system stems from the need to provide the underlying computational framework for tools that support learning among students in secondary-education classrooms. The ultimate goal is a tool that allows students to formalize hypotheses about phenomena in the natural sciences, such that their validity with respect to a formal experimental model can be verified automatically. The Calculus of Temporal Influence provides a language for formal statements and the mechanisms for reasoning about valid logical consequences. It extends (and in some respects deviates 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 polynomial-time decidability is achieved for a natural stratification of the problem.
Thursday, January 18, 2024: Martin Lange
Formal Reasoning about Influence in Natural Science 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 specific partial orders and statements. The motivation for this work stems from an effort to promote digitalization in secondary-education classrooms, particularly in experimental lessons in natural science classes. This provides a way to formally model experiments and to automatically determine the truth of hypotheses made about certain phenomena in such experiments.
Thursday, January 11, 2024: Adrian Wurm
Investigation of Reachability Problems in Neural Networks Using CSP Methods
We analyze verification problems for neural networks, such as: Given a description of valid inputs and outputs as instances of linear programs, is there a valid input whose output is also valid? And does this hold for all valid inputs?
To this end, 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 on decision problems related to CSPs are helpful in answering the above network questions for a range of different activation functions.
Thursday, November 9, 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 need for reliable safety certificates. The ultimate goal regarding such certificates would be a reasonably efficient, sound, and complete verification of relevant safety properties. However, the highly parameterized black-box nature of neural networks makes it difficult to provide clear answers as to under what circumstances this goal is achievable.
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 such as Graph Neural Networks (GNN) or Transformers, the situation is not quite as clear. We present relevant verification problems for 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 initial results and conjectures regarding corresponding complexity bounds. Finally, we conclude with a summary of the many open questions that must be answered to understand the role of sound and complete verification in safe deep learning.
Tuesday, October 31, 2023: Jan Heinemeyer
Hypothesis Testing in Biology: Extension and Integration of the Calculus of Influence into a Teaching/Learning System for Hypothesis Testing
This talk focuses on the extension of the teaching/learning system for hypothesis testing (iLL) to include the Calculus of Influence (CoI). As part of this presentation, a function for translating hypotheses into statements of the Calculus of Influence will be presented. Furthermore, the limitations of this translation will be discussed, and insights into possible extensions of the hypotheses will be provided. Finally, the structured process for setting up an experiment will be presented.
Thursday, October 12, 2023: Jana Klitzsch
Certifiable Adversarial Robustness for GNNs
Verification is required to ensure that machine learning methods are secure. Graph neural networks (GNNs) encompass various models for either node or graph classification. The goal of adversarial robustness verification is to certify, given the network and a graph, whether “similar” graphs are classified the same way. There are various definitions of similarity for graphs. There are also different types of certificates, each with its own advantages and disadvantages. A specific white-box certificate that uses linear programming will be presented in more detail.
Thursday, September 28, 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 number of parameters 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, September 5, 2023: Laurin Pöppe
Formalization of a Correctness Proof in the Context of NN Verification in Isabelle/HOL
In this project, a formalization for neural networks was developed in the theorem prover Isabelle/HOL.
This formalization was used to verify the correctness of a reduction from 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, the challenges, and the solutions encountered during the project’s implementation, and will conclude with a discussion of a recently published, alternative implementation of neural networks in Isabelle/HOL.
Thursday, August 17, 2023: Lukas Mentel
IC3 / PDR meets SMT-LIB
Bounded model checking in combination with k-induction is frequently used for symbolic model checking. IC3 (“Incremental Construction of Inductive Clauses for Indubitable Correctness”) [1] offers an alternative to this approach and is certainly one of the most important innovations of the past 15 years in this field [2].
As the name suggests, this method involves gradually modifying a set of formulas with the goal of obtaining a (1-inductive) invariant.
This talk provides an overview of IC3 and its variant, PDR. 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 of Graph Neural Networks (GNNs)
Verification of neural networks (NNs) ensures that they meet specific specifications. Graph neural networks (GNNs) are a subset of NNs that take graphs as input. Although there are individual verification algorithms for GNNs, they do not use a uniform format to operate on the GNNs. A standardized format for NNs is the Open Neural Network Exchange (ONNX) format. This format allows NNs to be represented independently of common machine learning (ML) frameworks (e.g., PyTorch or TensorFlow). However, ML frameworks do not fully support the export of GNNs to ONNX. Furthermore, structural information is lost during the export of GNNs.
The goal of this master’s project is to develop a tool that creates an ML-framework-independent representation, which will serve as the basis for GNN verification procedures. To this end, the Python tool “GeNNifier” was developed. It offers a high-level representation of GNNs based on JSON, which can be used to create GNN configurations. Such a configuration can be read by “GeNNifier” and processed further via an interface into a verification algorithm.
To test the applicability of “GeNNifier” for verification methods, the Naive Output Reachability Verification (NORV) algorithm was implemented in “GeNNifier.” This method operates on Message Passing Neural Networks (MPNNs), which are a type of GNN.
The NORV algorithm converts an MPNN into multiple feedforward neural networks (FNNs). A verification procedure for the output reachability problem is then applied sequentially to the generated FNNs 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 range of verifiers.
Thursday, May 25, 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’s thesis focuses on theoretical limits in the verification of such models. The talk provides an introduction to the architecture of Transformer models and the concept of self-attention.
Subsequently, various verification problems for Transformers and their decidability will be discussed.
No prior knowledge is required for the talk.
Wednesday, May 3, 2023: John Hundhausen
A Website Builder for Interactive Lecture Notes and Worksheets
Modern web technologies make it possible to provide interactive visualizations, various exercises, and even exercises that are automatically graded as additional learning tools for students. In the Theoretical Computer Science/Formal Methods research group, various projects are developing precisely this type of learning tool. The goal is not to offer these as separate resources, but to integrate them directly into lecture notes and worksheets.
To explore exactly how this can be implemented technically and conceptually, we have developed a prototype for a website builder for interactive lecture notes and worksheets. A unique feature of the prototype is that new and existing learning tools can be easily added through a flexible plugin system.
Wednesday, February 8, 2023: Clemens Weiße
Front-end development of a reduction trainer for students
Clemens describes the reduction trainer, its front-end components, the associated database, and the communication between all components of the reduction trainer. He then demonstrates its use with an example.
Thursday, February 2, 2023, Marco Sälzer
Expressibility of Graph Neural Networks Through the Lens of Formal Verification
In this talk, I will provide 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 the formal verification of GNNs.
Thursday, January 26, 2023: Kathrin Lehmann
Tool-Supported Learning in the Context of Computability Theory: A Backend Prototype for Automated Verification of Reductions
Thursday, January 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. The goal was to formalize three different semantics for this algebra and to prove the equivalence of two of these semantics in Isabelle/HOL. Furthermore, the thesis aimed to outline how a similar proof could be used to establish the equivalence of the third semantics to one of the first two.
Thursday, January 12, 2023: Stefan Kablowski
Computing All Minimal Corrections for a Word to Match a Context-Free Description
This work investigated the number of different ways in which a given word can be minimally rewritten so that the result belongs to a given context-free language. The concept of minimality was also to be clearly defined.
Thursday, December 15, 2022: Martin Lange
will present on the now-completed completeness proof in the well-known “Calculus of
Influence.”
Thursday, December 1, 2022: Janek Bürger
Student Assignment Submission Platform
This project resulted in a prototype web tool for the submission and automatic grading of student homework assignments. The tool includes a faculty page and a student page. On the instructor page, new assignments with grading criteria can be created, which are automatically graded by integrated tools. On the student side, assignments can be submitted for these tasks. In addition, all submissions and grades are stored in a database to make them available for statistical analysis; for example, they can be exported as a CSV file.
Thursday, November 24, 2022: Marco Sälzer
Because humans are poor teachers, neural networks do not understand NP-hardness!
Motivated by recent findings in the field of “Neural Algorithmic Learning”—that is, the learning of classical algorithms by deep learning models—I present papers by Yehuda et al. and Sanchis et al., which demonstrate that the way we train neural networks (and ML models in general) prevents these models from learning NP-hard problems (or causes them to merely pretend they can). Note: The talk is self-contained; no prior knowledge of machine learning is required.
Tuesday, November 15, 2022: Nicolai Fiege
Optimal Modulo Scheduling with SAT Solvers.
Modulo scheduling aims to speed up loop computations (for or while loops) by executing consecutive loop iterations nested within one another. Thus, the first operation of iteration 2 is executed before the last operation of iteration 1 has finished, and so on. The task of a modulo scheduling algorithm is to assign an execution time to each operation in the loop body such that (1) the loop’s execution time is minimized, (2) data dependencies within the loop are satisfied, and (3) resource constraints are met. In this presentation, we will demonstrate how we solve modulo scheduling using Boolean satisfiability (SAT) solvers.
Thursday, November 10, 2022: Luca Hertel
Integrating the FG learning tools with Moodle via the LTI interface
Tuesday, October 11, 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 us to prove hypotheses about systems that describe the influence of various variables on one another.
The goal of this thesis is to design an algorithm that uses these rules to prove such a hypothesis about a system. This algorithm should operate efficiently, with the term “efficiency” being further specified in the thesis. Furthermore, the algorithm will be implemented in Python to enable measurements and to evaluate its efficiency using real-world problems. For this purpose, measurement data will be used that can be transformed into scalable systems to allow conclusions to be drawn about the algorithm’s runtime behavior.
Friday, October 14, 2022: Shahla Rasulzade
On the modeling of biological influence experiments
Experimentation is a well-established learning mechanism in school subjects in the natural sciences, such as biology. To understand the basics of experimental design and formulate logically consistent hypotheses, students are expected to have some background knowledge and to focus on their own thinking. However, interaction with a teacher can distract a group of students from the thought processes they should engage in when designing an experiment.
The introduction of digital learning tools can help minimize such effects. We are working to create such a tool that can model influence experiments and allow their correctness to be verified using a simple proof system. I will present our model language and proof rules for influence experiments.
Wednesday, August 31, 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 currently lack anything similar. One reason for this is that a normal form for omega-regular languages must go beyond mere acceptance—for example, to have a normal form for a parity language, it should relate every infinite word to a natural color for that 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 demonstrate how this natural color can be derived from any deterministic parity automaton after two simple and efficient automaton transformations. We then show how this natural color provides a canonical representation for every ?-regular language.
Tuesday, April 5, 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 form the basis for fully specified mathematics.
This talk aims to provide a brief insight into the theorem prover Isabelle.
Thursday, March 3, 2022: Martin Lange
A Proof System for Statements about Influence in Biological Experiments
In biological school experiments, students are often required to formulate hypotheses about the influence relationship between variables occurring in these experiments. As part of our efforts to digitize such experiments, we have developed a modeling framework for these experiments and hypotheses, in which influence is characterized by the existence of partial functions on real numbers. I will present a simple proof system for the correctness of hypothesis statements in such experiments. The soundness of this system appears to be established, but the completeness and decidability of the proof search remain open questions. I will outline some ideas on how to establish these as well. This is joint work with Shahla Rasulzade.
Thursday, February 17, 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 a valid output given a valid input? It was recently claimed that the problem is NP-complete for general neural networks and conjunctive input/output specifications. We correct some flaws in the original proofs for the upper and lower bounds. 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 parameters involved.
Thursday, December 16, 2021: Shahla Rasulzade
Modeling biological experiments
Our study focuses on the creation of a digital learning tool capable of modeling a specific type of experiment in natural science school subjects, such as biology. It is developed using formal methods.
Our goal is to provide two frameworks for formal modeling—in other words, to develop two different experiment models. The first is an axiomatic approach, in which the correctness of hypotheses is reduced to the problem of proof search. The second is an operational approach, in which the correctness of hypotheses is reduced to model checking.
Wednesday, November 24, 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 with high expressive power, we obtain logics that retain some of the appealing pragmatic advantages of CTL and LTL, yet possess expressive power exceeding that of the modal μ-calculus or MSO. We advocate these logics by demonstrating how the recursion operator can be used to express interesting non-regular properties. We also study decidability and complexity issues related to standard decision problems.
Wednesday, November 10, 2021: Maurice Herwig
Calculation of a Weighting for Regular Languages
Results from his bachelor’s thesis
Thursday, September 9, 2021: Eric Alsmann
Inexpressibility Results for Propositional Dynamic Logic over Context-Free Programs
This paper compares the expressive power of PDL over regular, visibly-pushdown, and context-free languages, as well as the modal fixpoint logic vpFLC. Visibly Pushdown Fixpoint Logic with Chop (vpFLC) is a newly introduced decidable modal fixpoint logic capable of expressing non-regular properties. It is shown constructively, using a specific property, that vpFLC is genuinely more powerful than PDL over visibly-pushdown languages. Furthermore, the various PDL-based logics are constructively distinguished from one another. Finally, an overview of the different logics and their expressive power is provided.
Thursday, September 9, 2021: Georg Siebert
Toward an Artificial Teaching Assistant: Learning Grading Schemas for Finite Automata with GNNs
In this talk, we investigate the extent to which deep learning techniques are capable of grading student homework assignments. Specifically, we address the following question: Can we map a multi-valued grading scheme for homework assignments on the topic of “nondeterministic finite automata” using neural networks? We introduce graph neural networks (GNNs) as a suitable model for this task and describe the process from defining a grading scheme and formulating an appropriate classification task to designing and conducting corresponding experiments. Finally, we discuss our results for a specific homework assignment of this kind and provide an outlook on possible next steps.
Monday, July 5, 2021: Lukas Mentel
Detection and Elimination of Constants to Strengthen k-Induction
A major challenge in the practical application of formal methods is the high complexity of the systems being verified. By simplifying the input for model checkers and similar tools, the time required can be significantly reduced. This paper describes a technique for identifying variables that have a constant value, thereby accelerating the verification process.
Friday, March 19, 2021: Marco Sälzer
On Finite Convergence of the Modal Mu-Calculus
In this talk, we investigate a word structure with an infinite bisimulation quotient that guarantees finite convergence of all fixpoints definable in the modal mu-calculus. The talk does not require extensive background in this area of research, as we focus on understanding the result, why it is of interest, and what its implications are for the modal mu-calculus. Furthermore, we briefly examine how to prove this finite convergence property and encourage a discussion to gain deeper insights.
Thursday, March 5, 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, February 5, 2020: Stefan Göller
Stefan will continue his talk“On regularity of pushdown automata and related problems”
Wednesday, January 22, 2020: Stefan Göller
On regularity of pushdown automata and related problems
I will introduce a few problems on pushdown automata that I am currently working on and have worked on in the past. In particular, I plan to discuss in more depth a recent result with Pawel Parys: The problem of whether 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 blackboard talks on this topic.
Friday, November 22, 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, October 25, 2019: Marco Sälzer
will give a short talk about an on-the-fly model-checking algorithm for HFL.
Friday, October 18, 2019: Adrian Sturm
will present the results of his master’s thesis.
Monday, September 2, 2019: Benedikt Hruschka
Implementation of an interactive model checker for first-order logic over automatic structures
The talk will present the results of his master’s thesis.
Tuesday, July 16, 2019: Marco Sälzer
Marek Czarnecki investigated the question of whether there are modal logic formulas with a closure ordinal greater than omega. Here we summarize his work, focusing on developing a general understanding of how to construct formulas with a closure ordinal between omega and omega * 2. Furthermore, some related work is discussed to contextualize the topic within current research.
Friday, March 8, 2019: Lars Marquardt and Lukas Mäntel
We will hear two approximately 30-minute talks by Lars Marquardt and Lukas Mäntel. Lars Marquardt will give a talk on “Brzozowski’s derivatives,” and Lukas Mäntel will speak on “Quantifier elimination.”
Friday, January 18, 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, November 2, 2018: Lara Yörük
Proposal for a Modeling Language for Scientific Experiments
The goal of my dissertation is to develop a framework for modeling a wide variety of scientific experiments, which is intended for use in schools.
First, we need a mathematical modeling language that allows experiments to be created using a “building-block” approach. To define the semantics of the experiments, a hybrid system will be generated from the created model. In this talk, I would like to present a proposal for such a modeling language for discussion.
Friday, September 7, 2018: Martin Lange
Martin will present a small tool for the upcoming logic course
Friday, August 31, 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 with a simply typed lambda calculus, and is thus capable of expressing 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 current limitations in the algorithm’s efficiency.
Tuesday, July 3, 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 levels collapses into the alternation-free fragment, albeit with an increase in type level by one.
Friday, April 13, 2018: Florian Bruse
Fixpoint Stabilization on Certain Structure Classes
As part of our investigations into structure classes on which HFL fixpoint definitions become stable after a finite number of steps, it has become apparent that characterizing these classes is not so straightforward. We know that all structures with a finite bisimulation quotient possess this property, and we suspect that, for each fixed maximal type-theoretic order, there exist genuinely larger classes on which all fixed points up to that order become stable after a finite number of steps, but fixed points of higher order do not necessarily do so.
I will briefly provide some context and then present a fixed structure for which we conjecture that all fixed points in formulas of modal My calculus become stable after a finite number of steps, but for which we know that there exists an HFL[1] formula that only becomes stable starting at step omega.
Friday, March 16, 2018: Martin Lange
A small observation on the automata-theoretic decidability proof for Presburger arithmetic
Friday, February 16, 2018: Norbert Hundeshagen
Conjunctive grammars over single-element alphabets generate non-regular languages
Conjunctive grammars are an extension of context-free grammars by an explicit conjunction operator. It is well known that context-free grammars over single-element alphabets generate exactly the regular languages. It stands to reason that this also holds for conjunctive grammars. In this talk, a result by A. Jez will be presented showing that the language {a^4^n | n>0} can be generated by a conjunctive grammar.
Friday, December 1, 2017: Florian Bruse
Fixed-point alternation for HFL
A central question for fixed-point logics is whether mutual entanglement of the smallest and largest fixed points offers genuine added value or can always be eliminated. Fixed-point alternation makes formulas notoriously difficult to understand, and the model-checking problem for the modal “must” calculus, for example, includes the alternation degree of a formula as an input. For the mü-calculus, for example, it is known that it is generally not possible to remove fixed-point alternation, though it is possible to do so for the class of word structures.
In this talk, I will briefly introduce the topic and present the current state of research on higher-order modal fixed-point logic.
Friday, December 1, 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, November 2, 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—that is, the set of sequences of send operations it can perform—is the same whether its communications are FIFO asynchronous or simply rendezvous synchronizations. This property was claimed to be decidable in several conference and journal papers [1,2,3,4] for either mailbox (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 for either mailbox communications or peer-to-peer communications; therefore, the decidability of synchronizability remains an open question. We will resolve this question for peer-to-peer communications and show that,
, synchronizability is in fact 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, September 29, 2017: Daniel Kernberger
The Fully Hybrid μ-Calculus
We consider the hybridization of the μ-calculus through the addition of nominals, binder, and jump. In particular, the use of the binder distinguishes our approach from earlier hybridizations of the μ-calculus and also results in a more complex formal semantics. We then investigate the model-checking problem and establish ExpTime-completeness for the full logic, as well as 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 demonstrate that—unlike the non-hybrid case—the hybrid extension of the full branching-time logic CTL* is not a fragment of the fully hybrid μ-calculus.
Friday, September 22, 2017: Orcun Yörük
Simon—A Simulation Tool for Hybrid Systems
This master’s thesis focuses on the simulation of hybrid systems. Hybrid systems describe both discrete and continuous behavior. Therefore, they are well-suited for modeling state-based scenarios that involve time. To simulate such systems, a tool was developed as part of this thesis using the platform-independent programming language Java, which represents the theoretical findings in a practical implementation. The resulting tool, named Simon, enables the accurate simulation of hybrid systems.
Friday, September 15, 2017: Lara Yörük
SoPHY - A Specification Language for Hybrid Systems
This thesis contributes to three areas: hybrid systems, modeling languages, and educational software. It focuses on the development of SoPHY, a specification language for hybrid systems. The goal of this language is to describe scientific experiments. These experiments are modeled as hybrid automata. Based on SoPHY, a simulation tool can then be developed that is geared toward educational use in the field of self-directed learning.
Because it is closely based on experiments, the specification language is easy to read and self-explanatory. It is also easy for computers to process, as its structure is adapted to the well-known JSON format. This facilitates its subsequent use in the software.
Friday, September 1, 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 the 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 characterized by 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 consider only bounded buffers by requiring the function f to be Lipschitz continuous. This characterization holds only for certain restricted classes of automata. One of these automata should produce only words in which no letter commutes unboundedly to the left or right. We will show that such an automaton can be characterized by a cyclic-path-connected automaton, which is a refinement of a syntactic characterization of an automaton with a regular trace closure.
Friday, August 25, 2017: Florian Bruse
Space-Efficient Fragments of Higher-Order Fixpoint Logic
Higher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power far exceeds that of Monadic Second-Order Logic, achieved by incorporating 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 provide corresponding lower bounds. This yields generic results for the complexity of bisimulation-invariant non-regular properties, as these can typically be defined in HFL.
Friday, August 18, 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 as “automatic structures” in the field of predicate logic, or as “regular model checking” in formal verification. Both approaches use synchronized transducers, i.e., finite automata that read tuples of letters in each step. This is a strong transducer model with high expressive power, leading to the undecidability of model checking for any specification language capable of expressing transitive closure.
We develop conditions on a class of binary word relations that 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 its weaker expressive power, we find that this class satisfies the aforementioned sufficient conditions; thus, we obtain a decidability result for CTL model checking over a restricted class of infinite-state automatic structures.
Friday, July 21, 2017: Norbert Hundeshagen
Kleene’s Theorem and (At Least) One Monoid on Which It Does Not Hold
Friday, July 14, 2017:
Parity Games
Martin Lange - Positional determinacy of parity games
Denis Huseljic - Solving parity games by reduction to SAT
Marco Sälzer - Discrete strategy refinement
Florian Bruse - The fixed-point iteration algorithm
Friday, May 5, 2017: Georg Zetsche
Boolean closed full trios and rational Kripke frames
It is a well-known phenomenon that language classes induced by infinite-state systems typically lack the decidability and closure properties that make regular languages easy to analyze. Most notably, nondeterministic infinite-state systems typically fail to be closed under Boolean operations. In visibly pushdown automata, closure under Boolean operations is achieved, but at the cost of restricting the input alphabets used, meaning they are not closed under rational transductions.
This raises the question of whether there is some type of infinite-state system that is closed under both Boolean operations and rational transductions (and allows for the 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 entire arithmetic hierarchy (which significantly extends the recursively enumerable languages).
Wednesday, March 29, 2016: Arno Ehle
Automated Proofs in the Sequent Calculus Trainer
The presentation “Automated Proof Search for the Sequent Calculus Trainer” summarizes the results of the master’s thesis “Proof Search in the Sequent Calculus for First-Order Logic with Equality” by Arno Ehle. The Sequent Calculus Trainer is a program designed to support students in studying the sequent calculus. As an introduction, we will briefly demonstrate the Sequent Calculus Trainer, its past feature set, and what was still missing to support students even better. The main part of the presentation focuses on automated proof search. We will discuss the most significant challenges involved in performing automated proof search in the sequent calculus and present some solutions used in the master’s thesis. The final segment will feature a live demonstration of the Sequent Calculus Trainer, during which we will showcase the new features based on the findings of the master’s thesis.
Friday, February 24, 2016: Thao Nguyen
Formal verification of mobile robot protocols
Mobile robot networks have emerged in recent 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—that is, with a finite set of possible robot positions—under synchronous and asynchronous assumptions. The authors translate this formal model into the DVE language—the input format for the model-checkers DiVinE and ITS—and formally prove the equivalence of the two models. They then verify several instances of two existing protocols for variants of ring exploration in an asynchronous setting: exploration with a stop and perpetual exclusive exploration. For the first protocol, they refine the correctness bounds, and for the second, they provide a counterexample. For the second protocol, I also use the UPPAAL model-checking tool to re-verify the results.
Friday, November 4, 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 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 that stateless ordered restarting automata accept only regular languages.
Friday, July 15, 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 that restrict the interaction between hybrid operators and path formulae, in contrast to previous proposals in the literature that ignored potential problems with formal semantics. We then investigate the model-checking problem for these logics, obtaining complexities ranging from PSPACE-completeness to non-elementary decidability.
Friday, July 8, 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 a finite alphabet. We show that by using the tropical semiring, we can avoid the use of auxiliary symbols.
Furthermore, a certain type of (word-)weighted restarting automaton 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, July 1, 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 only 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, June 17, 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 for approximating 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 provide a topological characterization of the games using the notion of continuous and Lipschitz-continuous functions.
Friday, June 3, 2016: Florian Bruse
Alternating Krivine Automata
Alternating Parity Krivine Automata (APKA) provide operative semantics for Higher-Order Modal Fixpoint Logic (HFL). APKAs 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 outline how 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, April 15, 2016: Martin Lange
Higher-Order Fixpoint Logic
Higher-Order Fixpoint Logic (HFL) is an extension of the modal μ-calculus with 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 system, so a denotational semantics for fixpoint formulas over predicate transformers can be defined. This principle easily extends to higher-order functions.
We will introduce the syntax and semantics of HFL and provide some examples of properties expressible in HFL (but not in the mu-calculus), thereby attempting to offer some intuition on how such formulas can be read and understood. We will survey some known results regarding the expressive power and complexity of HFL, most importantly that the model-checking problem for the order-k fragment is complete in k-EXPTIME.
Friday, November 27, 2015: Martin Lange
LTL with Past: Expressiveness and Succinctness
We consider the linear-time temporal logic LTL enriched with temporal operators for the past, such as “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 provides a computable transformation of LTL+Past formulas to LTL that involves 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, if it exists, is not straightforward to demonstrate). We then present a clever argument by Laroussinie, Markey, and Schnoebelen, who proved the existence of an exponential succinctness gap between LTL+Past and LTL.
Thursday, November 17, 2015: Jörg Kreiker
Java Generics
Thursday, June 18, 2015: Maxime Folschette
Some Methods and Results on Biological Regulatory Networks
Biological Regulatory Networks (BRNs) are a broad class of qualitative models used to represent biological processes. Since their formalization (Kauffman, 1969 & Thomas, 1973), several interesting methods have emerged, leading to well-known results in this field. During this seminar, I will present some of the main results discovered regarding these models, while gradually shifting the focus to my field of research, which involves the use of formal methods to study the dynamics of BRNs.
Thursday, June 11, 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 converting a stateless deterministic ordered restarting automaton into an equivalent DFA is at least double exponential.
Here we show that the trade-off for converting 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 satisfying 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, May 28, 2015: Norbert Hundeshagen
Sequent Calculus Trainer
We present the Sequent CalculusTrainer, 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 that fosters an understanding of all the syntactic principles that must be followed when constructing correct proofs.
We also report on some empirical findings that indicate how the Sequent Calculus Trainer can improve students’ success in learning sequent calculus for full first-order logic.
Wednesday, April 29, 2015: Arno Ehle
Parity Games
This presentation deals with algorithms for parity games based on partial reductions to Büchi games. Here, the term “partial” refers, on the one hand, to how much information can be gleaned from the solution to a Büchi game and, on the other hand, to the principle of reduction itself. Three different approaches will be explained in this regard. The first approach enables a partial reduction to Büchi games by unrolling cycles in subgames, thereby generating a new game in each case that has one less priority. The second and third approaches extend the Büchi algorithm to include recursive calls to truly smaller subgames and solve the actual parity game by repeatedly calling this extended Büchi algorithm. All algorithms were implemented in the PGSolver project and compared with one another across various game families.
Wednesday, April 22, 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 viable alternative approach to solving language inclusion by trading 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 for pushdown automata but EXPTIME-complete for visibly pushdown automata. We show that the situation here 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, February 11, 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 computational problems involving strings and show how the polyadic modal μ-calculus can define their solutions. We use partial evaluation in a model-checking algorithm to obtain an efficient algorithm for the longest common substring problem. It demonstrates 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, February 4, 2015: Nobert Hundeshagen
A Hierarchy of Transducing Observer Systems
We primarily 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 position them between painter and length-reducing systems. Furthermore, 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 computed by transducing observer systems with weight-reducing rules is closed under intersection.
Wednesday, January 28, 2015: Arno Ehle
, “Model Checker”
This presentation introduces the “Model Checker” project, covering its objectives, implementation, and results. The “Model Checker” program offers the opportunity to interactively learn about and deepen one’s understanding of the relationship between first-order predicate logic formulas and their interpretations. The presentation includes a live demo that can incorporate suggestions from the audience.
Wednesday, January 14, 2015: Florian Bruse
The Canonical Model Technique for Modal Logic
Canonical models are a standard technique for establishing the completeness of a proof calculus for a modal logic. The successful construction of a canonical model implies the compactness of the logic in question. We will examine the technique for basic modal logic and how it must be extended for certain extensions, such as a fragment of PDL with intersection. If time permits, we will also explore how a similar technique works for non-compact logics.
Wednesday, December 17, 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 with 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 incorrect, and we will present several methods for determining this number to see in which cases it is a polynomial and in which it is not.
Wednesday, December 10, 2014: Maxime Folschette
Process Hitting
The representation and analysis of biological regulatory networks can be approached using formal methods. My work focuses on the use and enhancement of the expressiveness of Process Hitting, a recently introduced formalism that allows for the study of large models (up to hundreds of components). This framework in particular offers an efficient reachability analysis that avoids the usual combinatorial explosion associated with state graph computation.
Wednesday, November 26, 2014: Martin Lange
The Strictness of the Mu-Calculus Alternation Hierarchy over the Class of All Structures
In this final talk on the modal mu-calculus, we will show that the alternation hierarchy is generally strict—that is, more fixpoint alternation yields greater expressive power. Recall that for certain classes of structures, such as finite or infinite words, this is not the case.
The result was first established by Bradfield in 1996, and also independently by Lenzi that same year. The proof presented in this seminar is Arnold’s—a particularly elegant one—from 1999, which uses Banach’s Fixpoint Theorem. So most of the seminar will be devoted to discussing basic topology, namely complete metric spaces, etc. The actual proof of the alternation hierarchy is then a simple diagonalization argument using the fixed-point theorem and the Walukiewicz formulas, which determine whether or not an arbitrary μ-calculus formula of bounded alternation holds on a given structure.
Wednesday, November 19, 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. Although, in general, 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 arithmetic constraints on counters is NP-complete.
The proof technique used to obtain the NP upper bound leverages a stuttering theorem for (plain) Past LTL as well as properties regarding small integer solutions for quantifier-free Presburger formulas.
If time permits, results for extensions of LTL such as ETL, linear mu-calculus, or CTL* will also be discussed.
The talk is based on joint work with Amit Kumar Dhar and Arnaud Sangnier.
Wednesday, November 12, 2014: Martin Lange
The Collapse of the Mu-Calculus Alternation Hierarchy on Certain Classes of Structures
The goal of this short series of talks on 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 or words. That is, every formula is equivalent over such structures to one with “very little” fixpoint alternation.
The main motivation for these results stems from two facts: first, that fixpoint alternation—
—makes it difficult to understand the properties expressed by formulas; and second, that—
—it largely determines the complexity of model checking: the currently best-
’s algorithms are polynomial in the size of the structure and formula but exponential in its alternation depth.
Wednesday, November 5, 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 if and only if player 0 wins the game from that 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 straightforward μ-calculus model-checking algorithm: fixpoint iteration. This is also one of the few algorithms—if not the only one—that was not originally designed for solving parity games. While an empirical study quickly shows that this does not yield an algorithm that works well in practice, it is interesting from a theoretical standpoint for two reasons: first, it is exponential on virtually all families of games that were designed as lower bounds for very specific algorithms, suggesting that fixpoint iteration is related to all of them. Second, fixpoint iteration does not compute positional winning strategies. Note that the Walukiewicz formulas only define winning regions; additional work is needed to enable this algorithm to compute winning strategies. We show that these are specific exponential-space strategies that we call eventually-positional, and we demonstrate how positional strategies can be extracted from them.
Wednesday, October 29, 2014: Martin Lange
Introduction to the Modal Mu-Calculus
No Abstract
Friday, September 12, 2014, at 2:00 p.m.: 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 the 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 through a deterministic process. The family of all languages that recognize a picture in this way is abbreviated as DREC.
The second and entirely different definition uses a tiling system to recognize a picture by proceeding from one corner to the diagonally opposite corner. Due to this procedure, the class of all such languages is abbreviated as Diag-DREC. We show that Diag-DREC is not closed under intersection and union, whereas 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. Given that Diag-DREC is equal to the closure under rotation of the family of all two-dimensional deterministic online tessellation 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 obtained by merging Higher-Order Fixpoint Logic and the Polyadic $\mu$-Calculus—two formalisms originally introduced as expressive languages for program specification. Polyadicity enables formulas to make assertions about tuples of states rather than states alone. PHFL inherits from Higher-Order Fixpoint Logic the ability to formalize properties using higher-order functions.
We consider PHFL in the context of descriptive complexity theory: its fragment that does not use any higher-order functions 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 provide characterizations of PSPACE and NLOGSPACE using certain formulas from these two fragments, which can be regarded as containing only tail-recursive functions.
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, June 4, 2014, at 5:00 a.m.: Thorsten Löbig
Investigation into the Applicability of Formal Methods Using the Example of an Infusion Pump.
Model checking makes it possible to formally verify whether a system is a model of a given specification. It is thus also potentially possible to demonstrate the absence of certain classes of errors.
However, techniques from this field have so far found little application in 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’s thesis, I investigated the applicability of currently available model checkers within the context of a real-world large-scale software project (software for an infusion pump). In this presentation, I will present the results of my work and demonstrate the capabilities and limitations of the model checkers I examined using illustrative application examples.
Wednesday, May 14, 2014, at 10:00 a.m.: Richard Petersen, University of Kassel
Growing Context-Sensitive Matrix Grammars
In this thesis, the matrix languages introduced by the Sironmneys are combined with 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 find 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, May 7, 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, such as 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 of the two, is already PSPACE-hard—that is, computationally as hard as language inclusion itself. Continuous simulation is even EXPTIME-hard. We also provide corresponding 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 to verify the correctness of a sentence in a natural language. To study quantitative aspects of restarting automata, we introduce the concept of a weighted restarting automaton. By examining 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 present a few preliminary results on the properties of weighted restarting automata.
Monday, March 24, 2013, at 10:00 a.m.: Daniel Kernberger, University of Kassel
Weak alternating automata are not that weak
Automata on infinite words are used for the specification and verification of non-terminating programs. Different types of automata offer varying levels of expressive power, conciseness, and complexity. Alternating automata possess both existential and universal branching modes and are particularly well-suited for program specification. In a weak alternating automaton, the state space is partitioned into partially ordered sets, and the automaton can proceed from a given 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, consequently, 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, November 20, 2013, at 10:00 a.m.: Dr. Rüdiger Ehlers, University of Kassel
Synthesis with Identifiers
We consider the synthesis of reactive systems from specifications with identifiers. Identifiers are useful for parameterizing the input and output of a reactive system, e.g., to specify 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 may 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 provide 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 demonstrates the practical applicability of our algorithm.
Monday, October 14, 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 determines 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 justify this result by examining how certain Zeno properties can be model-checked, such as for a system that needs to interact with a Zeno environment.
Wednesday, October 9, 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 time. His thesis focused on RoCTL*, an extension of the common branching time logic CTL* for reasoning about robustness. RoCTL* is no more expressive than CTL* but has been shown to be exponentially succinct. Recent work has focused on decision tableaux for weaker logics, including BCTL* and Non-Local BCTL*.
The non-local tableau is used in ongoing work on the automatic verification of rewrite rules, with sample applications for crowdsourcing and the automatic generation of rewrite rules. Other ongoing research includes a model checker for a recently specified language used to express models for any satisfiable Real Temporal Logic formula, as well as potential extensions to Metric Temporal Logic.
Wednesday, July 3, 2013: Michael Falk and Etienne Lozes
Michael Falk: Fixed-Point Iteration for Solving Parity Games
This talk presents the results of the bachelor’s thesis of the same name.
Etienne Lozes: On Decision Problems for Probabilistic Büchi Automata
This talk is based on the slides by Nathalie Bertrand. people.rennes.inria.fr/Nathalie.Bertrand/pba-lsv.pdfs. I will try to understand most of that and present it. In short, probabilistic Büchi automata are Büchi automata in which 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, March 27, 2013, 11:30 a.m., Room WA1318: Milka Hutagalung (University of 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 remains a challenging problem. We introduce two new sequences of simulation relations, called multi-letter simulations, in which the Verifier must reproduce the Refuter’s moves by 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 simulations, have greater potential for an incremental inclusion test, as their size generally grows more slowly. We evaluate this idea experimentally and show that incremental inclusion testing can outperform the most advanced Ramsey-based algorithms by two orders of magnitude. This is a joint work with Martin Lange and Etienne Loze.
Wednesday, March 6, 2013, 11:00 a.m., Room WA1318: Manuel Vargas Guzmán (University of Kassel)
Model-Checking Process Equivalences.
Process equivalences are formal methods that relate programs and systems which, informally, behave in the same way. Since there is no single definition of what it means for two dynamic systems to exhibit the same behavior, there are a multitude of formal process equivalences—ranging from bisimulation to trace equivalence—categorized along the linear-time/branching-time spectrum. We present a logical framework based on an expressive modal fixpoint logic capable of defining many process equivalence relations: for each such equivalence, there is a fixed formula that is satisfied by a pair of processes if and only if they are equivalent with respect to this relation. We explain how to perform model checking—even symbolically—for a significant fragment of this logic that captures many process equivalences. This enables 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 work is presented in two papers—a conference paper and an extended version—written together with Martin Lange, Etienne Lozes, and myself.
Wednesday, January 23, 2013, 11:00 a.m., Room WA1318: Bahareh Badban (University of Kassel)
Three-Valued Abstraction-Refinement for Real-Time Systems.
The modeling of many real-world systems requires dense time domains to reflect the fact that events may occur arbitrarily close to one another in actual applications. Timed automata have emerged as a means of modeling such systems. Our goal is to improve the scalability of real-time model checking by developing a CEGAR-based framework grounded in three-valued logic. In general, CEGAR involves the iterative refinement of over-approximated models based on the analysis of counterexamples until no further counterexamples can be found. Our aim is to develop a fully automatic predicate abstraction method for the verification of concurrent dense real-time systems. The idea behind abstraction is to reduce dense timed automata to automata of a finite, manageable size. With the goal of improving the scalability of existing techniques, we have begun developing an algorithm that strengthens the automaton by discovering new hidden state invariants. A particular challenge lies in integrating various forms of inter-process communication into our algorithms. In a joint project with Martin Lange, we have expanded the initial results into a research proposal.
Wednesday, November 14, 2012, 11:00 a.m., Room WA1318: Martin Lange (University of 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 still lacks a satisfactory, sound, and complete axiomatization. The only known proof system for CTL* is Reynolds’ system, which involves a complex and lengthy completeness proof and, most importantly, uses rules that do not possess the subformula property.
We consider a large fragment of CTL* characterized by disallowing certain nestings of temporal operators inside universal path quantifiers. This fragment subsumes CTL+, for example. 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 techniques, such that the results represent proofs in a Hilbert-style axiom system for this fragment. The completeness of this axiomatization is a simple consequence of the soundness of the satisfiability games. (Joint work with Markus Latte.)
Wednesday, July 11, 2012, 11:00 a.m., Room WA1318: Bahareh Badban (University of 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 as follows: 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, June 20, 2012, 11:00 a.m., Room WA1318: Etienne Lozes (University of Kassel)
Separation Logic.
Part Two: Expressivity and Complexity. In this talk, we will introduce several decision problems related to separation logic and show how solving them can help verify heap-manipulating programs with varying degrees of automation. While discussing these problems, it will be interesting to consider issues of expressiveness and to examine the extension of Separation Logic to arbitrary graphs, known as Spatial Logic for Graphs. We will attempt to provide a comprehensive overview of the results—in particular, connections to (monadic) second-order logic—and explain which decision procedures are used in existing tools.
Wednesday, June 13, 2012, 11:00 a.m., Room WA1318: Etienne Lozes (University of 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 when it starts, it ensures B when it stops.” Separation Logic is an extension of Hoare-Floyd logic for reasoning about programs. The main component of separation logic is a second-order connective called separating conjunction: A*B asserts that the state consists of two disjoint parts, one satisfying A and the other satisfying B. This connective provides a new interpretation of a Hoare triple {A} p {B}: “if p can consume A when it starts, then it has sufficient resources to run safely, and it produces B when it stops”. Less than ten years after its theoretical foundation, Separation Logic is beginning to prove, through impressive automated tools, that it is a successful approach for verifying large amounts of low-level C code (Apache, Linux, etc.) and for effectively handling many small but intricate concurrent algorithms (e.g., lock-free concurrent data structures). The logical foundations, issues of expressiveness, and decision procedures have been greatly clarified since 2000. However, Separation Logic remains a very active field of research in all these areas and beyond.
Part One: Foundations. In this talk, we will introduce the general problem of verifying heap-manipulating programs; we will define a simple programming language and the core of Separation Logic’s proof system. We’ll illustrate this with several examples of standard yet subtle algorithms for recursive data structures, which often offer significant gains in conciseness and readability compared to other formalisms. We’ll discuss semantic issues, as well as ways to formally prove that a well-verified program possesses certain desirable properties.
Wednesday, May 30, 2012, 11:30 a.m., Room WA1318: Waled Almakhawi (University of Freiburg / University of Hodeidah, Yemen)
Landmarks in Directed Model Checking.
Model checking involves determining whether a given system description satisfies a given property. In the case of erroneous systems, a counterexample is returned. Numerous studies have been conducted to find efficient techniques capable of identifying error states within the system model’s state space in an efficient manner. Large system models have a vast number of states in their state space, making it very costly to enumerate the entire state space. Therefore, there is a strong need to identify guiding information that can address the problem of large state spaces. Directed model checking employs methods that can direct the search process toward error states. It utilizes the concept of heuristic functions to determine the order in which states should be processed during state space traversal in order to quickly locate an error state. In this thesis, we introduce the concept of landmarks to directed model checking. Landmarks were originally introduced in AI planning. They provide additional information that can be integrated alongside the heuristic function. Landmarks are specific formulas that must be satisfied on the path to every error state. We will demonstrate how landmarks can be extracted and ordered, and how we can use these orderings to optimize the search and advise the model checker on the best next step to take toward the error state. We have implemented our approach in the mcta model checker. Our experiments show that performance improvements can sometimes be achieved.
Wednesday, May 2, 2012, 11:00 a.m., Room WA1318: Martin Lange (University of Kassel)
Parity Games: Theory, Practice, Applications
Parity games are two-player games played on a (usually finite) directed graph in which each node has a priority. The winner of an infinite game is determined by the parity of the highest priority that occurs infinitely often in the game. This seemingly arbitrary concept encompasses all sorts of other winning conditions—namely, all those that can be expressed as an omega-regular set of plays. It also possesses nice algorithmic properties as well as a rich theory, even though the exact computational complexity of the problem of solving parity games remains unknown to this day. In this talk, I will begin by providing 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 field of formal methods, most notably satisfiability checking and program synthesis problems. I will also present PGSolver—a tool designed to solve parity games efficiently in practice—and highlight some (surprising?) discrepancies between its behavior in practice and theoretical predictions. I will conclude with an overview of potential future 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, February 8, 2012, 2:00 p.m., Room WA1318: Norbert Hundeshagen (University of Kassel)
Characterizing Rational Functions via Restarting Transducers
Rational relations are the well-known class of relations defined as the rational subsets of the product of two monoids. This talk focuses on a proper subset of these relations: rational functions. Here we characterize these functions and some of their proper subclasses using certain types of deterministic restarting transducers with window size one. A restarting transducer is a restarting automaton equipped with an output function.
Wednesday, February 1, 2012, 2:00 p.m., Room WA1318: Friedrich Otto (University of 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 generate only context-sensitive languages. In the literature, it is claimed that this result extends to centralized PC grammar systems with context-sensitive components that operate in nonreturning mode. Here, however, we show that the class of languages generated by centralized PC grammar systems with context-sensitive components operating in nonreturning mode coincides with the complexity class NEXT.
Wednesday, November 23, 2011, 2:00 p.m., Room WA1318: Peter Cerno (Charles University in Prague)
Clearing Restarting Automata
Restarting automata were introduced as a model for analysis by reduction, which is a linguistically motivated method for checking the correctness of a sentence. We propose a new restricted version of restarting automata called clearing restarting automata, which has a very simple definition but exhibits interesting properties with respect to their potential 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 delta-clearing restarting automata, which is capable of recognizing all context-free languages. We also discuss some open problems and possible directions for future research in this area.
Wednesday, November 9, 2011, 2:00 p.m., Room WA1318: Martin Lange (University of 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 such as satisfiability, subsumption, equivalence, etc., then translate into questions about automata such as emptiness, inclusion, language equivalence, etc. Linear-time temporal logics such as 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 resorting to intermediate automaton models, such as nondeterministic ones. The method is a direct adaptation of the size-change termination principle, which was originally used to determine the termination of abstract functional programs.
Wednesday, September 19, 2012, 2:00 p.m., Room WA1318: Bahareh Badban (University of 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 verifying the safety properties of real-time systems. Many of the classical automata-theoretic decision problems are undecidable for timed automata; for example, the subsumption problem and the universality problem. In this paper, we consider restrictions of these problems: universality for deterministic timed automata and the subsumption of a nondeterministic timed automaton 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 only domains of timed words of bounded length and show that each bounded instance is NP-complete. We present some experimental data obtained from a prototypical implementation that measures the practical feasibility of the approach to timed automata using SMT solvers.
Wednesday, July 13, 2011, 11:00 a.m., Room WA1318: Norbert Hundeshagen (University of Kassel)
Characterizing Regular Languages Using Nonforgetting Restarting Automata
The restarting automaton is a machine model motivated by the technique of analysis by reduction from linguistics. Essentially, it can be viewed as an extension of the finite-state automaton. It is well known that certain types of restarting automata with window size one compute exactly the regular languages. This talk focuses on these types of automata that are 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, July 13, 2011, 11:30 a.m., Room WA1318: Marcel Vollweiler (University of Kassel)
Pushdown Automata with Translucent Pushdown Symbols
Pushdown automata with translucent pushdown symbols are presented. Such a device is a pushdown automaton $M$ equipped with a {`transparency relation'}~$\tau$. In a transition step, $M$ does not read (and replace) the topmost symbol on its pushdown store, but rather the topmost symbol that is covered only by translucent symbols. We prove that these automata accept all recursively enumerable languages. We then focus on pushdown automata with translucent pushdown symbols that operate in real time or quasi-real time. We compare the corresponding language classes to other classical complexity classes and study closure properties for these language classes.
Wednesday, June 22, 2011, and June 29, 2011, 11:00 a.m., Room WA1318: Martin Lange (University of Kassel)
Tableaux(-Like) Decision Procedures for Temporal Logics
Temporal logics are modal logics over infinite flows of time. They serve as important tools for specifying program behavior. Their satisfiability problems therefore constitute the algorithmic core of consistency checks for logical specifications of correct program behavior.
Temporal operators are typically characterized elegantly 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 specific difficulties for deciding satisfiability: one must 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 from 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 specific prior knowledge of temporal logics is required. However, participants are expected to have some general knowledge of logic. Some knowledge of automata theory will be helpful but is not essential.
Wednesday, June 15, 2011, 11:00 a.m., Room WA1318: Bahareh Badban (University of Kassel)
Toward an Automated Predicate Abstraction of Dense Real-Time Automata
Real-time requirements—particularly those involving strict real-time bounds—play a crucial role in the design of concurrent, embedded real-time systems. In many application areas, such as transportation, process control, or medical automation, these systems are safety-critical; that is, their malfunction could result in loss of life. Efficient verification technology is therefore a crucial requirement for the real-time system design process. Due to the inherent complexity of these systems, manual verification approaches are impractical.
To scale existing verification strategies to the analysis of real-world systems of realistic size, our goal is to develop an automatic, abstraction-based verification approach for concurrent dense real-time models. During the verification of a system, it becomes apparent that many important properties of real-time designs are, in fact, safety properties. Safety properties can be checked using reachability analysis of the real-time model. Therefore, in our investigations, we will focus on solving this class of problems. Our aim is to develop a fully automatic predicate abstraction method for the verification of concurrent dense real-time systems. The idea behind abstraction is to reduce dense timed automata to finite, tractable automata. With the aim of improving the scalability of existing techniques, we have begun developing an algorithm that first identifies idle transitions imposed by hidden-state invariants. A particular challenge lies in accommodating various forms of inter-process communication. 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)
Cooperative Distributed Systems of Stateless Deterministic Restart Automata with Window Size One
The restarting automaton is a machine model inspired 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 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, whereas stateless deterministic R(1)-automata accept only 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 accept only 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-systems are not required to be stateless, then these systems are strictly more expressive, since they then even accept some languages that are not semi-linear.
Tuesday (!), February 22, 2011, 10:15 a.m., Room WA1318: Markus Latte (LMU Munich)
Separation Results for XCTL
XCTL[A] is an extension of CTL that refines the temporal “until” and “release” operators using formal languages in A. In this way, XCTL can express non-regular properties, unlike CTL. For regular, visibly pushdown, and deterministic context-free languages, the separation of the respective XCTL can be proven using automata-theoretic techniques. However, these techniques introduce non-determinism on the automata side. Since non-determinism is also the difference between DCFL and CFL, these techniques appear to be unsuitable for separating XCTL[DCFL] from XCTL[CFL]. Nevertheless, we demonstrate the separation of DCFL from CFL for the EF/AG fragment of XCTL.
Friday (!) January 21, 2011, 10:15 a.m., 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 initially devoted to the specification of mobile processes. They were subsequently extended to static structures, including XML documents and graphs. Almost at the same time, Separation Logic gained popularity through Reynolds’ 2002 LICS invited paper, and to this day continues to grow in influence across many areas of research, encompassing both theoretical and highly practical aspects. In this talk, I will attempt to provide an overview of the theoretical aspects of my work (I will omit the more practical aspects I have been involved in over the past few years), with a shift in focus from Spatial Logic toward Separation Logic. I will present results on expressivity, decidability, and complexity for several spatial and separation logics, whether or not they are extended by temporal constructs.
December 15, 2010, 3:15 p.m., Room WA1318: Norbert Hundeshagen (University of Kassel)
Transducing by Observing
A large portion of the computational models developed in recent years have been motivated by biochemical processes. Many of these mechanisms follow the well-known black-box concept: An input is directly converted into an output, which is the result of the computation and provides insight into the computational power. The observer systems that are the focus of this talk take a different approach: what is of interest is not exclusively the output of such a system, but rather the change in the system itself. The computational power of various speech-generating or speech-recognition systems has already been investigated in this context. Here, this concept is extended to include observer systems that compute transductions.
December 1, 2010, 3:15 p.m., Room WA1318: Martin Lange (University of Kassel)
Bounded Model Checking and Analysis of Context-Free Grammars
Many problems concerning context-free grammars are undecidable, such as ambiguity, universality, subsumption, equivalence, etc. However, if these are restricted to words of a maximum 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 encoding, and determines whether there exists a word of length at most k that is not generated by the grammar. If one now successively increases the parameter k, one naturally obtains a semi-decision procedure for the respective original problem.
A similar technique—albeit “only” a reduction from PSPACE to NP—is used in bounded model checking. In addition, we take advantage of the fact that problems in NP can often be solved well by SAT solvers.
In this talk, we will first introduce Bounded Model Checking and then show how this technique can be applied to the problems mentioned above to obtain semi-decision schemes that are even usable in practice.
November 10, 2010, 3:00 p.m., Room WA2104: Jan Hoffmann (LMU Munich)
Analyzing Sorting Algorithms with Resource-Aware ML
We recently developed an automatic amortized analysis to compute polynomial resource bounds for first-order functional programs at compile time. It is based on 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 the pros and cons, I will compare our automatic analysis to a manual analysis of the algorithms found in a popular textbook.
For more information, see the project’s website: raml.tcs.ifi.lmu.de