Guarded Successor: A Novel Temporal Logic

TL;DR

This paper introduces GS, a decidable temporal logic capable of handling infinite data values with rich theories, distinguishing inputs and outputs, and enabling complex reasoning crucial for safe AI development.

Contribution

It presents GS, a novel temporal logic with unique features like rich data theories and self-referential data values, advancing formal methods for AI safety.

Findings

GS is decidable and supports rich data theories.

The logic distinguishes inputs and outputs for precise modeling.

A non-temporal fragment NSO is also introduced.

Abstract

We present GS (Guarded Successor), a novel decidable temporal logic with several unique distinctive features. Among those, it allows infinitely many data values that come not only with equality but with a somehow rich theory too: the first-order theory of atomless Boolean algebras. The language also distinguishes between inputs and outputs, and has a decision procedure for determining whether for all inputs exist outputs, at each point of time. Moreover, and maybe most surprisingly, the data values can be nothing but sentences in GS itself. We also present a non-temporal fragment called NSO (Nullary Second Order) that enjoys merely this last property. These results are crucial necessary ingredients in any meaningful design of safe AI. Finally, all those results are obtained from a novel treatment of the first-order theory of atomless Boolean algebras.