Logikfragmente für unendliche und partiell-kommutative Objekte

• Antragsteller: Professor Dr. Volker Diekert
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2010 bis 2020
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 166222852

In dem Projekt sollen neue Entscheidbarkeitsresultate für Fragmenteder Prädikatenlogik erster Stufe erzielt werden. Als Modelle wollen wir sowohl endliche und unendliche Wörter als auch für Mazurkiewicz-Spuren untersuchen. Dies ist von daher interessant, da man mit diesen partiell-kommutativen Strukturennebenläufige Systeme modellieren kann. Das Vorhaben behandelt Grundlagenfragen. Die Motivation zu diesen Fragestellungen er gibt sich jedoch aus den praktischen Überlegungen zur Validierung vonSoftware und Schaltkreisen. Hier sind logische Fragmente vor allem aus zwei Gründen interessant. Zum einen erlauben sie eine Beurteilung der Schwierigkeit von Eigenschaften und zum anderen sind für einfache Fragmente oft effizientere Verfahren (etwa für das Model-Checking-Problem) bekannt. Intuitiv ist eine Eigenschaft schwieriger, wenn sie nur in einem ausdrucksstärkeren Fragmentformulierbar ist, und entsprechend können beispielsweise für die formale Verifikation einer solchen Eigenschaft aufwendigere Verfahren notwendig sein. Die neuen von uns verwendeten Methoden sind algebraisch, topologisch und kombinatorisch.

• DFG-Verfahren: Sachbeihilfen