ocLTL: LTL Realizability and Synthesis Modulo ω-Categorical Structures
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911690173448192 |
|---|---|
| author | Asor, Ohad |
| author_facet | Asor, Ohad |
| contents | We introduce ocLTL, the case of LTL+P modulo ω-categorical theories. We reduce its realizability and synthesis problems into the corresponding problems in propositional LTL+P. The core of the reduction replaces each data subformula with a finite disjunction over complete types. The complexity remains 2-EXPTIME with an additional blowup that depends only on the theory but not the formula. We demonstrate an application of this framework that is related to atomless Boolean algebras and Lindenbaum-Tarski algebras while drawing a connection to AI safety. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_12539 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | ocLTL: LTL Realizability and Synthesis Modulo ω-Categorical Structures Asor, Ohad Logic in Computer Science We introduce ocLTL, the case of LTL+P modulo ω-categorical theories. We reduce its realizability and synthesis problems into the corresponding problems in propositional LTL+P. The core of the reduction replaces each data subformula with a finite disjunction over complete types. The complexity remains 2-EXPTIME with an additional blowup that depends only on the theory but not the formula. We demonstrate an application of this framework that is related to atomless Boolean algebras and Lindenbaum-Tarski algebras while drawing a connection to AI safety. |
| title | ocLTL: LTL Realizability and Synthesis Modulo ω-Categorical Structures |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2605.12539 |