First order synthesis for data words revisited
Julien Grange, Mathieu Lehaut
TL;DR
This paper investigates the synthesis problem for data words within fragments of first-order logic, clarifying the exact boundaries between decidability and undecidability in this domain.
Contribution
It provides a precise characterization of the decidability frontier for the synthesis problem on data words in first-order logic fragments.
Findings
Identifies the exact boundary between decidability and undecidability.
Clarifies the limits of algorithmic synthesis for data words.
Advances understanding of logical fragments in data word synthesis.
Abstract
We carry on the study of the synthesis problem on data words for fragments of first order logic, and delineate precisely the border between decidability and undecidability.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Software Testing and Debugging Techniques