Fast Obligation Translation and Synthesis
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910213140905984 |
|---|---|
| author | Duret-Lutz, Alexandre De Giacomo, Giuseppe Jurdzinski, Marcin Piterman, Nir Vardi, Moshe Y. Zhu, Shufang |
| author_facet | Duret-Lutz, Alexandre De Giacomo, Giuseppe Jurdzinski, Marcin Piterman, Nir Vardi, Moshe Y. Zhu, Shufang |
| contents | Syntactic obligations are a fragment of LTL formulas that translate to deterministic weak $ω$-automata (DWA). We show that syntactic obligations can be very efficiently converted to minimal DWA represented using multi-terminal binary decision diagrams (MTBDDs), and that synthesis of such specifications can be solved directly on the MTBDD representation on the fly. Our implementation in Spot shows substantial runtime improvements in translation and synthesis. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_12372 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Fast Obligation Translation and Synthesis Duret-Lutz, Alexandre De Giacomo, Giuseppe Jurdzinski, Marcin Piterman, Nir Vardi, Moshe Y. Zhu, Shufang Formal Languages and Automata Theory Logic in Computer Science Syntactic obligations are a fragment of LTL formulas that translate to deterministic weak $ω$-automata (DWA). We show that syntactic obligations can be very efficiently converted to minimal DWA represented using multi-terminal binary decision diagrams (MTBDDs), and that synthesis of such specifications can be solved directly on the MTBDD representation on the fly. Our implementation in Spot shows substantial runtime improvements in translation and synthesis. |
| title | Fast Obligation Translation and Synthesis |
| topic | Formal Languages and Automata Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2605.12372 |