JUCS - Journal of Universal Computer Science 18(20): 2798-2831, doi: 10.3217/jucs-018-20-2798
Crossing the Undecidability Border with Extensions of Propositional Neighborhood Logic over Natural Numbers
expand article infoDario Della Monica, Valentin Goranko§, Angelo Montanari|, Guido Sciavicco
‡ Reykjavik University, Reykjavik, Iceland§ Technical Institute of Denmark, Copenhagen, Denmark| University of Udine, Udine, Italy¶ University of Murcia, Murcia, Spain
Open Access
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).
interval neighborhood logics, undecidability, hybrid logics, interval length binders, first-order logic