Pith Number

pith:V7CJRSUD

pith:2026:V7CJRSUDIU3KH2MKW6MJ42TJYS

not attested not anchored not stored refs resolved

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

Ohad Asor

ocLTL realizability and synthesis reduce to propositional LTL+P by replacing each data subformula with a finite disjunction over complete types.

arxiv:2605.12539 v1 · 2026-05-05 · cs.LO

Open paper page JSON Open Graph Bundle Merged state Verified badge What is a Pith Number?

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{V7CJRSUDIU3KH2MKW6MJ42TJYS}

Prints a linked badge after your title and injects PDF metadata. Compiles on arXiv. Learn more · Embed verified badge

Record completeness

1 Bitcoin timestamp

2 Internet Archive

3 Author claim open · sign in to claim

4 Citations open

5 Replications open

✓ Portable graph bundle live · download bundle · merged state

The bundle contains the canonical record plus signed events. A mirror can host it anywhere and recompute the same current state with the deterministic merge algorithm.

Claims

C1strongest claim

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.

C2weakest assumption

The assumption that for the given ω-categorical theory, there are only finitely many complete types, allowing the disjunction to be finite, and that this replacement correctly captures the semantics of the data subformulas in the context of the temporal logic.

C3one line summary

ocLTL reduces realizability and synthesis for LTL over ω-categorical structures to propositional LTL+P while preserving 2-EXPTIME complexity with theory-dependent blowup.

References

17 extracted · 17 resolved · 0 Pith anchors

[1] Full LTL synthesis overinfinite-statearenas 2024

[2] Ashwin Bhaskar and M. Praveen. Realizability problem for constraint LTL. In29th Inter- national Symposium on Temporal Representation and Reasoning (TIME 2022), volume 247 of LIPIcs, pages 8:1–8:19. Sc 2022

[3] Two- variable logic on data words.ACM Transactions on Computational Logic, 12(4):27:1–27:26,

[4] Conference version: LICS 2006. 8 2006

[5] Automata theory in nominal sets 2014

Formal links

2 machine-checked theorem links

Receipt and verification

First computed	2026-05-18T03:10:02.372114Z
Builder	pith-number-builder-2026-05-17-v1
Signature	Pith Ed25519 (`pith-v1-2026-05`) · public key
Schema	pith-number/v1.0

Canonical hash

afc498ca834536a3e98ab7989e6a69c4b36ce3c2e89c8c1d9d108eb2d714be29

Aliases

arxiv: 2605.12539 · arxiv_version: 2605.12539v1 · doi: 10.48550/arxiv.2605.12539 · pith_short_12: V7CJRSUDIU3K · pith_short_16: V7CJRSUDIU3KH2MK · pith_short_8: V7CJRSUD

Agent API

Resolver JSON Graph JSON Events JSON Schema Signing key

Verify this Pith Number yourself

curl -sH 'Accept: application/ld+json' https://pith.science/pith/V7CJRSUDIU3KH2MKW6MJ42TJYS \
  | jq -c '.canonical_record' \
  | python3 -c "import sys,json,hashlib; b=json.dumps(json.loads(sys.stdin.read()), sort_keys=True, separators=(',',':'), ensure_ascii=False).encode(); print(hashlib.sha256(b).hexdigest())"
# expect: afc498ca834536a3e98ab7989e6a69c4b36ce3c2e89c8c1d9d108eb2d714be29

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "2762366ea4c53de8e1f514c91399821d6cb2f29584cb139b362c13c3e31b5888",
    "cross_cats_sorted": [],
    "license": "http://creativecommons.org/licenses/by-nc-nd/4.0/",
    "primary_cat": "cs.LO",
    "submitted_at": "2026-05-05T14:00:15Z",
    "title_canon_sha256": "f2da74a5c2ee121e6b1b58ef10cb3d91b51bed56e3763754861b86498c4f43eb"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2605.12539",
    "kind": "arxiv",
    "version": 1
  }
}