sweap: Reactive Synthesis for Infinite-State Integer Problems
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866911674128138240 |
|---|---|
| author | Azzopardi, Shaun Di Stefano, Luca Piterman, Nir |
| author_facet | Azzopardi, Shaun Di Stefano, Luca Piterman, Nir |
| contents | Recent years have seen a significant increase in the interest in reactive synthesis from specifications that relate to infinite state spaces. We present sweap, a tool for synthesis of infinite-state Linear Integer Arithmetic reactive systems. sweap implements a CEGAR approach, relying on state-of-the-art finite-state synthesis tools as black boxes to solve abstract synthesis problems. sweap supports most common input formalisms for infinite-state reactive-synthesis problems: Temporal Stream Logic Modulo Theories, Reactive Program Games, the bespoke input of the ISSY tool, and our own bespoke input. We present a mature version of sweap with novel features: a dual abstraction approach that improves its capabilities in proving unrealisability, support for nondeterministic and unbounded updates, more general initialization of variables, and equirealisable reductions for optimisation. Experimental evaluation shows that sweap outperforms its only competitor in this domain. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_11992 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | sweap: Reactive Synthesis for Infinite-State Integer Problems Azzopardi, Shaun Di Stefano, Luca Piterman, Nir Logic in Computer Science Formal Languages and Automata Theory Systems and Control Recent years have seen a significant increase in the interest in reactive synthesis from specifications that relate to infinite state spaces. We present sweap, a tool for synthesis of infinite-state Linear Integer Arithmetic reactive systems. sweap implements a CEGAR approach, relying on state-of-the-art finite-state synthesis tools as black boxes to solve abstract synthesis problems. sweap supports most common input formalisms for infinite-state reactive-synthesis problems: Temporal Stream Logic Modulo Theories, Reactive Program Games, the bespoke input of the ISSY tool, and our own bespoke input. We present a mature version of sweap with novel features: a dual abstraction approach that improves its capabilities in proving unrealisability, support for nondeterministic and unbounded updates, more general initialization of variables, and equirealisable reductions for optimisation. Experimental evaluation shows that sweap outperforms its only competitor in this domain. |
| title | sweap: Reactive Synthesis for Infinite-State Integer Problems |
| topic | Logic in Computer Science Formal Languages and Automata Theory Systems and Control |
| url | https://arxiv.org/abs/2605.11992 |