Crossing the Undecidability Border with Extensions of Propositional Neighborhood Logic over Natural Numbers

Dario Della Monica, Valentin Goranko, Angelo Montanari, Guido Sciavicco

    Research output: Contribution to journalJournal articleResearchpeer-review

    192 Downloads (Pure)

    Abstract

    Propositional Neighborhood Logic (PNL) is an interval temporal logic featuring two modalities corresponding to the relations of right and left neighborhood between two intervals on a linear order (in terms of Allen's relations, meets/ and met by). Recently, it has been shown that PNL interpreted over several classes of linear orders, including natural numbers, is decidable (NEXPTIME-complete) and that some of its natural extensions preserve decidability. Most notably, this is the case with PNL over natural numbers extended with a limited form of metric constraints and with the future fragment of PNL extended with modal operators corresponding to Allen's relations begins, begun by, and before/. This paper aims at demonstrating that PNL and its metric version MPNL, interpreted over natural numbers, are indeed very close to the border with undecidability, and even relatively weak extensions of them become undecidable. In particular, we show that (i) the addition of binders on integer variables ranging over interval lengths makes the resulting hybrid extension of MPNL undecidable, and (ii) a very weak first-order extension of the future fragment of PNL, obtained by replacing proposition letters by a restricted subclass of first-order formulae where only one variable is allowed, is undecidable (in contrast with the decidability of similar first-order extensions of point-based temporal logics).
    Original languageEnglish
    JournalJournal of Universal Computer Science
    Volume18
    Issue number20
    Pages (from-to)2798-2831
    ISSN0948-695X
    Publication statusPublished - 2012

    Keywords

    • Interval neighborhood logics
    • Undecidability
    • Hybrid logics
    • Interval length binders
    • First-order logic

    Fingerprint

    Dive into the research topics of 'Crossing the Undecidability Border with Extensions of Propositional Neighborhood Logic over Natural Numbers'. Together they form a unique fingerprint.

    Cite this