William H English

Author directory

2026

Natural language (NL) to temporal logic (TL) translation lets engineers specify and verify system behaviors without hand-crafting formal specifications. Existing frameworks lift NL into syntactically valid TL but leave atomic propositions abstract—not grounded to the concrete predicates and typed objects a system exposes (e.g., binding “find the bookbag” to search(backpack)). Ungrounded formulas cannot be checked over traces, yet current systems either omit grounding or ground inaccurately. We propose , a modular stage for Grounding Natural Language Into System Signatures that attaches to any NL-to-TL lifter. We cast grounding as signature-conditioned classification: enumerating the signature as an input prefix lets one encoder-only model assign each abstract AP a predicate and its typed arguments, generalize to unseen signature elements, and transfer across domains without retraining, while never hallucinating out-of-signature atoms. Because predictions are selections from the enumerated signature, the out-of-signature rate is 0% by construction, against up to 95% for prompted LLMs given the same signature in-context. attains at least 99% joint grounding accuracy across seven domains (worst case 99.39 ± 0.04 over five seeds); paired with a lifter, it produces executable specifications that track the oracle-grounding upper bound, improving grounded logical equivalence by 75% over the strongest prompted-LLM and embedding-similarity grounder.