Temporal logics with incommensurable distances are undecidable (Q879597)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Temporal logics with incommensurable distances are undecidable
scientific article

    Statements

    Temporal logics with incommensurable distances are undecidable (English)
    0 references
    14 May 2007
    0 references
    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.
    0 references
    0 references
    temporal logic
    0 references
    metric properties
    0 references
    undecidability
    0 references

    Identifiers