Servicenavigation

Detailseite

Zurück

Projekt Druckansicht

Effektive Denotationelle Semantik für die Synthese

Fachliche Zuordnung Theoretische Informatik
Softwaretechnik und Programmiersprachen
Förderung Förderung von 2018 bis 2023
Projektkennung Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 417532197
 
Erstellungsjahr 2023

Zusammenfassung der Projektergebnisse

Das Projekt war der Studie denotationeller Semantiken zur Lösung von Syntheseproblemen gewidmet. Unterstützt werden sollten insbesondere Modelle mit imperfekter Information und unendlichen Zustandsräumen. Entlang des Projektplans erzielten wir folgende Ergebnisse. Wir entwickelten denotationelle Semantiken zur Lösung von Syntheseproblemen über Multi-Pushdown-Systemen. Die Komplexität war längere Zeit offen und wir konnten sie mit unserem Ansatz lösen. Wir studierten Verifikations- und Syntheseprobleme für Programme, die auf Graph-Monoiden operieren, und erzielten vollständige Charakterisierungen (entlang des Monoids) der Komplexität für die Verifikation bzw. der Entscheidbarkeit für die Synthese. Wir entwickelten das Modell der Urgency-Programme, in dem alternierende Choice-Operatoren mit Urgencies annotiert sind, die angeben, wann eine Choice zu treffen ist (unter Begutachtung). Wir demonstrierten die Nützlichkeit des Modells in Fallstudien und lösten das Syntheseproblem. Interessanterweise erwies sich die denotationelle Semantik für die Synthese als abgeleitetes Konzept, das aus einer Axiomatisierung der kontextuellen Äquivalenz gewonnen werden konnte. Wir zeigten, dass sich für (Collapsible) Pushdown-Systeme Parity-Games in polynomieller Zeit auf Safety-Games reduzieren lassen. Wir haben das Projekt auf die Studie regulärer Separierbarkeit angepasst: gegeben seien Sprachen L, K ⊆ Σ∗ , gibt es eine reguläre Sprache R ⊆ Σ∗ mit L ⊆ R und R ∩ K = ∅? Reguläre Separierbarkeit ist ein natürliches Problem im Kontext von Alternierung und imperfekter Information. Außerdem wurde das Problem für uns wichtig, da wir ein überraschend allgemeines Resultat erzielen konnten (CONCUR’18): die Sprachen zweier wohlstrukturierter Transitionssysteme (WSTS) sind disjunkt gdw. sie regulär separierbar sind. Das Resultat nimmt eines der WSTS als deterministisch an. Wir konnten zeigen, dass sich fast alle WSTS (finitely-branching WSTS und WSTS über ω2 -WQOs) determinisieren lassen. Die allgemeinen Fragen nach Separierbarkeit und Determinisierbarkeit konnten wir erst zu einem späteren Zeitpunkt lösen. Wir gaben eine WSTS Sprache an, die nachweislich nicht von einem deterministischen WSTS akzeptiert werden kann. Dennoch gelang es uns, das reguläre Separierbarkeitsresultat auf alle WSTS zu verallgemeinern. Wir studierten das Problem außerdem für unendliche Worte. Wir fügten dem Projekt ein Arbeitspaket über Flowgraphen hinzu, einem neuen Modell der Separation-Logik, das hohes Interesse geweckt hatte aber noch Schwachstellen besaß. Zu unserer Überraschung war es unser Verständnis kontextueller Äquivalenz, das es uns erlaubte, die Flowgraph-Theorie zu verbessern. Um die Nützlichkeit des neuen Modells unter Beweis zu stellen, entwickelten wir einen Proof-Checker für Flow-basierte Korrektheitsbeweise nebenläufiger Datenstrukturen.

Projektbezogene Publikationen (Auswahl)

 
 

Zusatzinformationen

© 2025 DFG Kontakt / Impressum / Datenschutz

Textvergrößerung und Kontrastanpassung