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.

翻译：本文提出ocLTL，即LTL+P在ω-范畴理论下的情形。我们将其可实现性与综合问题归约为命题LTL+P中的对应问题。该归约的核心是用完全类型的有限析取替换每个数据子公式。其复杂度仍为2-EXPTIME，且额外的指数增长仅取决于理论本身而非公式。我们展示了该框架的一个应用，该应用与无原子布尔代数及林登鲍姆-塔尔斯基代数相关，同时建立了与人工智能安全性的联系。