2026-10-05T22:55:33Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:25432 2026-03-19T12:28:26Z ddc:004 open_access

Register-Bounded Synthesis from Constraint LTL Dauvier, Nino Filiot, Emmanuel Reynier, Pierre-Alain Synthesis Data words Constraint linear time logic Register transducer We consider synthesis problems from logical specifications over infinite data domains, expressed in the logic constraint LTL (CLTL), which extends LTL with predicates over an infinite set of data values. We consider register-bounded synthesis, where the goal is to automatically generate, if it exists, a transducer with r registers that realizes a given CLTL formula, where r is also given as input. We prove that CLTL register-bounded synthesis is 2ExpTime-c for various data domains such as any infinite set with equality, (ℚ, <), and (ℕ, <). For the latter domain, this contrasts with known undecidability results of (unbounded) register CLTL synthesis, by Bhaskar and Praveen. Lastly, we consider synthesis in a partial observation setting by extending CLTL with invisible variables. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Nino Dauvier and Emmanuel Filiot and Pierre-Alain Reynier 2026 Is Part Of LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2026.8 urn:nbn:de:0030-drops-254322 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.8 eng https://creativecommons.org/licenses/by/4.0/legalcode