Effective Denotational Semantics for Synthesis
Software Engineering and Programming Languages
Final Report Abstract
We studied denotational semantics for solving synthesis problems. A focus was on the support of imperfect information and infinite state spaces. The following are the main results along the project plan. We developed denotational semantics for solving synthesis problems over multi-pushdown systems. The complexity had been open for a while and we settled it. We studied verification and synthesis problems over programs operating on graph monoids. We obtained complete classifications (along the monoid) of the complexity for verification and the decidability for synthesis. We developed urgency programs where the alternating choices are annotated by urgencies indicating when a choice is due (under submission). We demonstrated the usefulness in case studies and settled the complexity for synthesis. Interestingly, the denotational semantics for synthesis turned out to be a derived concept: it was induced by an axiomatization of the contextual equivalence of the language. We showed that for (collapsible) pushdown systems parity games can be reduced to safety games in polynomial time. We adapted the project to study regular separability: given languages L, K ⊆ Σ∗ , is there a regular language R ⊆ Σ∗ with L ⊆ R and R ∩ K = ∅? Regular separability naturally comes up when thinking about alternation and imperfect information. Another reason it became important to us was the following suprisingly general result that we obtained: the languages of two well-structured transition systems (WSTS) are disjoint if and only if there is a regular separator. The result assumes one of the WSTS to be deterministic. We then showed that almost all WSTS (finitely-branching WSTS and WSTS over ω2 -WQOs) can be determinized. The results left open whether regular separability holds in general, and what is the impact of determinism on WSTS. We also managed to solve these problems. We came up with a WSTS language that provably cannot be accepted by a deterministic WSTS. Still, we managed to generalize the regular separability result to all WSTS. The proof introduces the concept of converging transition systems, which may be of independent interest. We also studied an infinite-word variant of the problem. Already for Petri nets, the above separability is lost: there are disjoint ω-coverability languages that do not admit an ω-regular separator. We studied the problem of checking whether a regular separator exists, showed decidability, and settled the complexity in the one-dimensional case. We added a work package on flow graphs, a recent model of separation logic that is gaining popularity but still had weaknesses. We improved the model, and our understanding of contextual equivalence was instrumental in doing so. To demonstrate the usefulness of the new model, we built a proof checker for flow-based correctness proofs of concurrent data structures.
Publications
-
Bounded Context Switching for Valence Systems. In CONCUR, 12:1–12:18, 2018.
R. Meyer; S. Muskalla & G. Zetzsche
-
Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems. In MFCS, 57:1–57:15, 2018.
M. Hague; R. Meyer; S. Muskalla & M. Zimmermann
-
Regular Separability of Well-Structured Transition Systems. In CONCUR, 35:1–35:18, 2018.
W. Czerwinski; S. Lasota; R. Meyer; S. Muskalla; K. Narayan Kumar & P. Saivasan
-
On the Complexity of Multi-Pushdown Games. In FSTTCS, 52:1–52:35, 2020.
R. Meyer & S. van der Wall.
-
Make Flows Small Again: Revisiting the Flow Framework. Lecture Notes in Computer Science, 628-646. Springer Nature Switzerland.
Meyer, Roland; Wies, Thomas & Wolff, Sebastian
-
nekton: A Linearizability Proof Checker. Lecture Notes in Computer Science, 170-183. Springer Nature Switzerland.
Meyer, Roland; Opaterny, Anton; Wies, Thomas & Wolff, Sebastian
-
Regular Separability in Büchi VASS. In STACS, 9:1–9:19, 2023.
P. Baumann; R. Meyer & G. Zetzsche
-
Separability and Non-Determinizatbility in WSTS. In CONCUR, 8:1–9:17, 2023.
E. Keskin & R. Meyer
