Multi-Property 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_ | 1866912826522599424 |
|---|---|
| author | Weinhuber, Christoph Schnitzer, Yannik Abate, Alessandro Parker, David De Giacomo, Giuseppe Vardi, Moshe Y. |
| author_facet | Weinhuber, Christoph Schnitzer, Yannik Abate, Alessandro Parker, David De Giacomo, Giuseppe Vardi, Moshe Y. |
| contents | We study LTLf synthesis with multiple properties, where satisfying all properties may be impossible. Instead of enumerating subsets of properties, we compute in one fixed-point computation the relation between product-game states and the goal sets that are realizable from them, and we synthesize strategies achieving maximal realizable sets. We develop a fully symbolic algorithm that introduces Boolean goal variables and exploits monotonicity to represent exponentially many goal combinations compactly. Our approach substantially outperforms enumeration-based baselines, with speedups of up to two orders of magnitude. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_10651 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Multi-Property Synthesis Weinhuber, Christoph Schnitzer, Yannik Abate, Alessandro Parker, David De Giacomo, Giuseppe Vardi, Moshe Y. Artificial Intelligence Logic in Computer Science We study LTLf synthesis with multiple properties, where satisfying all properties may be impossible. Instead of enumerating subsets of properties, we compute in one fixed-point computation the relation between product-game states and the goal sets that are realizable from them, and we synthesize strategies achieving maximal realizable sets. We develop a fully symbolic algorithm that introduces Boolean goal variables and exploits monotonicity to represent exponentially many goal combinations compactly. Our approach substantially outperforms enumeration-based baselines, with speedups of up to two orders of magnitude. |
| title | Multi-Property Synthesis |
| topic | Artificial Intelligence Logic in Computer Science |
| url | https://arxiv.org/abs/2601.10651 |