Upper seminar "Theoretical computer science

Im Oberseminar  "Theoretische Informatik" tragen Mitarbeiter, interessierte Studenten und Gäste über aktuelle Forschungsarbeiten im Bereich der theoretischen Informatik vor.

Donnerstag am 17.8.2023: Lukas Mentel

IC3 / PDR meets SMT-LIB

Für das symbolische Model Checking wird häufig Bounded Model Checking in Verbindung mit k-Induktion eingesetzt. IC3 ("Incremental Construction of Inductive Clauses for Indubitable Correctness") [1] stellt eine Alternative zu diesem Ansatz dar und ist sicherlich eine der wichtigsten Neuerungen der vergangenen 15 Jahre in diesem Bereich [2].
Wie bereits dem Namen zu entnehmen ist, wird hierbei schrittweise eine Formelmenge modifiziert, mit dem Ziel, eine (1-induktive) Invariante zu erhalten.
In diesem Vortrag wird ein Überblick über IC3 und dessen Variante PDR gegeben. Zusätzlich wird ein Implementierungsansatz vorgestellt, der auf dem SMT-LIB-Standard aufbaut.

[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.

Donnerstag, 1.6.2023: Georg Sieberg

GeNNifier - Verifikation auf Graph Neural Networks (GNNs)

Über die Verifikation von neuronalen Netzen (NN) kann sichergestellt werden, dass diese bestimmten Spezifikationen erfüllen. Eine Untergruppe der NN sind die Graph neuronalen Netze (GNN), welche als Eingabe Graphen entgegennehmen. Für die Verifikation von GNNs gibt es zwar einzelne Verifikationsalgorithmen, jedoch nutzen diese kein einheitliches Format, um auf den GNNs zu arbeiten. Ein einheitliches Format für NN ist das Open Neural Network Exchange (ONNX) Format. Dieses ermöglicht es, NN unabhängig von gängigen Machine Learning (ML) Frameworks (z.B. Pytorch oder Tensorflow) darzustellen. Jedoch unterstützen die ML Frameworks den Export von GNNs nach ONNX nicht vollständig. Des Weiteren gehen beim Export des GNNs Strukturinformationen verloren.
Ziel des Master-Projektes ist es ein Tool zu entwickeln, welches eine ML-Framework unabhängige Darstellung schafft, welche als Basis für Verifikationsverfahren von GNNs dienen soll. Dafür ist das Python-Tool "GeNNifier" entstanden. Dieses bietet eine auf JSON aufsetzende High-Level Darstellung von GNNs, womit Konfigurationen von GNNs erstellt werden können. Eine solche Konfiguration kann von "GeNNifier" eingelesen werden und über eine Schnittstelle in einen Verifikationsalgorithmus weiterverarbeitet werden.
Um die Einsetzbarkeit von "GeNNifier" für Verifikationsverfahren zu erproben, wurde der Naive Output Reachability Verification (NORV) Algorithmus in "GeNNifier" implementiert. Dieses Verfahren arbeitet auf Message Passing Neural Networks (MPNN), welches eine Form von GNNs sind.
Der NORV Algorithmus wandelt ein MPNN in mehrere Feedforward NN (FNN) um. Anschließend wird nacheinander auf den erstellten FNN ein Verifikationsverfahren für das Output Reachability Problem angewendet, bis eine Lösung gefunden ist. Die Implementierung in "GeNNifier" deckt den Algorithmus bis zur Umwandlung des MPNN in ein FNN ab. Dabei werden die generierten FNN im ONNX Format ausgegeben, um eine möglichst breite Anzahl an Verifizierern zu unterstützen.

Donnerstag, 25.5.2023: Eric Alsmann

Eine Einführung in die Architektur von Transformer-Modellen und die Limits zugehöriger Verifikationsprobleme

Motiviert durch den Erfolg generativer Sprachmodelle wie GPT und Bard, geht es in meiner Masterarbeit um theoretische Limits in der Verifikation solcher Modelle. Der Vortrag gibt eine Einführung in die Architektur von Transformer-Modellen und das Konzept der Self-Attention.
Anschließend werden verschiedene Verifikationsprobleme für Transformer und ihre Entscheidbarkeit diskutiert.
Für den Vortrag sind keine besonderen Vorkenntnisse notwendig.

Mittwoch, 3.5.2023: John Hundhausen

Ein Website-Baukasten für interaktive Vorlesungsskripte und Arbeitsblätter

Moderne Web-Technologien machen es möglich, interaktive Visualisierungen, verschiedene Übungen und sogar Übungen, die automatisch korrigiert werden, als zusätzliche Lerntools für Studierende bereitzustellen. Im Fachgebiet Theoretische Informatik/Formale Methoden entstehen in verschiedenen Projekten genau diese Art von Lerntools. Nun sollen diese nicht zusätzlich angeboten werden, sondern direkt in die Vorlesungsskripte und Arbeitsblätter integriert werden.
Um zu erforschen, wie genau das technisch und konzeptuell umgesetzt werden kann, haben wir einen Prototyp für einen Website-Baukasten für interaktive Vorlesungsskripte und Arbeitsblätter entwickelt. Eine Besonderheit des Prototyps ist, dass neue und bereits existierende Lerntools durch ein flexibles Plugin-System einfach hinzugefügt werden können.
Mittwoch, 8.2.2023: Clemens Weiße
Frontend-Entwicklung eines Reduktions-Trainers für Studierende
Clemens beschreibt den Reduktions-Trainer, dessen zum Frontend gehörende Komponenten, der zugehörigen Datenbank und der Kommunikation zwischen allen Komponenten des Reduktions-Trainers. Anschließend führt er beispielhaft dessen Verwendung durch.

Donnerstag, 2.2.2023, Marco Sälzer

Expressibility of Graph Neural Networks Through the Lens of Formal Verification

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

Donnerstag, 26.1.2023: Kathrin Lehmann

Toolgestütztes Lernen im Kontext der Berechenbarkeitstheorie: ein Backend-Prototyp zur automatisierten Überprüfung von Reduktionen
 

Donnerstag, 19.1.2023: Lars-Eric Marquardt

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

Das Thema der Arbeit war die formale Verifikation unterschiedlicher Semantiken für eine abstrakte Fixpunkt-Algebra höherer Ordnung in Isabelle/HOL. Dabei sollten drei unterschiedliche Semantiken für diese Algebra formalisiert werden, und die Äquivalenz zweier dieser Semantiken in Isabelle/HOL nachgewiesen werden. Weiterhin sollte skizziert werden, inwiefern ein ähnlicher Beweis auch für die Äquivalenz der dritten Semantik zu einer der ersten beiden geführt werden könnte.

Donnerstag, 12.1.2023: Stefan Kablowski

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

Die Arbeit hat untersucht, auf wie viele verschiedenen Wegen sich ein gegebenes Wort in mininaler Art und Weise so umschreiben lässt, dass das Ergebnis in einer gegebenen kontextfreien Sprache liegt. Dabei sollte auch der Begriff der Minimalität sauber definiert werden.

Donnerstag, 15.12.2022: Martin Lange

wird über den nun fertigen Vollständigkeitsbeweis im bereits bekannten "Calculus of
Influence" vortragen.

Donnerstag, 1.12.2022: Janek Bürger

Studentische Abgabe-Plattform

In dem Projekt entstand ein Prototyp Webtool für die Abgabe und automatische Bewertung von studentischen Hausaufgaben. Das Tool beinhaltet eine Dozentenseite sowie eine Studentenseite. Auf der Dozentenseite lassen sich neue Aufgaben mit Bewertungskriterien erstellen, die von eingebundenen Tools automatisch bewertet werden. Auf Studentenseite können für diese Aufgaben Abgaben eingereicht werden. Darüber hinaus werden alle Abgaben sowie Bewertungen in einer Datenbank gespeichert, um sie für statistische Erhebungen bereitzustellen, beispielsweise steht ein Export als CSV Datei zur Verfügung.

Donnerstag, 24.11.2022: Marco Sälzer

Weil der Mensch ein schlechter Lehrer ist, verstehen neuronale Netze NP-Schwere nicht!

Motiviert durch neuerliche Ergebnisse aus dem Bereich des "Neural Algorithmic Learning", also dem Erlernen klassischer Algorithmen durch Deep Learning  Modelle, stelle ich Arbeiten von Yehuda et al. und Sanchis et al. vor, welche aufzeigen, dass die Art und Weise wie wir neuronale Netze (und ML-Modelle im Allgemeinen) trainieren dazu führt, dass diese Modelle NP-schwere Probleme nicht erlernen können (oder nur so tun als würden sie es). Hinweis: Der Vortrag ist in sich geschlossen, das heißt es wird kein besonderes Wissen über maschinelles Lernen vorausgesetzt.

Dienstag, 15.11.2022: Nicolai Fiege

Optimales Modulo Scheduling mit SAT Solvern.

Modulo Scheduling hat das Ziel, Schleifenberechnungen (For- oder While-Loops) zu beschleunigen, indem aufeinander folgende Schleifeniterationen ineinander verschachtelt ausgeführt werden. Die erste Operation aus Iteration 2 wird also ausgeführt, bevor die letzte Operation aus Iteration 1 fertig wurde, usw. Die Aufgabe eines Modulo-Scheduling-Algorithmus ist es, jeder Operation des Loop-Bodys einen Ausführungszeitpunkt zuzuweisen, sodass (1) die Ausführungszeit der Loop minimiert wird, (2) Datenabhängigkeiten innerhalb der Loop und (3) Ressourcenbeschränkungen eingehalten werden. Im Vortrag wird gezeigt, wie wir Modulo Scheduling mit Hilfe von Boolean Satisfiability (SAT)-Solvern lösen.

Donnerstag,10.11.2022: Luca Hertel

Anbindung der FG-Lerntools an Moodle mittels LTI-Schnittstelle

Dienstag, 11.10.2022: Sören Möller

An Efficient Algorithm for Proof Search in the Calculus of Influence

Der "Calculus of Influence" besteht aus Regeln, die es erlauben, Hypothesen über Systeme zu beweisen, welche den Einfluss von verschiedenen Größen aufeinander beschreiben.
Ziel der Arbeit ist es, einen Algorithmus zu entwerfen, welcher mithilfe dieser Regeln den Beweis einer solchen Hypothese über ein System führt. Dieser sollte effizient arbeiten, wobei der Begriff der "Effizienz" in der Arbeit weiter spezifiziert wird. Des Weiteren wird der Algorithmus in Python implementiert, um Messungen durchführen zu können und die Effizienz anhand von echten Problemstellungen zu bewerten. Dafür werden Messdaten verwendet, welche in skalierbare Systeme transformiert werden können, um Aussagen über das Laufzeitverhalten des Algorithmus zuzulassen.

Freitag, 14.10.2022: Shahla Rasulzade

On the modeling of biological influence experiments

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

Mittwoch, 31.8.2022: Rüdiger Ehlers

Natural Colors of Infinite Words.

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

Dienstag, 5.4.2022: Lars-Eric Marquardt

Isabelle: Ein Theorembeweiser

Theorembeweiser sind Tools mit denen man die Korrektheit von Programmen beweisen kann. Im Vergleich zu Model Checkern und SAT-Solvern bringen Theorembeweiser einen hohen Grad an Interaktivität mit sich. "Machine-checked formal proofs" führen zu zuverlässigen Programmen und sind die Basis für vollständig spezifizierte Mathematik.
Dieser Vortrag soll einen kleinen Einblick in den Theorembeweiser Isabelle geben.

Donnerstag, 3.3.2022: Martin Lange

A Proof System for Statements about Influence in Biological Experiments

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

Donnerstag, 17.2.2022: Marco Sälzer

Reachability is NP-Complete Even for the Simplest Neural Networks

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

Donnerstag, 16.12.2021: Shahla Rasulzade

Modeling biological experiments

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

Mittwoch, 24.11.2021: Martin Lange

Temporal Logic with Recursion

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

Mittwoch, 10.11.2021: Maurice Herwig

Berechnung einer Gewichtung regulärer Sprachen

Ergebnisse seiner Bachelorarbeit

Donnerstag, 9.9.2021: Eric Alsmann

Inexpressibility Results for Propositional Dynamic Logic over Context-Free Programs

In dieser Arbeit wird die Ausdrucksstärke von PDL über regulären, visibly-pushdown und kontextfreien Sprachen, sowie der modalen Fixpunktlogik vpFLC verglichen. Visibly Pushdown Fixpoint Logic with Chop (vpFLC) ist eine neu eingeführte entscheidbare modale Fixpunktlogik, welche nicht-reguläre Eigenschaften ausdrücken kann. Es wird konstruktiv anhand einer konkreten Eigenschaft gezeigt, dass vpFLC echt ausdrucksstärker als PDL über visibly-pushdown Sprachen ist. Außerdem werden die verschiedenen PDL-basierten Logiken konstruktiv voneinander getrennt. Zum Ende wird noch ein Überblick über die verschiedenen Logiken und ihrer Ausdrucksstärke gegeben.

Donnerstag, 9.9.2021: Georg Siebert

Auf dem Weg zum künstlichen Lehrassistenten: Das Lernen von Bewertungsschemata für endliche Automaten mit GNNs

In diesem Vortrag untersuchen wir inwiefern Deep Learning Techniken in der Lage sind studentische Hausaufgaben zu bewerten. Konkret betrachten wir folgende Fragestellung: Können wir ein mehrwertiges Bewertungsschema für Hausaufgaben bezüglich dem Thema "Nichtdeterministische endliche Automaten" mithilfe von Neuronalen Netzwerken abbilden? Wir stellen das für diese Aufgabe geeignete Modell der Graph Neural Networks vor und beschreiben den Prozess von Definition eines Bewertungsschemas über die Formulierung einer geeigneten Klassifikationsaufgabe bis zur Konzeption und Durchführung entsprechender Experimente. Zum Abschluss diskutieren wir unsere Ergebnisse für eine konkrete solche Hausaufgabe und geben einen Ausblick zu möglichen nächsten Schritten.

Montag, 5.7.2021: Lukas Mentel

Detection and Elimination of Constants to Strengthen k-Induction

Ein wesentliches Problem beim Einsatz formaler Methoden in der Praxis stellt die große Komplexität der verifizierten Systeme dar. Durch die Vereinfachung der Eingabe für Model Checker und ähnliche Werkzeuge kann die benötigte Zeit deutlich reduziert werden. In dieser Arbeit wird eine Technik beschrieben, um Variablen zu identifizieren, die einen konstanten Wert aufweisen, und dadurch den Verifikationsprozess zu beschleunigen.

Freitag, 19.3.2021: Marco Sälzer

On Finite Convergence of the Modal Mu-Calculus

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

Donnerstag, 5.3.2020: Martin Lange

Existential Length Universality

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

Mittwoch, 5.2.2020: Stefan Göller

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

Mittwoch, 22.1.2020: Stefan Göller

On regularity of pushdown automata and related problems

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

Freitag, 22.11.2019: Martin Lange

From the modal mu-calculus to HFL

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

Freitag, 25.10.2019: Marco Sälzer

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

Freitag, 18.10.2019: Adrian Sturm

wird die Ergebnisse seiner Masterarbeit vorstellen.

Montag, 02.09.2019: Benedikt Hruschka

Implementierung eines Interaktiven Model-Checkers für erststufige Logik über automatischen Strukturen

Im Vortrag wird das Ergebnis seiner Masterarbeit vorgestellt.

Dienstag, 16.07.2019: Marco Sälzer

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

Freitag, 08.03.2019: Lars Marquardt und Lukas Mäntel

Wir hören dabei zwei ca. 30-minütige Vorträge von Lars Marquardt und Lukas Mäntel. Lars Marquardt wird einen Vortrag zum Thema "Brzozowski's derivatives" halten und Lukas Mäntel zum Thema "Quantoreneliminierung".

Freitag, 18.01.2019: David Kronenberger

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

Freitag, 02.11.2018: Lara Yörük

Vorschlag für eine Modellierungssprache für naturwissenschaftliche Experimente

Das Ziel meiner Dissertation ist, ein Framework für die Modellierung verschiedenster naturwissenschaftlicher Experimente zu entwickeln, welches Anwendung in Schulen finden soll.
Zunächst ist dafür eine mathematische Modellierungssprache gesucht, mit der Experimente „baukastenartig“ erstellt werden können. Zur Definition der Semantik der Experimente soll aus dem erstellten Modell ein hybrides System generiert werden. Einen Vorschlag für eine solche Modellierungssprache möchte ich in diesem Vortrag zur Diskussion stellen.

Freitag, 07.09.2018: Martin Lange

Martin will present a small tool for the upcoming logic course

Freitag, 31.08.2018: Marco Sälzer

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

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

Dienstag, 03.07.2018: Florian Bruse

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

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

Freitag, 13.04.2018: Florian Bruse

Fixpunktstabilisation auf bestimmten Strukturklassen

Im Rahmen unserer Untersuchungen zu Strukturklassen, auf denen HFL-Fixpunktdefinitionen schon nach endlich vielen Schritten stabil werden, hast sich herausgestellt, dass die Charakterisierung dieser Klasse(n) gar nicht so einfach ist. Wir wissen, dass alle Strukturen mit endlichem Bisimulationsquotienten diese Eigenschaft haben, und wir vermuten, dass jeweils für fixe maximale typtheoretische Ordnung echt größere Klassen bestehen, auf denen alle Fixpunkte bis zu dieser Ordnung nach endlich vielen Schritten stabil werden, Fixpunkte höherer Ordnung aber nicht unbedingt.
Ich werde kurz etwas zum Kontext sagen und dann eine fixe Struktur angeben, von der wir vermuten, dass alle Fixpunkte in Formeln des modalen My-Kalküls nach endlich vielen Schritten stabil werden, von der wir aber wissen, dass es eine HFL[1]-Formel gibt, die erst ab Schritt omega stabil wird.

Freitag, 16.03.2018: Martin Lange

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

Freitag, 16.02.2018: Norbert Hundeshagen

Konjunktive Grammatiken über einelementigen Alphabeten generieren nicht-reguläre Sprachen

Konjunktive Grammatiken sind eine Erweiterung der kontextfreien Grammatiken um einen expliziten Konjunktionsoperator. Es ist bekannt, dass kontextfreie Grammatiken über einelementigen Alphabeten genau die regulären Sprachen generieren. Die Vermutung liegt nahe, dass dies auch für konjunktive Grammatiken gilt. Im Vortrag wird ein Resultat von A. Jez gezeigt, dass die Sprache {a^4^n | n>0} durch eine konj. Grammatik generiert werden kann.

Freitag, 01.12.2017: Florian Bruse

Fixpunktalternierung für HFL

Eine zentrale Frage für Fixpunktlogiken ist, ob wechselseitige Verschränkung von kleinsten und größten Fixpunkten einen echten Mehrwert bietet, oder immer eliminiert werden kann. Fixpunktalternierung macht Formeln notorisch schwer verständlich und das Model-Checking Problem für den modalen mü-Kalkül enthält zum Beispiel den Alternierungsgrad einer Formel als Eingabe. Für den  mü-Kalkül weiß man zum Beispiel, dass es im Allgemeinen nicht möglich ist Fixpunktalternierung zu entfernen, über der Klasse der Wortstrukturen allerdings schon.
In diesem Vortrag führe ich kurz in die Thematik ein und stelle ich den Forschungsstand für modale Fixpunktlogik höherer Ordnung vor.

Freitag, 01.12.2017: Daniel Kernberger

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

Donnerstag, 02.11.2017: Etienne Lozes

Synchronizability of Communicating Finite State Machines is not Decidable

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

Freitag, 29.09.2017: Daniel Kernberger

The Fully Hybrid μ-Calculus

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

Freitag, 22.09.2017: Orcun Yörük

Simon - Ein Simulationstool für Hybride Systeme

In dieser Masterarbeit geht es um die Simulation von Hybriden Systemen. Hybride Systeme beschreiben sowohl diskretes als auch kontinuierliches Verhalten. Daher sind sie gut geeignet, um zustandsbasierte Szenarien zu modellieren, welche einen Bezug zur Zeit haben. Um solche Systeme zu simulieren, wurde im Rahmen dieser Arbeit ein Tool mithilfe der plattformunabhängigen Programmiersprache Java entwickelt, welches die gesammelten theoretischen Erkenntnisse in einer praktischen Umsetzung repräsentiert. Das entstandene Tool mit dem Namen Simon lässt die korrekte Simulation von Hybriden Systemen zu.

Freitag, 15.09.2017: Lara Yörük

SoPHY - A specification language for hybrid systems

Diese Arbeit leistet einen Beitrag zu den drei Themen, Hybride Systeme, Modellierungssprachen und Bildungssoftware. Hierbei wird die Spezifikationssprache für Hybride Systeme, SoPHY, entwickelt. Das Ziel dieser Sprache ist, wissenschaftliche Experimente zu beschreiben. Diese Experimente werden in Form von Hybriden Automaten modelliert. Auf Basis von SoPHY kann dann ein Simulationstool entwickelt werden, welches auf den didaktischen Einsatz im Themenbereich Selbstgesteuertes Lernen ausgerichtet ist.

Die Spezifikationssprache ist durch ihre nahe Anlehnung an Experimente leicht lesbar und selbsterklärend. Sie ist außerdem leicht durch Computer zu verarbeiten, da ihr Aufbau an das bekannte JSON Format angepasst ist. Das erleichtert ihre spätere Verwendung in der Software.

Freitag, 01.09.2017: Milka Hutagalung

Topological Characterisation of Multi-Buffer Simulation

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

Freitag, 25.08.2017: Florian Bruse

Space-Efficient Fragments of Higher-Order Fixpoint Logic

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

Freitag, 18.08.2017: Martin Lange

Model Checking CTL over Restricted Classes of Automatic Structures

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

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

Freitag, 21.07.2017: Norbert Hundeshagen

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

Freitag, 14.07.2017:

Paritätsspiele

Martin Lange - Positionale Determiniertheit von Paritätsspielen

Denis Huseljic - Paritätsspiele per Reduktion auf SAT lösen

Marco Sälzer - Diskrete Strategieverbesserung

Florian Bruse - Der Fixpunktiterationsalgorithmus

Freitag, 05.05.2017: Georg Zetsche

Boolean closed full trios and rational Kripke frames

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

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

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

Mittwoch, 29.03.2016: Arno Ehle

Automatisierte Beweise im Sequenzenkalkül-Trainer

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

Freitag, 24.02.2016: Thao Nguyen

Formal verification of mobile robot protocols

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

Freitag, 04.11.2016: Kent Kwee

Ordered Restarting Automata: The Benefit of Patterns

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

Freitag, 15.07.2016: Daniel Kernberger

Model Checking for the Full Hybrid Computation Tree Logic

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

Freitag, 08.07.2016: Qichao Wang

Weighted Restarting Automata as Language Acceptors

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

Freitag, 01.07.2016: Kent Kwee

Ordered RRWW-Automata

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

Freitag, 17.06.2016: Milka Hutagalung

Buffered Simulation Games

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

Freitag, 03.06.2016: Florian Bruse

Alternating Krivine Automata

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

Freitag, 15.04.2016: Martin Lange

Higher-Order Fixpoint Logic

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

Freitag, 27.11.2015: Martin Lange

LTL with Past: Expressiveness and Succinctness

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

Donnerstag, 17.11.2015: Jörg Kreiker

Java Generics

Donnerstag, 18.06.2015: Maxime Folschette

Some Methods and Results on Biological Regulatory Networks

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

Donnerstag, 11.06.2015: Kent Kwee

On Some Decision Problems for Stateless Deterministic Ordered Restarting Automata

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

Mittwoch, 28.05.2015: Norbert Hundeshagen

Sequent Calculus Trainer

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

Mittwoch, 29.04.2015: Arno Ehle

Parity Games

Dieser Vortag befasst sich mit Algorithmen für Paritätsspiele auf Basis partieller Reduktionen auf Büchi-Spiele. Dabei bezieht sich der Begriff partiell zum einen darauf, wie viele Informationen aus der Lösung eines Büchi-Spiels gewonnen werden können und zum anderen auf das Prinzip der Reduktion an sich. Diesbezüglich werden drei verschiedene Ansätze erläutert. Der erste Ansatz ermöglicht eine partielle Reduktion auf Büchi-Spiele durch das Ausrollen von Zyklen in Teilspielen, wodurch jeweils ein neues Spiel erzeugt wird, das eine Priorität weniger besitzt. Der zweite und dritte Ansatz erweitern den Büchi-Algorithmus um rekursive Aufrufe auf echt kleineren Teilspielen und lösen durch mehrfaches Aufrufen dieses erweiterten Büchi-Algorithmus das eigentliche Paritätsspiel. Alle Algorithmen wurden in dem Projekt PGSolver implementiert und auf verschiedenen Spiele-Familien miteinander verglichen.

Mittwoch, 22.04.2015: Martin Lange

Language Inclusion

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

Mittwoch, 11.02.2015: Martin Lange

Model Checking for String Problems

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

Mittwoch, 04.02.2015: Nobert Hundeshagen

A Hierarchy of Transducing Observer Systems

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

Mittwoch, 28.01.2015: Arno Ehle

Model Checker

In dem Vortrag wird das Projekt "Model Checker" vorgestellt, wobei Bezug auf die Aufgabenstellung, die Umsetzung und die Ergebnisse genommen wird. Das Programm "Model Checker" bietet die Möglichkeit interaktiv den Zusammenhang zwischen Formeln der Prädikatenlogik erster Stufe und deren Interpretationen zu erlernen bzw. zu vertiefen. In den Vortag integriert ist eine Live-Demo, die die Anregungen des Hörerkreises miteinbeziehen kann.

Mittwoch, 14.01.2015: Florian Bruse

The Canonical Model Technique for Modal Logic

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

Mittwoch, 17.12.2014: Kent Kwee

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

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

Mittwoch, 10.12.2014: Maxime Folschette

Process Hitting

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

Mittwoch, 26.11.2014: Martin Lange

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

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

Mittwoch, 19.11.2014: Stéphane Demri

Verification of Linear-Time Properties on Flat Counter Systems

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

Mittwoch, 12.11.2014: Martin Lange

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

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

Mittwoch, 05.11.2014: Florian Bruse

The Fixpoint-Iteration Algorithm for Parity Games

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

Mittwoch, 29.10.2014: Martin Lange

Introduction to the Modal Mu-Calculus

No Abstract

Freitag, 12.09.2014 um 14:00 Uhr: David Kronenberger

Comparing two different classes of deterministic recognizable picture languages

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

Mittwoch, 25.06.2014 um 10:00 Uhr: Etienne Lozes, Uni Kassel

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

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

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

While many characterisations 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 characterises complexity classes by fragments of this generic framework.

Mittwoch, 04.06.2014 um 05:00 Uhr: Thorsten Löbig

Untersuchung zur Anwendbarkeit von Formalen Methoden am Beispiel einer Infusionspumpe.

Model Checking ermöglicht es formal nachzuweisen, ob ein System ein Modell einer gegebenen Spezifikation ist. Es ist damit auch potentiell möglich, die Abwesenheit von bestimmten Fehlerklassen zu zeigen.
Techniken aus diesem Gebiet haben bisher jedoch kaum Eingang in die moderne Softwareentwicklung gefunden. Die Hauptgründe hierfür sind das "State-space explosion" Problem und das nötige Expertenwissen, um diese Werkzeuge effektiv einsetzen zu können.
In meiner Bachelor Arbeit habe ich die Anwendbarkeit von heute verfügbaren Model Checkern im Rahmen eines realen Software-Großprojekts (Software einer Infusionspumpe) untersucht. In dem Vortrag stelle ich die Ergebnisse meiner Arbeit vor und demonstriere die Möglichkeiten und Limitationen der untersuchten Model Checker mit anschaulichen Anwendungsbeispielen.

Mittwoch, 14.05.2014 um 10:00 Uhr: Richard Petersen, Uni Kassel

Growing Context-Sensitive Matrix Grammars

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

Mittwoch, 07.05.2014 um 10:00 Uhr: Etienne Lozes, Uni Kassel

Buffered Simulation Games for Büchi Automata

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

Mittwoch, 30.04.2014 um 10:00 Uhr: Qichao Wang, M.Sc., Uni Kassel

Weighted Restarting Automata

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

Montag, 24.3.2013 um 10:00 Uhr: Daniel Kernberger, Uni Kassel

Weak alternating automata are not that weak

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

Mittwoch, 20.11.2013 um 10:00 Uhr: Dr. Rüdiger Ehlers, Uni Kassel

Synthesis with Identifiers

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

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

Model Checking for Compositional Models of General Linear Time

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

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

Algorithms and Temporal Logics

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

Mittwoch, 3.7.2013: Michael Falk und Etienne Lozes

Michael Falk: Fixpunkt-Iteration für das Lösen von Paritätsspielen

In diesem Vortrag werden die Ergebnisse der gleichnamigen Bachelor-Arbeit präsentiert.

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

This will be a talk based on the slides of Nathalie Bertrand. people.rennes.inria.fr/Nathalie.Bertrand/pba-lsv.pdf. I will try to understand most of that and present it. In short, Probabilistic Büchi Automata are Büchi automata where the non-determinism is replaced by a random choice. An infinite word defines thus 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.

Mittwoch, 27.03.2013, 11:30 Uhr, Raum WA1318:  Milka Hutagalung (Uni Kassel)

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

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

Mittwoch, 06.03.2013, 11:00 Uhr, Raum WA1318:  Manuel Vargas Guzmán (Uni Kassel)

Model-Checking Process Equivalences.

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

Mittwoch, 23.01.2013, 11:00 Uhr, Raum WA1318: Bahareh Badban (Uni Kassel)

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

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

Mittwoch, 14.11.2012, 11:00 Uhr, Raum WA1318: Martin Lange (Uni Kassel)

Branching Time? Pruning Time!

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

Mittwoch, 11.7.2012, 11:00 Uhr, Raum WA1318: Bahareh Badban (Uni Kassel)

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

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

Mittwoch, 20.6.2012, 11:00 Uhr, Raum WA1318: Etienne Lozes (Uni Kassel)

Separation Logic .

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

Mittwoch, 13.6.2012, 11:00 Uhr, Raum WA1318: Etienne Lozes (Uni Kassel)

Separation Logic .

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

Mittwoch, 30.5.2012, 11:30 Uhr, Raum WA1318: Waled Almakhawi (Uni Freiburg / Hodeidah Uni, Yemen)

Landmarks into Directed Model Checking.

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

Mittwoch, 2.5.2012, 11:00 Uhr, Raum WA1318: Martin Lange (Uni Kassel)

Parity Games: Theory, Practice, Applications

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

Mittwoch, 8.2.2012, 14:00 Uhr, Raum WA1318: Norbert Hundeshagen (Uni Kassel)

Characterizing the Rational Functions by Restarting Transducers

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

Mittwoch, 1.2.2012, 14:00 Uhr, Raum WA1318: Friedrich Otto (Uni Kassel)

On Centralized PC Grammar Systems with Context-Sensitive Components

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

Mittwoch, 23.11.2011, 14:00 Uhr, Raum WA1318: Peter Cerno (Karls-Universität Prag)

Clearing Restarting Automata

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

Mittwoch, 9.11.2011, 14:00 Uhr, Raum WA1318: Martin Lange (Uni Kassel)

Size-Change Termination and Emptiness for Alternating Parity Automata

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

Mittwoch, 19.9.2012, 14:00 Uhr, Raum WA1318: Bahareh Badban (Uni Kassel)

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

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

Mittwoch, 13.7.2011, 11:00 Uhr, Raum WA1318: Norbert Hundeshagen (Uni Kassel)

Characterizing the Regular Languages by Nonforgetting Restarting Automata

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

Mittwoch, 13.7.2011, 11:30 Uhr, Raum WA1318: Marcel Vollweiler (Uni Kassel)

Pushdown Automata with Translucent Pushdown Symbols

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

Mittwoch, 22.6.2011 und 29.6.2011, 11:00 Uhr, Raum WA1318: Martin Lange (Uni Kassel)

Tableaux(-Like) Decision Procedures for Temporal Logics

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

Mittwoch, 15.6.2011, 11:00 Uhr, Raum WA1318: Bahareh Badban (Uni Kassel)

Towards an Automatized Predicate Abstraction of Dense Real-Time Automata

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

Mittwoch, 1.6.2011, 11:00 Uhr, Raum WA1318: Friedrich Otto (Uni Kassel)

Kooperierende verteilte Systeme von zustandslosen deterministischen Restart-Automaten mit Fenstergröße eins

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

Dienstag (!), 22.2.2011, 10:15 Uhr, Raum WA1318: Markus Latte (LMU München)

Separation Results for XCTL

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

Freitag (!) 21.1.2011, 10:15 Uhr, Raum WA1318: Etienne Lozes (RWTH Aachen)

From Spatial Logics to Separation Logic

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

15.12.2010, 15:15 Uhr, Raum WA1318: Norbert Hundeshagen (Uni Kassel)

Transducing by Observing

Ein Großteil der in den letzten Jahren entwickelten Berechnungsmodelle wurde durch biochemische Prozesse motiviert. Viele dieser Maschinismen folgen dabei dem bekannten black-box-Konzept: Eine Eingabe wird direkt in eine Ausgabe überführt, welche das Ergebnis der Berechnung ist und Aufschluss über die Berechnungskraft gibt. Die in diesem Vortrag im Mittelpunkt stehenden Beobachtersysteme nutzen einen anderen Ansatz: Von Interesse ist nicht ausschließlich das Produkt eines solchen Systems, sondern die Veränderung des Systems selber. Die Berechnungskraft verschiedener Spracherzeugender oder -akzeptierender Systeme ist in diesem Zusammenhang bereits untersucht worden. Dieses Konzept wird hier um Beobachtersysteme erweitert, die Transduktionen berechnen.

1.12.2010, 15:15 Uhr, Raum WA1318: Martin Lange (Uni Kassel)

Bounded Model Checking und Analyse kontext-freier Grammatiken

Viele Probleme über kontext-freie Grammatiken sind unentscheidbar, wie z.B. Mehrdeutigkeit, Universalität, Subsumption, Äquivalenz, etc. Schränkt man diese jedoch auf Wörter einer maximalen Länge ein, so sind sie typischerweise in NP oder coNP. Bsp.: Das beschränkte Universalitätsproblem nimmt als Eingabe eine kontext-freie Grammatik und eine Zahl k in unärer Kodierung und entscheidet, ob es ein Wort der Länge höchstens k gibt, welches nicht von der Grammatik erzeugt wird. Erhöht man sukzessive nun den Parameter k, so erhält man natürlich ein Semi-Entscheidungsverfahren für das jeweils ursprüngliche Problem.
Eine ähnliche Technik - allerdings "nur" eine Reduzierung von PSPACE auf NP - wird beim Bounded Model Checking eingesetzt. Zusätzlich macht man sich zunutze, dass Probleme in NP oft gut von SAT-Solvern gelöst werden können.
In diesem Vortrag stellen wir zunächst Bounded Model Checking vor und zeigen dann, wie sich diese Technik auf die oben genannten Probleme anwenden lässt, um in der Praxis sogar verwendbare Semi-Entscheidungsverfahren zu gewinnen.

10.11.2010, 15:00 Uhr, Raum WA2104: Jan Hoffmann (LMU München)

Analyzing Sorting Algorithms with Resource Aware ML

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