Themen für Studentische Arbeiten

Aktive Lernalgorithmen für Automaten haben praktische Relevanz im Bereich des black-box testings, in welchem man aus einem unbekannten zustandsbasierten System einen formalen äquivalenten Automaten konstruiert um diesen mit Hilfe von Modellprüfungsmethoden dann auf Korrektheit zu prüfen. Seit den 1990ern sind auch Automaten mit Speichermöglichkeiten (Registerautomaten, siehe Kaminski/Francez 1994 [1] u.a.) relevant. Mit ihnen ist es möglich sogenannte Datensprachen (formal gesehen: Sprachen über einem unendlichen Alphabet) zu akzeptieren. Schröder/Kozen/Milius/Wißmann [2] haben 2017 Automaten mit Namensbindung (RNNAs) entwickelt, die entscheidbare Modellprüfungsprobleme haben. Vereinfacht gesagt akzeptieren diese Automaten λ-Terme ohne Klammern modulo α-Äquivalenz und bestimmte Datensprachen über die Entfernung von Bindern. Frank/Milius/Rot/Urbat [3] haben 2026 einen Lernalgorithmus für RNNAs und andere Automaten mit Namensbindung entworfen, welcher klassische Lernalgorithmen für DEAs/NEAs nimmt und mit Hilfe eines teaching assistants einen Automaten mit Namensbindung lernt.

In der Bachelor- oder Masterarbeit geht es hauptsächlich um die Implementierung und das Testen eben dieses Lernalgorithmus. Für eine Bachelorarbeit soll der im Aufsatz [3] beschriebene Algorithmus in einer frei wählbaren Zielsprache unter Einhaltung standardmäßiger Programmierrichtlinien implementiert werden und anschließend mit zufälligen Automaten getestet werden. Es geht hierbei insbesondere um die Implementierung zweier Grundbausteine des Lernalgorithmus, nämlich einerseits die Findung eines α-äquivalenten Repräsentanten und andererseits um die Akzeptanzfrage modulo α-Äquivalenz bei Automaten.
Für eine Masterarbeit soll sich zudem mit der Frage nach sinnvollen Testsuiten für die praktische Implementierung von Äquivalenzanfragen im Rahmen des Automatenlernens beschäftigt werden. Die von den in Frage stehenden Automaten akzeptierten Sprachen haben dabei einen „endlichen“ Kern, welcher von klassischen DEAs/NEAs akzeptiert wird und die Sprache bis auf α-Äquivalenz eindeutig beschreibt. Können somit Testsuiten von DEAs/NEAs einfach auf diese Automaten hochgezogen werden?

Vorwissen wird keines direkt benötigt, allerdings kann Vorwissen in Automatenlernen (bspw. über Aufzeichnungen der gleichnamigen Vorlesung aus dem WS2025/26) oder nominalen Techniken (bspw. über Aufzeichnungen der Vorlesung „Nominal Sets“ aus dem SS2024) von Vorteil sein.

Modallogik wird gerne als logisches Werkzeug bei der Formalisierung der Begriffe von Möglichkeit (possibility) und Notwendigkeit (necessity) verwendet. Die probabilistische Modallogik erweitert die klassische durch das zusätzliche Erfassen von Unsicherheit im zu formalisierenden System. Besonders für die Logik und Formalisierung von Interesse ist dabei die Erfüllbarkeitsprüfung (satisfiability checking). Wir interessieren uns hier für eine Implementierung bereits bestehender Algorithmen im Rahmen des am Lehrstuhl entwickelten generischen Logikinferenztools COOL (Gitlab des Lehrstuhls).

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.

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.

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.

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.

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.

Ansprechpartner: Lutz Schröder