Modelltheorie temporallogischer Spezifikationen

(Durchführung teilweise im Rahmen des Graduiertenkollegs Sprache, Information und Logik)

Ziel dieses Projekts ist die Untersuchung grundlegender modelltheoretischer Fragen, die durch temporallogische Spezifikationen aufgeworfen werden. Dabei geht es einerseits darum, Definitionen und Konzepte der klassischen Modelltheorie wie Substrukturen, p-Morphismen und Ultrafilter und -produkte für modale Logiken auf temporale Logiken zu übertragen und damit etwa Vollständigkeitsaussagen oder Löwenheim-Skolem-Theoreme abzuleiten. Andererseits werfen spezifisch informatik-orientierte Konzepte wie Stotterinvarianz oder alternative Semantikdefinitionen, bei denen etwa eine Folge statt einer Menge von Welten zu Grunde gelegt werden, interessante Fragen etwa bezüglich der Modellvielfalt und ausgezeichneter Modelle auf.

Ansprechpartner: Dr. Stephan Merz

Arbeiten und Veröffentlichungen:

A.Kurz: Sequence Frames. Proc. Verif. in New Orientation, Univ. Maribor, 1995.

Liste aller Projekte

Institut

Universität