ocLTL: LTL Realizability and Synthesis Modulo {\omega}-Categorical Structures

TL;DR

This paper introduces ocLTL, a logic framework for LTL+P over {}-categorical structures, reducing realizability and synthesis problems to propositional LTL+P with manageable complexity.

Contribution

It presents a reduction technique for LTL+P modulo -categorical theories, enabling complexity bounds and applications to algebraic structures and AI safety.

Findings

Complexity remains 2-EXPTIME after reduction.

Finite disjunction over complete types replaces data subformulas.

Application to atomless Boolean algebras and Lindenbaum-Tarski algebras.

Abstract

We introduce ocLTL, the case of LTL+P modulo {\omega}-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.