ocLTL: LTL Realizability and Synthesis Modulo ω-Categorical Structures
This work extends LTL realizability and synthesis to a broader class of data-aware specifications for formal verification.
The paper introduces ocLTL, a version of LTL+P modulo ω-categorical theories, and reduces its realizability and synthesis problems to propositional LTL+P, showing that complexity remains 2-EXPTIME with a theory-dependent but formula-independent blowup.
We introduce ocLTL, a version 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 additional blowup that depends only on the theory but not the formula.