Prof. Jan-Georg Smaus

Forschung

Die meiste Forschung entstand in Zusammenarbeit mit verschiedenen Kollegen.

In meiner Lehre beschäftige ich mich seit fast zehn Jahren mit interaktivem Theorembeweisen. Seit 2008 habe ich dieses Gebiet auch in meine Forschung aufgenommen und eine Brücke zu meiner Forschung im Model-Checking geschlagen. In einer Arbeit wird ein Teil eines Model-Checking-Verfahrens für Büchi-Automaten und Temporallogik mittels interaktivem Theorembeweisen verifiziert. Ich habe ein DFG-Projekt bewilligt bekommen, um mehr Arbeiten auf diesem Gebiet vorzunehmen. Das Projekt wird voraussichtlich Anfang 2011 starten.
Seit 2004 habe ich innerhalb des AVACS-Projekts zu hybriden und Realzeitautomaten gearbeitet.
- Heuristische Suche in Realzeitautomaten. Ich interessiere mich für die Anwendung von Ideen aus der Künstlichen Intelligenz auf das Model-Checking von Realzeitautomaten. In der KI haben sich Heuristiken als sehr nützlich für die Suche erwiesen. Im Model-Checking können ähnliche Methoden angewendet werden, um Heuristiken zu entwickeln, die die Suche nach geeignet spezifizierten Fehlerzuständen eines Realzeitautomaten beschleunigen können.
- Fehlersuche in hybriden Systemen. Das Ziel dieser Forschungsrichtung ist, trotz gewisser technischer Unterschiede, das selbe wie für Realzeitautomaten: das Finden von Fehlertrajektorien. Zu diesem Zwecke verwende ich Simulationen, die von Abstraktionen geleitet werden, die ursprünglich für die Verifikation entwickelt worden waren.
- Lineare pseudo-Boolesche Constraints. Ein linearer pseudo-Boolescher Constraint (LPB) ist eine Verallgemeinerung einer aussagenlogischen Klausel. Ich interessiere mich dafür, die Ausdrucksmächtigkeit von LPBs genau zu analysieren. Unter anderem habe ich einen kombinatorischen Algorithmus entwickelt, der eine aussagenlogische Formel in einen LPB transformiert, sofern dies möglich ist; ein mehr als 30 Jahre lang offenes Problem.
Bis zum Jahre 2004 lagen meine Interessen hauptsächlich in der Logikprogrammierung.
- Verifikation von Logikprogrammen mit dynamischer Selektion. In der Logikprogrammierung bezeichnet dynamische Selektion die Situation, dass in jedem Berechnungsschritt ein Atom aufgrund von Kriterien selektiert wird, die mit der Instanziierung dieses Atoms zusammenhängen, anstatt immer das am weitesten links stehende Atom einer Anfrage zu selektieren. Ich habe Methoden entwickelt, um in diesem Kontext die Terminierung und andere Korrektheitseigenschaften zu gewährleisten und zu beweisen. Insbesondere habe ich den Begriff der inputkonsumierenden Ableitungen (input-consuming derivations) eingeführt, der abstrakter und einer theoretischen Analyse zugänglicher ist als die Konstrukte, die in konkreten Programmiersprachen existieren. Ich habe außerdem Übersichtsartikel über den Zusammenhang von Terminierung und der Selektionsregel geschrieben.
- Getypte Programmiersprachen. Ich habe zu getypten logischen Programmiersprachen wie Gödel oder Mercury gearbeitet. Insbesondere habe ich die subject-reduction studiert, d.h. die Eigenschaft, dass während der Berechnung eines Programmes nur wohlgetypte Anfragen vorkommen können. Ich habe betrachtet, wie man diese Eigenschaft als Eigenschaft der beweistheoretischen Semantik eines Programms auffassen kann, und wie man sie bei Systemen mit Subtypen gewährleisten kann. In einer anderen Arbeit habe ich die so genannte polymorphe Rekursion für die funktionale und die Logikprogrammierung untersucht.
- Mode-Analyse für getypte Logikprogramme. Ich habe Methoden entwickelt, um basierend auf den Typen eines Programms die Instanziierung von Variablen zu charakterisieren (Mode-Analyse). Insbesondere kann man den Verlauf der Instanziierung beim Ablauf eines Programms analysieren, indem man das Programm auf einem eigens entwickelten abstrakten Datenbereich ablaufen lässt und die gewöhnliche Unifikation durch ACI-Unifikation ersetzt.