Temporal logics with incommensurable distances are undecidable (Q879597)

The paper under review shows the undecidability of linear temporal logic with ``since'' and ``until'' extended by the two modalities ``\(X\) will happen within one unit of time'' and ``\(X\) will happen within \(\tau\) unit of time'' where \(\tau\) is irrational. The result can be straightforwardly generalized to the case when 1 and \(\tau\) are replaced by numbers \(c\) and \(d\) such that \(c/d\) is irrational. The undecidability proof is obtained by a reduction of the reachability problem for two-counter machines. Such a machine \(M\) consists of a finite set of states and two unbounded non-negative integer variables called counters. Three types of instructions are used in \(M\): branching based on whether a specific counter has the value 0, incrementing and decrementing of a counter. It is well known that for such machines it is undecidable whether a given state is reachable from the initial state. In the main part of the paper, the author provides a detailed account of how to ``encode'' computations of \(M\) in the temporal logic under consideration, which yields the desired result.