Guarded Successor: A Novel Temporal Logic
TL;DR — A decidable temporal logic proposed for specifying and verifying systems, from the Tau Net project.
⬇ Download the archived copy — kept here so the document survives its source going dark. arXiv preprint (author distribution licence).
arXiv:2407.06214v1 [cs.LO], 4 July 2024, from IDNI AG.
Asor presents GS (Guarded Successor), a decidable temporal logic — decidability being the property that matters, since it is what allows a machine to check a specification rather than merely state one.
The context is the Tau Net project’s aim of executable, verifiable specifications. A narrow technical paper whose interest is the ambition behind it: software whose behaviour is proven against a declared spec rather than tested.
Where this came from
15 pages. A copy is archived locally against link rot; the header links the original source.