Themen für Studentische Arbeiten

Model checking is the task of determining whether a reactive system meets a given formal specification, typically expressed in a form of temporal logic. Systems may either be explicitly, by enumerating all system sttates, or in a more compact symbolic representation. The aim of the thesis is to transform existing generic model checking algorithms for coalgebraic fixpoint logics into a symbolic variant.

Many modal and description logic reasoners rely on the tableau methor, which essentially attempts to construct countermodels from syntactic material. The aim of the thesis is to implement the actual extraction of models from runs of a tableau procedure within the Coalgebraic Ontology Logic Solver COOL, a versatile reasoner for a wide variety of logics.

Finite automata have been widely used in computer science and engineering for decades as a powerful tool for modeling and analyzing a wide range of systems and processes. There are various types of automata, such as the classical non-deterministic finite automata (NFA), which works with sets, or the non-deterministic orbit-finite automata (NOFA), which work with nominal sets. These types of automata can be uniformly captured by a notion of automaton in a category, more precisely, a topos.

The language semantics for automata in a topos is straightforward. Since these automata are coalgebras they also have an ensuing coalgebraic semantics. The question is whether this coincides with the language semantics. To answer this question affirmatively one should use the internal language of toposes. In addition (or alternatively) a more direct diagrammatic proof should be possible, and it could be compared with the topos theoretic one. This topic will require a good working knowledge in category theory and the theory of coalgebras. Prior knowledge in topos theory as well as their internal logic would be rather helpful but is not strictly required.

Art der Arbeit: Masterprojekt (ambitioniert) oder Masterarbeit

Ansprechpartner: Stefan Milius

In probabilistischen Beschreibungs- und Modallogiken werden Constraints auf die Wahrscheinlichkeiten für Eigenschaften zufälliger Nachfolger formalisiert, iwie etwa in „der aktuelle Zustand gerärt mit Wahrscheinlichkeit hächstens 5% in einen Deadlock“. Solche Logiken sollen als Instanz in den am Lehrstuhl in Kooperation mit der Australian National University entwickelten generischen Bescheibungslogikreasoner COOL (Coalgebraic Ontology Logic Solver) eingebunden werden.

In der unscharfen Logik (Fuzzy Logic) werden die klassischen Wahrheitswerte “wahr”/“falsch” ersetzt durch Wahrheitsgrade, typischerweise Zahlen zwischen 0 und 1. Über den ursprünglich rein propositionalen Formalismus hinaus gibt es mittlerweile ausdrucksstarke unscharfe Logiken; eine interessante Klasse noch entscheidbarer Logiken dieser Art sind die unscharfen Beschreibungslogiken (Fuzzy Description Logics). Effiziente Deduktionsalgorithmen für Fuzzy DLs werden gerade erst entwickelt, wie etwa dieser hier. Es liegt bereits eine Implementierung eines Tableaualgorithmus für fuzzy ALC vor; mögliche weitere Themen betreffen die systematische Optimierung des Algorithmus und die Erweiterung auf ausdrucksstärkere Logiken.

Art der Arbeit: Bachelor- oder Masterarbeit

Ansprechpartner: Lutz Schröder

Leichtgewichtige Beschreibungslogiken zeichnen sich durch geringe Ausdrucksstärke bei gleichzeitiger effizienter Entscheidbarkeit der zentralen Schlussfolgerungsprobleme aus. Die zur Zeit vielleicht erfolgreichste leichtgewichtige Beschreibungslogik ist EL, das auch die in wichtigen großen Ontologien wie SNOMET CT verwendet wird. Wir haben eine koalgebraische Verallgemeinerung von EL entwickelt, in der statt der üblichen relationalen Modalitäten auch z.B. verschiedene spielorientierte Modalitäten verwendet werden können. Ein Reasoner für koalgebraisches EL ist in Vorarbeiten bereits implementiert worden. Als weitere Arbeiten bieten sich systematische Evaluationen sowie eine Erweiterung sowohl der Theorie als auch der Implementierung auf sogenannte general concept inclusions an.

Art der Arbeit: Bachelor- oder Masterarbeit

Ansprechpartner: Lutz Schröder

Koalgebraische Modallogik dient als allgemeines Rahmenwerk für Modallogiken jenseits der relationalen Welt, z.B. für probabilistische oder spieltheoretische Modalitäten. Die meisten Resultate in der koalgebraischen Modallogik haben als Gültigkeitsbereich ausschließlich solche Logiken, die, ähnlich wie die Beschreibungslogik ALC bzw. die relationale Modallogik K, nur durch sogenannte Rang-1-Axiome, also solche, in denen alle aussagenlogischen Variablen unter genau einer Modalität stehen, definiert sind (im Falle von K lautet das Axiom [](a→b) → []a → []b). In diesem Projekt soll die Allgemeinheitsebene auf solche Axiome angehoben werden, in denen zwar noch keine geschachtelten Modalitäten, wohl aber Vorkommen von aussagenlogischen Variablen außerhalb von Modaloperatoren erlaubt sind; Grundbeispiel hierfür ist die Modallogik T, die Reflexivität definiert und K um das Axiom []a → a erweitert.

Art der Arbeit: Bachelor- oder Masterarbeit

Ansprechpartner: Lutz Schröder

Der klassische mu-Kalkül ist ein Formalismus u.a. zur Beschreibung nebenläufiger Systeme. Seine koalgebraische Variante (siehe z.B. hier) deckt in uniformer Weise verschiedene interessante Erweiterungen ab, wie z.B. den alternierenden mu-Kalkül (zur Beschreibung von Agentensystemen) oder den gradierten mu-Kalkül (mit Zähloperatoren, etwa zur Messung von Redundanz). Als theoretische Arbeiten in diesem Gebiet bieten sich die Entwicklung von Modellprüfungsalgorithen (model checker) oder eine Kodierung von Nominalen, also Namen für einzelne Zustände, an.

Art der Arbeit: Bachelor- oder Masterarbeit

Ansprechpartner: Lutz Schröder