Prompt Interval Temporal Logic

Abstract

Interval temporal logics are expressive formalisms for temporal representation and reasoning, which use time intervals as primitive temporal entities. They have been extensively studied for the past two decades and successfully applied in AI and computer science. Unfortunately, they lack the ability of expressing promptness conditions, as it happens with the commonly-used temporal logics, e.g., LTL: whenever we deal with a liveness request, such as “something good eventually happens”, there is no way to impose a bound on the delay with which it is fulfilled. In the last years, such an issue has been addressed in automata theory, game theory, and temporal logic. In this paper, we approach it in the interval temporal logic setting. First, we introduce PROMPT- PNL, a prompt extension of the well-studied interval temporal logic PNL, and we prove the undecidability of its satisfiability problem; then, we show how to recover decidability (NEXPTIME-completeness) by imposing a natural syntactic restriction on it.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Interval temporal logics provide a powerful framework suitable for reasoning about time. Unlike classic temporal logics, such as Linear Temporal Logic (LTL) [21] and the like, they use time intervals, instead of time points, as primitive temporal entities. Such a distinctive feature turns out to be very useful in various Computer Science and AI application domains, ranging from hardware and real-time system verification to natural language processing, from constraint satisfaction to planning [1, 2, 10, 20, 22, 23]. As concrete applications, we mention TERENCE [14], an adaptive learning system for poor comprehenders and their educators (based on Allen’s interval algebra IA [1]), and RISMA [17], an algorithm to analyze behavior and performance of real-time data systems (based on Halpern and Shoham’s modal logic of Allen’s relations HS  [15]).

A fundamental class of properties that can be expressed in (both interval- and point-based) temporal logics is that of liveness properties, which allow one to state that something “good” will eventually happen. However, a limitation that is common to most temporal logics is the lack of support for promptness: it is not possible to bound the delay with which a liveness request is fulfilled, despite the fact that this is desirable for many practical applications (see [16] for a convincing argument). To overcome such a shortcoming, a whole body of work has been recently devoted to the study of promptness. In [4, 16], the authors extend LTL with the ability of bounding the delay with which a temporal request is satisfied. In [3], the use of prompt accepting conditions in the context of $\omega$-regular automata is explored by introducing prompt-Büchi automata, whose accepting condition imposes the existence of a bound on the number of non-accepting states in between two consecutive occurrences of accepting ones. Prompt extensions of LTL have also been investigated outside the realm of closed systems. Two-player turn-based games with perfect information have been explored in the prompt LTL setting in [24]. In [9], the authors lift the prompt semantics to $\omega$-regular games, under the parity winning condition, by introducing finitary parity games. They make use of the concept of distance between positions in a play that refers to the number of edges traversed in the game arena; the classical parity winning condition is then reformulated to take into consideration only those states occurring with a bounded distance. Such an idea has been generalised to deal with more involved prompt parity conditions [13, 19]. In the field of formal languages, promptness comes into play in [6], where $\omega$B-regular languages and their automata counterpart, known as $\omega$B-automata, are studied. Intuitively, $\omega$B-regular languages extend $\omega$-regular ones with the ability of bounding the distance between occurrences of sub-expressions in consecutive $\omega$-iterations, within each word of the language. Finally, an extension of alternating-time epistemic temporal logic with prompt-eventuality has been recently investigated in [5].

In this paper, we show that interval temporal logics can be successfully provided with a support for prompt-liveness specifications by lifting the work done in [4, 16] to the interval-based setting.

In [4], the language of LTL is enriched with parameterized versions of temporal modalities F (eventually) and U (until), as well as of the dual modalities G (globally) and R (release). The resulting logic, called PLTL, features the following parameterized modalities: $F_{\le x}$, $F_{> y}$, $G_{\le y}$, $G_{> x}$, $U_{\le x}$, $U_{> y}$, $R_{\le y}$, and $R_{> x}$, where $x \in X$, $y \in Y$, and X and Y are two disjoint sets of bounding variables. Intuitively, a formula $F_{\le x} \phi$ is true if $\phi$ is satisfied within x time units, according to the valuation of x (the other parameterized modalities have an analogous interpretation). Thus, PLTL models are LTL models, i.e., words over the powerset of the set of atomic propositions, enriched with a valuation for the bounding variables in $X \cup Y$. The satisfiability problem for PLTL is PSPACE-complete, as for LTL. The assumption that X and Y are disjoint is crucial in retaining decidability. In [16], the authors introduce the logic PROMPT- LTL, which restricts PLTL in three ways: (i) a parameterized version is introduced for the modality F only (parameterized versions of modalities G, U, and R are not included); (ii) only upper bounds appear in parameterized modalities, i.e., no subscript of the form $_{>x}$ occurs; (iii) there is only one bounding variable. The restriction imposed by PROMPT- LTL is less strong than it looks like: as shown in [4], operator $F_{\le x}$, along with the classic LTL constructs, is enough to define operators $G_{> x}$, $U_{\le x}$, $R_{> x}$ (i.e., all the operators involving in their subscript variables in X). As PROMPT- LTL enriches LTL with the ability of limiting the amount of time a fulfillment of an existential request (corresponding to a liveness property) can be delayed, it can be thought of as an extension of LTL with prompt liveness. In [16], it is shown that reasoning about PROMPT- LTL is not harder than reasoning about LTL, with respect to a series of basic problems, including satisfiability (PSPACE-complete).

In the present paper, we show how to extend the logic PNL of temporal neighborhood (a well-known fragment of HS whose satisfiability problem is NEXPTIME-complete [8]), with the ability of expressing prompt-liveness properties. Following the approach of [16], we introduce ‘prompt’ versions (i.e., upper bounds only) of all modalities of PNL. The resulting modality templates are as follows: the prompt-right-adjacency $\langle A_{x} \rangle$ and the prompt-left-adjacency $\langle \overline{A}_{x} \rangle$, capturing prompt-liveness in the future and in the past, respectively, as well as the dual modalities $[ A_{x} ]$ and $[ \overline{A}_{x} ]$. Intuitively, a modality $\langle A_{x} \rangle$ (for some upper bound x) forces the existence of an event starting exactly when the current one terminates and ending within an amount of time bounded above by the value of x. Similarly, $\langle \overline{A}_{x} \rangle$ forces the existence of an event ending exactly when the current one begins and starting at most x time units before the beginning of the current one. Modalities $[ A_{x} ]$ and $[ \overline{A}_{x} ]$ express dual properties in the standard way, namely, ${{ [ A_{x} ]}} \psi$ stands for $\lnot {{ \langle A_{x} \rangle }} \lnot \psi$ and ${{ [ \overline{A}_{x} ]}} \psi$ stands for $\lnot {{ \langle \overline{A}_{x} \rangle }} \lnot \psi$. We name the proposed logic PROMPT- PNL (Sect. 2).

We first prove that the future fragment of PROMPT- PNL (PROMPT- RPNL), involving the future modalities $\langle A \rangle$, $[ A ]$, ${{ \langle A_{x} \rangle }}$, and ${{ [ A_{x} ]}}$ only, is expressive enough to encode the finite colouring problem, known to be undecidable [18]. Undecidability of PROMPT- RPNL (and PROMPT- PNL) immediately follows (Sect. 3). Notably, unlike LTL, PNL is strictly more expressive than its future fragment RPNL (see [12]); such a separation result holds between PROMPT- PNL and PROMPT- RPNL as well. Our undecidability result hinges on the unrestricted use of bounding variables within prompt modalities, which allows one to somehow establish tight bounds for the length of intervals. We show that decidability can be recovered by using two disjoint sets of bounding variables, one for existential modalities and the other for universal ones. Formulas of the resulting logic, which we name , enjoy some useful monotonicity property, i.e., the truth of a formula ${{ \langle A_{x} \rangle }} \psi$ under a certain interpretation ${\sigma } (x)$ of the bounding variable x implies its truth under every interpretation ${\sigma } '$, with ${\sigma } '(x) \ge {\sigma } (x)$. This allows us to prove a small (pseudo-)model property for , from which we conclude that the satisfiability problem for is NEXPTIME-complete (Sect. 4). Due to lack of space, most of the proofs are omitted (see [11] for full proofs).

2 The Logic PROMPT- PNL

Let us start with some basic notions of interval-based temporal logics. A linear order $\mathbb D$ is a pair $\langle D, < \rangle$, where D is a set, called domain, whose elements are referred to as points, and < is a strict total order over D. A (strongly) discrete linear order is a linear order such that there are only finitely many points in between any two points. In the rest of the paper, we tacitly assume every domain to be discrete. For the sake of simplicity, we identify the domain of a linear order with the linear order itself, e.g., we write “$d \in \mathbb D$” instead of “$d \in D$”. Let $d \in {\mathbb {D}}$. The successors (resp., predecessors) of d in $\mathbb {D}$ are the points $d' \in {\mathbb {D}}$ such that $d < d'$ (resp., $d' < d$); the immediate successor (resp., immediate predecessor) of d in $\mathbb {D}$, denoted by ${\mathtt {succ}_{\mathbb {D}}} (d)$ (resp., ${\mathtt {pred}_{\mathbb {D}}} (d)$), is (if any) the point $d' \in {\mathbb {D}}$ such that $d'$ is a successor (resp., predecessor) of d in $\mathbb {D}$ and no point $d'' \in {\mathbb {D}}$ exists with $d< d'' < d'$ (resp., $d'< d'' < d$). Note that ${\mathtt {succ}_{\mathbb {D}}} (d)$ (resp., ${\mathtt {pred}_{\mathbb {D}}} (d)$) is defined unless d is the greatest (resp., least) element in ${\mathbb {D}}$. Given a linear order $\mathbb D$ and two points $a,b \in \mathbb D$, with $a < b$, we denote by [a, b] an interval (over $\mathbb D$). The set of intervals over a linear order $\mathbb D$ is denoted by $\mathbb {I(D)}$. An interval structure (over a countable set $\mathcal {AP}$ of atomic propositions) is a pair $\langle \mathbb D, V \rangle$, where $\mathbb D$ is a linear order and $V : \mathbb {I(D)} \rightarrow 2^{{\mathcal {AP}}}$ is a valuation function, which assigns to each interval over $\mathbb D$ the set of atomic proposition that are true over it. Given a linear order $\mathbb {D}$ and $a,b \in {\mathbb {D}}$, we denote by ${\mathbb {D}} ^{\ge a}$ (resp., ${\mathbb {D}} ^{> a}$, ${\mathbb {D}} ^{\le a}$, ${\mathbb {D}} ^{< a}$, ${\mathbb {D}} ^{[a,b]}$, ${\mathbb {D}} ^{]a,b[}$, ${\mathbb {D}} ^{[a,b[}$, ${\mathbb {D}} ^{]a,b]}$) the set of elements $d \in {\mathbb {D}}$ such that $d \ge a$ (resp., $d > a$, $d \le a$, $d < a$, $a \le d \le b$, $a< d < b$, $a \le d < b$, $a < d \le b$). For instance, we denote by ${\mathbb {\mathbb R}} ^{> 0}$ the set of positive reals.

Syntax and Semantics. Let $\mathcal {AP}$ (atomic propositions) and X (bounding variables) be two countable sets. Formulas of PROMPT- PNL in negation normal form are defined as follows:

$\begin{array}{l@{\quad }r@{\quad }c@{\quad }l@{\quad }c@{\quad } l@{\quad }c@{\quad }l@{\quad }c@{\quad }l@{\quad }c@{\quad }l@{\quad }c} \varphi &{} {:}{:}= &{} p &{} \mid &{} \varphi \wedge \varphi &{} \mid &{} \langle A \rangle \varphi &{} \mid &{} \langle \overline{A} \rangle \varphi &{} \mid &{} {{ \langle A_{x} \rangle }} \varphi &{} \mid &{} {{ \langle \overline{A}_{x} \rangle }} \varphi \\ &{} \mid &{} \lnot p &{} \mid &{} \varphi \vee \varphi &{} \mid &{} [ A ]\varphi &{} \mid &{} [ \overline{A} ]\varphi &{} \mid &{} {{ [ A_{x} ]}} \varphi &{} \mid &{} {{ [ \overline{A}_{x} ]}} \varphi \end{array}$

where $p \in {\mathcal {AP}}$ and $x \in X$. We also use other standard Boolean connectives, e.g., $\rightarrow$, and logical constants $\top$ and $\bot$, which are defined in the usual way. We denote by PROMPT- RPNL the PROMPT- PNL fragment obtained by excluding past modalities $\langle \overline{A} \rangle$, $[ \overline{A} ]$, ${{ \langle \overline{A}_{x} \rangle }}$, and ${{ [ \overline{A}_{x} ]}}$, and we write PROMPT-(R)PNL when we refer to both formalisms. In the following, we will take the liberty of writing PROMPT-(R)PNL formulas not in negation normal form when useful.

PROMPT-(R)PNL models are interval structures enriched with a valuation function for bounding variables in X and a metric over the underlying domain. Formally, a model for PROMPT-(R)PNL (over $\mathcal {AP}$ and X) is a quadruple $\langle \mathbb {D}, V, {\sigma }, \delta \rangle$, where $\langle \mathbb {D}, V \rangle$ is an interval structure ($\mathbb D$ is the domain of the model), ${\sigma }: X \rightarrow \mathbb R^{>0}$ is a valuation function for bounding variables, and $\delta : \mathbb D \times \mathbb D \rightarrow \mathbb R^{>0}$ is a metric over $\mathbb D$ (i.e., the pair $(\mathbb D, \delta )$ is a metric space) satisfying the additional properties: for every $d,d',d'' \in \mathbb D$ (i) if $d< d' < d''$, then $\delta (d,d'') = \delta (d,d') + \delta (d',d'')$, (ii) if d has infinitely many successors in $\mathbb {D}$, then the set ${\{ \delta (d,\bar{d}) \mid d < \bar{d} \}}$ is not bounded above, and (iii) if d has infinitely many predecessors in $\mathbb {D}$, then the set ${\{ \delta (\bar{d},d) \mid \bar{d} < d \}}$ is not bounded above. For a model $M = \langle \mathbb {D}, V, {\sigma }, \delta \rangle$, we let $\mathbb D_M = \mathbb D$, $V_M = V$, ${\sigma } _M = {\sigma }$, and $\delta _M = \delta$, that is, $\mathbb D_M$, $V_M$, ${\sigma } _M$, and $\delta _M$ denote the four components of M. A PROMPT-(R)PNL model is finite (resp., infinite) if so is its domain.

The truth value of a PROMPT- PNL formula over a model and an interval in it is inductively defined as follows:

• $M, [a,b] \models p$ if and only if $p \in V_M([a,b])$, for every $p \in {\mathcal {AP}}$;

• $M, [a,b] \models \lnot p$ if and only if $p \not \in V_M([a,b])$, for every $p \in {\mathcal {AP}}$;

• $M, [a,b] \models \varphi _1 \wedge \varphi _2$ if and only if $M, [a,b] \models \varphi _1$ and $M, [a,b] \models \varphi _2$;

• $M, [a,b] \models \varphi _1 \vee \varphi _2$ if and only if $M, [a,b] \models \varphi _1$ or $M, [a,b] \models \varphi _2$;

• $M, [a,b] \models \langle A \rangle \varphi$ if and only if there is $c \in {\mathbb {D}} ^{> b} _M$ such that $M, [b,c] \models \varphi$;

• $M, [a,b] \models [ A ]\varphi$ if and only if for all $c \in {\mathbb {D}} ^{> b} _M$ it holds $M, [b,c] \models \varphi$;

• $M, [a,b] \models \langle \overline{A} \rangle \varphi$ if and only if there is $c \in {\mathbb {D}} ^{< a} _M$ such that $M,[c,a] \models \varphi$;

• $M, [a,b] \models [ \overline{A} ]\varphi$ if and only if for all $c \in {\mathbb {D}} ^{< a} _M$ it holds $M,[c,a] \models \varphi$;

• $M, [a,b] \models {{ \langle A_{x} \rangle }} \varphi$ if and only if there is $c \in {\mathbb {D}} ^{> b} _M$, with $\delta _M(b,c) \le {\sigma } _M(x)$, such that $M,[b,c] \models \varphi$, for every $x \in X$;

• $M, [a,b] \models {{ [ A_{x} ]}} \varphi$ if and only if for all $c \in {\mathbb {D}} ^{> b} _M$, with $\delta _M(b,c) \le {\sigma } _M(x)$, it holds $M,[b,c] \models \varphi$, for every $x \in X$;

• $M, [a,b] \models {{ \langle \overline{A}_{x} \rangle }} \varphi$ if and only if there is $c \in {\mathbb {D}} ^{< a} _M$, with $\delta _M(c,a) \le {\sigma } _M(x)$, such that $M,[c,a] \models \varphi$, for every $x \in X$;

• $M, [a,b] \models {{ [ \overline{A}_{x} ]}} \varphi$ if and only if for all $c \in {\mathbb {D}} ^{< a} _M$, with $\delta _M(c,a) \le {\sigma } _M(x)$, it holds $M,[c,a] \models \varphi$, for every $x \in X$.

The truth value of a PROMPT- RPNL formula is obtained, as expected, by restricting to the relevant clauses only.

In PNL, modalities $\langle L \rangle$ and $\langle \overline{L} \rangle$, corresponding to Allen’s relations later and before, are definable as: $\langle L \rangle \varphi \equiv \langle A \rangle \langle A \rangle \varphi$ and $\langle \overline{L} \rangle \varphi \equiv \langle \overline{A} \rangle \langle \overline{A} \rangle \varphi$. Additionally, in PROMPT- PNL it is possible to define the ‘prompt’ counterparts of modalities $\langle L \rangle$ and $\langle \overline{L} \rangle$ as: ${{ \langle L_{x} \rangle }} \varphi \equiv {{ \langle A_{x} \rangle }} {{ \langle A_{x} \rangle }} \varphi$ and ${{ \langle \overline{L}_{x} \rangle }} \varphi \equiv {{ \langle \overline{A}_{x} \rangle }} {{ \langle \overline{A}_{x} \rangle }} \varphi$. The resulting semantic interpretation for ${{ \langle L_{x} \rangle }}$ and ${{ \langle \overline{L}_{x} \rangle }}$ is as follows:

• $M, [a,b] \models {{ \langle L_{x} \rangle }} \varphi$ if and only if there is $[c,d] \in \mathbb {I}(\mathbb D_M)$ such that $b < c$, $\delta _M(b,c) \le {\sigma } _M(x)$, $\delta _M(c,d) \le {\sigma } _M(x)$, and $M,[c,d] \models \varphi$;

• $M, [a,b] \models {{ \langle \overline{L}_{x} \rangle }} \varphi$ if and only if there is $[c,d] \in \mathbb {I}(\mathbb D_M)$ such that $d < a$, $\delta _M(d,a) \le {\sigma } _M(x)$, $\delta _M(c,d) \le {\sigma } _M(x)$, and $M,[c,d] \models \varphi$.

Intuitively, a modality $\langle L_{x} \rangle$, for some bounding variable x, requires the existence of an event starting and ending within a bounded amount of time after the termination of the current one (modalities $\langle \overline{L}_{x} \rangle$ impose an analogous constraint in the past). Obviously, only $\langle L_{x} \rangle$ is definable in PROMPT- RPNL ($\langle \overline{L}_{x} \rangle$ is not).

The globally-in-the-future modality $[G]$ is defined as $[G]\psi \equiv \psi \wedge [ A ]\psi \wedge [ A ][ A ]\psi$, for every PROMPT- PNL formula $\psi$; analogously the prompt-globally-in-the-future modality $[G_{x}]$ is defined as $[G_{x}]\psi \equiv \psi \wedge {{ [ A_{x} ]}} \psi \wedge [ A ]{{ [ A_{x} ]}} \psi$, for every PROMPT- PNL formula $\psi$ and $x \in X$. Given a PROMPT-(R)PNL model M, modalities $[G]$ and $[G_{x}]$ induce the sets ${\mathcal G^{[a,b]}_{M}} = {\{ [a,b] \}} \cup {\{ [c,d] \in \mathbb I({\mathbb {D}} _M) \mid b \le c \}}$ and ${\mathcal G^{[a,b],x}_{M}} = {\{ [a,b] \}} \cup {\{ [c,d] \in \mathbb I({\mathbb {D}} _M) \mid b \le c \text { and } \delta _M(c,d) \le {\sigma } _M(x) \}}$. We omit the subscript $_M$ when it is clear from the context. For every PROMPT-(R)PNL model M, $[a,b] \in \mathbb I({\mathbb {D}} _M)$, and PROMPT- PNL formula $\psi$, it holds that $M,[a,b] \models [G]\psi$ if and only if $M,[c,d] \models \psi$ for every $[c,d] \in {\mathcal G^{[a,b]}_{}}$ and $M,[a,b] \models [G_{x}]\psi$ if and only if $M,[c,d] \models \psi$ for every $[c,d] \in {\mathcal G^{[a,b],x}_{}}$. Finally, for a model M and $[a,b] \in \mathbb I({\mathbb {D}} _M)$, we define the length of [a, b] (in M) as the value $\delta _M(a,b)$ and, for every $p \in {\mathcal {AP}}$, if $M, [a,b] \models p$, then we say that [a, b] is a p-interval (in M).

The Satisfiability Problem. A PROMPT-(R)PNL formula $\varphi$ is satisfiable if, and only if, there exist a PROMPT-(R)PNL model M and an interval [x, y] in M such that $M, [x,y] \models \varphi$. Moreover, a satisfiable formula is said to be finitely satisfiable if there exists a finite model for it; otherwise it is non-finitely satisfiable. The satisfiability (resp., finite satisfiability) problem for PROMPT-(R)PNL consists in deciding whether a given PROMPT-(R)PNL formula is satisfiable (resp., finitely satisfiable).

3 Undecidability of PROMPT- RPNL

We prove the undecidability of the satisfiability problem for the logic PROMPT- RPNL (and thus for PROMPT- PNL as well), by a reduction from the finite coloring problem (FCP) [18]. An instance of FCP (aka finite tiling problem) is a tuple $\varDelta = \langle C, H, V, c_i,$ $c_f \rangle$, where C is a finite, non-empty set of colours, $H, V \subseteq C \times C$ are total binary relations over the set of colours C, and $c_i, c_f \in C$ are distinguished colours. A solution to $\varDelta$ is a pair $\langle \mathcal C, (K,L) \rangle$, where $K,L \in \mathbb N$ and $\mathcal C : \{ 0, \ldots , K \} \times \{ 0, \ldots , L \} \rightarrow C$ is a colouring function such that $\mathcal C(0,0) = c_i$, $\mathcal C(K,L) = c_f$, and, in addition,

• $(\mathcal C(i,j), \mathcal C(i+1,j)) \in H$, for each $i < K$ and $j \le L$ (horizontal constraint), and

• $(\mathcal C(i,j), \mathcal C(i,j+1)) \in V$, for each $i \le K$ and $j < L$ (vertical constraint).

FCP consists in establishing whether there are two natural numbers K and L, and a colouring of the plane $\{ 0, \ldots , K \} \times \{ 0, \ldots , L \}$ such that horizontal and vertical constraints are fulfilled, and bottom-left and top-right colours are given. CFP is undecidable [18, Proposition 7.2]. We encode CFP by means of a PROMPT- RPNL formula. The different aspects of the problem are encoded by means of (blocks of) formulas and the correctness of such partial encodings is testified by the corresponding lemmas below. Clearly, the conjunction of all these formulas is satisfiable if and only if CFP admits a solution. In what follows, we fix an interval model $M = \langle \mathbb {D}, V, {\sigma }, \delta \rangle$.

For every $d \in \mathbb {D}$ and $x \in X$, we define ${{\lfloor {\sigma } \rfloor _{d}} (x)} = \max \{ \delta (d,d') \in \mathbb R^{>0} \mid d' \in {\mathbb {D}} ^{> d} \text { and } \delta (d,d') \le {\sigma } (x) \}$. It clearly holds that ${{\lfloor {\sigma } \rfloor _{d}} (x)} \le {\sigma } (x)$ and, for every $d' \in {{\mathbb {D}} ^{\ge d}}$, we have that $\delta (d,d') \le {\sigma } (x)$ implies $\delta (d,d') \le {{\lfloor {\sigma } \rfloor _{d}} (x)}$. For every $x \in X$, there is exactly one point $d' \in {{\mathbb {D}} ^{\ge d}}$ such that $\delta (d,d') = {{\lfloor {\sigma } \rfloor _{d}} (x)}$; we call such a point the x-canonical successor of d. The length of an interval $[d,d'] \in \mathbb I({\mathbb {D}})$, where $d'$ is the x-canonical successor of d, is said to be x-canonical, for every $x \in X$.

Let $succ \text {-}upperbound$ be the formula $[G](\langle A \rangle \top \rightarrow {{ \langle A_{s} \rangle }} \top )$, where $s \in X$.

Lemma 1

If $M,[a,b] \models { succ \text {-}upperbound }$ for some [a, b], then for every $c \in {{\mathbb {D}} ^{\ge b}}$ that is not the greatest element in $\mathbb {D}$ it holds $\delta (c,{\mathtt {succ}_{\mathbb {D}}} (c)) \le {{\lfloor {\sigma } \rfloor _{c}} (s)}$. Moreover, let $c'$ be the x-canonical successor of c. If $c'$ is not the greatest element in $\mathbb {D}$, then ${{\lfloor {\sigma } \rfloor _{c}} (x)} + {\sigma } (s) > {\sigma } (x)$, for every $x \in X$.

Let $less \text {-}than( x,y )$ be the formula $[G](\langle A \rangle \top \rightarrow { \langle A_{y} \rangle } {\mathsf {aux_{ x,y }}}) \wedge [G]{{ [ A_{x} ]}} \lnot {\mathsf {aux_{ x,y }}}$ (it is a parametric formula to be instantiated with some $x,y \in X$).

Lemma 2

If $M,[a,b] \models { less \text {-}than( x,y ) }$ for some [a, b], then ${\sigma } (x) < {{\lfloor {\sigma } \rfloor _{c}} (y)}$ holds for every $c \in {{\mathbb {D}} ^{\ge b}}$, unless c is the greatest element in $\mathbb {D}$.

Let $\exists \text {-}last$ be the conjunction of the following formulas:

$$\begin{aligned}&\lnot {\mathsf {last}} \wedge \langle A \rangle \langle A \rangle {\mathsf {last}} \wedge [G](\langle A \rangle {\mathsf {last}} \rightarrow \bigwedge \nolimits _{{\mathsf {p}} \in {\mathcal {AP}}} [ A ](\lnot {\mathsf {p}} \wedge [ A ]\lnot {\mathsf {p}})) \end{aligned}$$

(1)

$$\begin{aligned}&[G](\langle A \rangle {\mathsf {last}} \rightarrow [ A ]\lnot \langle A \rangle {\mathsf {last}}) \end{aligned}$$

(2)

$$\begin{aligned}&[G](({\mathsf {last}} \rightarrow \langle A \rangle {\mathsf {unique}}) \wedge (\langle A \rangle {\mathsf {unique}} \rightarrow [ A ]\lnot \langle A \rangle {\mathsf {unique}})) \end{aligned}$$

(3)

Lemma 3

If $M,[a,b] \models { \exists \text {-}last }$ for some [a, b], then there is exactly one $\mathsf {last}$-interval in $\mathcal G^{[a,b]}_{}$, say it [c, d]. Moreover, it holds $c > b$ and there is no $\mathsf {p}$-interval starting in c or after it, for every ${\mathsf {p}} \in {\mathcal {AP}} \setminus {\{ {\mathsf {last}} \}}$.

Let $a \in {\mathbb {D}}$ and $[c,d] \in \mathbb I({\mathbb {D}})$ be the unique $\mathsf {last}$-interval (see Lemma 3). Given ${\mathsf {p}} \in {\mathcal {AP}}$, a $\mathsf {p}$ -chain starting at a (or, simply, $\mathsf {p}$ -chain) is a finite sequence of $\mathsf {p}$-intervals $[a_0,b_0], [a_1,b_1], \ldots , [a_m,b_m]$ such that $a = a_0$, $b_m = c$, and $b_i = a_{i+1}$ for every $i \in {\{ 0, 1, \ldots , m-1 \}}$. Let $chain({\mathsf {p}},x)$ be the parametric formula, to be instantiated with some ${\mathsf {p}} \in {\mathcal {AP}}$ and $x \in X$, defined as the conjunction of the following ones:

$$\begin{aligned}&{ succ \text {-}upperbound } \wedge { \exists \text {-}last } \end{aligned}$$

(4)

$$\begin{aligned}&\lnot {\mathsf {p}} \wedge {{ \langle A_{x} \rangle }} {\mathsf {p}} \wedge [G](({\mathsf {p}} \wedge \lnot \langle A \rangle {\mathsf {last}}) \rightarrow {{ \langle A_{x} \rangle }} {\mathsf {p}}) \end{aligned}$$

(5)

$$\begin{aligned}&[G]({\mathsf {p}} \rightarrow {\mathsf {p_1}} \vee {\mathsf {p_2}}) \end{aligned}$$

(6)

$$\begin{aligned}&[G](\langle A \rangle {{\mathsf {p}} _{i}} \rightarrow {{ [ A_{x} ]}} [ A ]{{\mathsf {p}} _{i}^{+}})&i \in \{ 1,2 \} \end{aligned}$$

(7)

$$\begin{aligned}&[G_{x}](\langle A \rangle {{\mathsf {p}} _{i}^{+}} \rightarrow {{\mathsf {p}} _{i}^{-}})&i \in \{ 1,2 \} \end{aligned}$$

(8)

$$\begin{aligned}&[G]({{\mathsf {p}} _{i}} \rightarrow \lnot \langle A \rangle {{\mathsf {p}} _{i}^{-}})&i \in \{ 1,2 \} \end{aligned}$$

(9)

$$\begin{aligned}&[G](\langle A \rangle {\mathsf {p}} \rightarrow {{ [ A_{x} ]}} (\lnot {\mathsf {p}} \rightarrow [ A ]\lnot {\mathsf {p}})) \end{aligned}$$

(10)

Lemma 4

If $M,[a,b] \models { chain({\mathsf {p}},x) }$ for some [a, b], then there is a finite $\mathsf {p}$-chain starting at b whose intervals have x-canonical length. Moreover, no other $\mathsf {p}$-interval exists in $\mathcal G^{[a,b],x}_{}$ besides the ones in such a $\mathsf {p}$-chain.

We now provide an encoding of a finite plane $\{ 0, \ldots , K \} \times \{ 0, \ldots , L \}$, for some $K, L \in {\mathbb {N}}$. The idea is to use a $\mathsf {u}$-chain whose intervals are either $\mathsf {tile}$-intervals, encoding some point of the finite plane, or $\mathsf {*}$-intervals, which are used as separators between rows of the plane. Let $plane$ be the conjunction of the following formulas:

$$\begin{aligned}&{ less \text {-}than( s,x ) } \wedge { less \text {-}than( x,y ) } \wedge { chain({\mathsf {u}},x) } \wedge { chain({\mathsf {row}},y) } \end{aligned}$$

(11)

$$\begin{aligned}&[G](({\mathsf {u}} \leftrightarrow {\mathsf {*}} \vee {\mathsf {tile}}) \wedge ({\mathsf {*}} \rightarrow \lnot {\mathsf {tile}})) \end{aligned}$$

(12)

$$\begin{aligned}&\langle A \rangle {\mathsf {*}} \wedge [G](({\mathsf {*}} \rightarrow \langle A \rangle {\mathsf {tile}}) \wedge ({\mathsf {u}} \wedge \langle A \rangle {\mathsf {last}} \rightarrow {\mathsf {tile}})) \end{aligned}$$

(13)

$$\begin{aligned}&[G](\langle A \rangle {\mathsf {row}} \rightarrow \langle A \rangle {\mathsf {*}}) \end{aligned}$$

(14)

$$\begin{aligned}&[G](\langle A \rangle {\mathsf {*}} \rightarrow {{ [ A_{y} ]}} (\langle A \rangle {\mathsf {*}} \rightarrow {\mathsf {row}})) \end{aligned}$$

(15)

Lemma 5

If $M,[a,b] \models { plane }$ for some [a, b], then there is a finite sequence of points $b = p_0^1< p_1^1< \ldots< p_{n_1}^1 = p_0^2< p_1^2< \ldots< p_{n_2}^2 = p_0^3< \ldots< p_{n_{r-1}}^{r-1} = p_0^r< \ldots < p_{n_r}^r$, with $r \ge 1$ and $n_i > 1$ for every $i \in \{ 1, \ldots , r \}$ such that: (i) $[p_0^i,p_1^i]$ is a $\mathsf {*}$-interval and its length is x-canonical, for every $i \in \{ 1, \ldots , r \}$; (ii) $[p_j^i,p_{j+1}^i]$ is a $\mathsf {tile}$-interval and its length is x-canonical, for every $i \in \{ 1, \ldots , r \}$ and $j \in \{ 1, \ldots , n_i-1 \}$; (iii) $[p_0^i,p_0^{i+1}]$ is a $\mathsf {row}$-interval and its length is y-canonical, for every $i \in \{ 1, \ldots , r-1 \}$; (iv) $M,[p_{n_r}^r,p']$ is the unique $\mathsf {last}$-interval, for some $p' > p_{n_r}^r$. Moreover, no other $\mathsf {*}$-interval (resp., $\mathsf {tile}$-interval) exists in $\mathcal G^{[a,b],x}_{}$.

The encoding of the finite plane $\{ 0, \ldots , K \} \times \{ 0, \ldots , L \}$ we have obtained so far is incomplete, the problem being that rows ($\mathsf {row}$-intervals) do not necessarily contain the same number of tiles ($\mathsf {tile}$-intervals). In order to overcome such a problem, we introduce below $\mathsf {corr}$-intervals, which are used to link the ith $\mathsf {tile}$-interval of a row to the ith $\mathsf {tile}$-interval of the next row (if any) and to the ith $\mathsf {tile}$-interval of the previous row (if any). This will guarantee that each row of our encoding features the same number of tiles.

Let $w \text {-}def$ be the conjunction of the following formulas:

$$\begin{aligned}&{ less \text {-}than( x,w ) } \wedge { less \text {-}than( w,y ) } \end{aligned}$$

(16)

$$\begin{aligned}&{{ [ A_{y} ]}} \lnot \langle A \rangle {\mathsf {{\mathsf {*}} \text {-}aux}} \wedge ({{ \langle A_{y} \rangle }} ({\mathsf {row}} \wedge \lnot {{ \langle A_{x} \rangle }} {\mathsf {last}}) \rightarrow \langle A \rangle \langle A \rangle {\mathsf {{\mathsf {*}} \text {-}aux}}) \end{aligned}$$

(17)

$$\begin{aligned}&{{ \langle A_{s} \rangle }} {{ \langle A_{w} \rangle }} ([ A ](\lnot {\mathsf {last}} \wedge [ A ]\lnot {\mathsf {last}}) \vee \langle A \rangle {\mathsf {{\mathsf {*}} \text {-}aux}}) \end{aligned}$$

(18)

Lemma 6

If $M,[a,b] \models { plane } \wedge { w \text {-}def }$ for some [a, b], then ${\sigma } (w)< {{\lfloor {\sigma } \rfloor _{c}} (y)} \le {\sigma } (y) < {\sigma } (w) + {\sigma } (s)$ for every $c \in {{\mathbb {D}} ^{\ge b}}$, unless c is the greatest element in $\mathbb {D}$.

Let $correspondence$ be the conjunction of the following formulas:

$$\begin{aligned}&{ plane } \wedge { w \text {-}def } \wedge { less \text {-}than( s,z ) } \wedge { less \text {-}than( z,x ) } \end{aligned}$$

(19)

$$\begin{aligned}&[G]({{ \langle A_{x} \rangle }} {\mathsf {u}} \rightarrow {{ [ A_{z} ]}} {{ \langle A_{z} \rangle }} ({\mathsf {u \text {-}suffix}} \wedge ({{ \langle A_{x} \rangle }} {\mathsf {u}} \vee \langle A \rangle {\mathsf {last}}))) \end{aligned}$$

(20)

$$\begin{aligned}&[G_{s}] \lnot {\mathsf {u \text {-}suffix}} \end{aligned}$$

(21)

$$\begin{aligned}&[G](({\mathsf {row}} \wedge \lnot \langle A \rangle {\mathsf {last}}) \rightarrow {\mathsf {corr}}) \end{aligned}$$

(22)

$$\begin{aligned}&[G](({{ \langle A_{x} \rangle }} {\mathsf {tile}} \wedge \langle A \rangle {{ \langle A_{x} \rangle }} {\mathsf {*}}) \rightarrow {{ \langle A_{y} \rangle }} {\mathsf {corr}}) \end{aligned}$$

(23)

$$\begin{aligned}&[G_{w}]\lnot {\mathsf {corr}} \end{aligned}$$

(24)

$$\begin{aligned}&[G]({\mathsf {corr}} \rightarrow \langle A \rangle {\mathsf {tile}})\end{aligned}$$

(25)

$$\begin{aligned}&[G]({{ \langle A_{x} \rangle }} ({\mathsf {tile}} \wedge {{ \langle A_{x} \rangle }} {\mathsf {*}}) \rightarrow {{ [ A_{y} ]}} ({\mathsf {corr}} \rightarrow {{ \langle A_{x} \rangle }} ({\mathsf {tile}} \wedge {{ \langle A_{x} \rangle }} {\mathsf {*}}))) \end{aligned}$$

(26)

Lemma 7

If $M,[a,b] \models { correspondence }$ for some [a, b], then $[p_j^i,p_j^{i+1}]$ is a $\mathsf {corr}$-interval, with ${\sigma } (w) < \delta (p_j^i,p_j^{i+1}) \le {\sigma } (y)$, for every $i \in {\{ 1, \ldots , r-1 \}}$ and $j \in {\{ 0, \ldots , n_i-1 \}}$. Moreover, for every $i \in {\{ 1, \ldots , r-1 \}}$, it holds that $n_i = n_{i+1}$.

Now, let $\varDelta = \langle C, H, V, c_i, c_f \rangle$ be an instance of FCP and let $\varphi _\varDelta$ be the conjunction of the following formulas:

$$\begin{aligned}&{ correspondence } \wedge {{ \langle A_{x} \rangle }} {\mathsf {c_i}} \wedge [G_{x}] (({\mathsf {tile}} \wedge \langle A \rangle {\mathsf {last}}) \rightarrow {\mathsf {c_f}}) \end{aligned}$$

(27)

$$\begin{aligned}&[G_{x}] ({\mathsf {tile}} \leftrightarrow \bigvee \nolimits _{{\mathsf {c}} \in C} {\mathsf {c}}) \wedge [G]( \bigwedge \nolimits _{{\mathsf {c}},{\mathsf {c'}} \in C, {\mathsf {c}} \ne {\mathsf {c'}}} \lnot ({\mathsf {c}} \wedge {\mathsf {c'}}) )\end{aligned}$$

(28)

$$\begin{aligned}&[G]({{ \langle A_{x} \rangle }} ({\mathsf {tile}} \wedge {{ \langle A_{x} \rangle }} {\mathsf {tile}}) \rightarrow \bigvee \nolimits _{({\mathsf {c}},{\mathsf {c'}}) \in H} {{ \langle A_{x} \rangle }} ({\mathsf {c}} \wedge {{ \langle A_{x} \rangle }} {\mathsf {c'}}))\end{aligned}$$

(29)

$$\begin{aligned}&[G_{x}] (({{ \langle A_{x} \rangle }} {\mathsf {tile}} \wedge {{ \langle A_{y} \rangle }} {\mathsf {corr}}) \rightarrow \bigvee \nolimits _{({\mathsf {c}},{\mathsf {c'}}) \in V} ({{ \langle A_{x} \rangle }} {\mathsf {c}} \wedge {{ [ A_{y} ]}} ({\mathsf {corr}} \rightarrow {{ \langle A_{x} \rangle }} {\mathsf {c'}}))) \end{aligned}$$

(30)

Lemma 8

The formula $\varphi _\varDelta$ is satisfiable iff the CFP instance $\varDelta$ has a positive answer.

Theorem 1

The satisfiability problem for PROMPT- RPNL, and thus the one for PROMPT- PNL, is undecidable.

4 Decidability of

In this section, we show how to restrict the use of prompt modalities to get a fragment of PROMPT- PNL with a decidable satisfiability problem.

We define as the fragment of PROMPT- PNL obtained by using disjoint sets of bounding variables for existential and universal prompt modalities. Formally, let us partition the set X of bounding variables into sets $X_{\Diamond }$ and $X_{\Box }$. The syntax of is defined as:

$\begin{array}{l@{\quad }r@{\quad }c@{\quad }l@{\quad }c@{\quad } l@{\quad }c@{\quad }l@{\quad }c@{\quad }l@{\quad }c@{\quad }l@{\quad }c} \varphi &{} {:}{:}= &{} p &{} \mid &{} \varphi \wedge \varphi &{} \mid &{} \langle A \rangle \varphi &{} \mid &{} \langle \overline{A} \rangle \varphi &{} \mid &{} {{ \langle A_{x} \rangle }} \varphi &{} \mid &{} {{ \langle \overline{A}_{x} \rangle }} \varphi \\ &{} \mid &{} \lnot p &{} \mid &{} \varphi \vee \varphi &{} \mid &{} [ A ]\varphi &{} \mid &{} [ \overline{A} ]\varphi &{} \mid &{} {{ [ A_{y} ]}} \varphi &{} \mid &{} {{ [ \overline{A}_{y} ]}} \varphi \end{array}$

where $p \in {\mathcal {AP}}$, $x \in X_{\Diamond }$, and $y \in X_{\Box }$. Since is a syntactic restriction of PROMPT- PNL, both formalisms share the same semantics. In particular, a PROMPT- PNL model is a model as well. Analogously to the unrestricted case, we define as devoid of past modalities $\langle \overline{A} \rangle$, $[ \overline{A} ]$, ${{ \langle \overline{A}_{x} \rangle }}$, and ${{ [ \overline{A}_{y} ]}}$.

is not closed under negation. For any given formula $\psi$, we inductively define $neg(\psi )$ as shown in Table 1 ($neg(\psi )$ is not necessarily a formula). If $\psi$ is a (non-prompt) PNL formula, then $neg(\psi ) \equiv \lnot \psi$. Moreover, we define $neg({\sim \! \psi })$ as $\psi$ and thus we have that $neg(neg(\psi )) \equiv \psi$, for every formula $\psi$.

Table 1. Definition of $neg(\psi )$, for a formula $\psi$

A close analysis of the proof of the undecidability of PROMPT-(R)PNL reveals that the unrestricted use of bounding variables within prompt modalities allows one to somehow establish tight bounds for the length of intervals, and this ability is crucial to the encoding. We are going to show that decidability can be recovered by not allowing both existential and universal prompt quantification on the same bounding variable. Intuitively, decidability follows from the fact that, when disjoint sets of bounding variables are used within existential and universal prompt modalities, formulas enjoy a monotonicity property, which does not hold for unrestricted PROMPT-(R)PNL formulas.

Let $M = \langle \mathbb {D}, V, {\sigma }, \delta \rangle$ be a PROMPT- PNL model, $x \in X$, and $r \in {\mathbb {R}} ^{> 0}$. We denote by $M_{[x := r]}$ the model $\langle \mathbb {D}, V, {\sigma } ', \delta \rangle$, where ${\sigma } '(x) = r$ and ${\sigma } '(x') = {\sigma } (x')$ for every $x' \in X$ with $x' \ne x$.

Proposition 1

(monotonicity). Let $\psi$ be a formula of , M be a model of , and [a, b] be an interval in M. If $M, [a,b] \models \psi$, then $M_{[x:=r]}, [a,b] \models \psi$ for all $x \in X_{\Diamond }$ and $r \in {\mathbb {R}} ^{> 0}$, with $r \ge {\sigma } _M(x)$. In a dual fashion, if $M, [a,b] \models \psi$, then $M_{[y:=r]}, [a,b] \models \psi$ for all $y \in X_{\Box }$ and $r \in {\mathbb {R}} ^{> 0}$, with $r \le {\sigma } _M(y)$.

Checking that the above monotonicity property holds for is immediate. To see that it does not hold for PROMPT- PNL, consider the formula $\psi = {{ [ A_{y} ]}} \lnot {\mathsf {p}} \wedge {{ \langle A_{x} \rangle }} {\mathsf {p}} \wedge {{ [ A_{x} ]}} \lnot {\mathsf {q}} \wedge {{ \langle A_{z} \rangle }} {\mathsf {q}}$. Clearly, $\psi$ is satisfiable and all of its models are such that the value of x is bounded below by the value of y and above by the value of z.

By Proposition 1, when studying the (finite) satisfiability problem for we can assume, w.l.o.g., that $| X_{\Diamond } | = | X_{\Box } | = 1$, as every formula $\psi$, featuring (possibly) more than one bounding variable in $X_{\Diamond }$ or $X_{\Box }$, can be transformed into an equisatisfiable one $\psi '$, obtained by replacing two distinguished (chosen randomly) variables $\hat{x} \in X_{\Diamond }$ and $\hat{y} \in X_{\Box }$ for every $x \in X_{\Diamond }$ and $y \in X_{\Box }$, respectively. It is not difficult to check that, due to monotonicity, $\psi$ is (finitely) satisfiable if and only if so is $\psi '$. Therefore, for the remainder of the section, we set $X_{\Diamond } = {\{ x \}}$ and $X_{\Box } = {\{ y \}}$.

Finite Satisfiability. The finite satisfiability problem for can be reduced to the one for plain PNL, known to be NEXPTIME-complete [8]. Let $\psi$ be a formula of and let $plain (\psi )$ be the PNL formula obtained from $\psi$ by:

• (i) replacing existential prompt modalities by the corresponding non-prompt versions (i.e., substituting $\langle A \rangle$ for $\langle A_{x} \rangle$ and $\langle \overline{A} \rangle$ for $\langle \overline{A}_{x} \rangle$), and

• (ii) replacing all sub-formulas of the forms ${{ [ A_{y} ]}} \psi$ and ${{ [ \overline{A}_{y} ]}} \psi$ by the constant $\top$.

It is not difficult to show by induction on the structure of $\psi$ that if $\psi$ is finitely satisfiable, so is $plain (\psi )$. On the other hand, if $plain (\psi )$ is finitely satisfiable, then let $M_{ plain (\psi )} = \langle {\mathbb {D}}, V \rangle$ be a PNL model such that $M_{ plain (\psi )}, [a,b] \models { plain (\psi )}$ for some $[a,b] \in \mathbb I({\mathbb {D}})$. We define $\delta (d,d') = | {\{ d'' \in {\mathbb {D}} \mid d < d'' \le d' \}} |$ for every $d,d' \in {\mathbb {D}}$. Since $\mathbb {D}$ is finite, both $\max _\delta = \max {\{ \delta (d,d') \mid d,d' \in {\mathbb {D}} \text { and } d \ne d' \}}$ and $\min _\delta = \min {\{ \delta (d,d') \mid d,d' \in {\mathbb {D}} \text { and } d \ne d' \}}$ are well defined, thus we can set ${\sigma } (x) = \max _\delta$, and ${\sigma } (y) = \frac{\min _\delta }{2}$. It is possible to show that $M = \langle \mathbb {D}, V, {\sigma }, \delta \rangle$ is such that $M, [a,b] \models \psi$. Therefore, $\psi$ is finitely satisfiable, too.

Theorem 2

The finite satisfiability problem for is NEXPTIME-complete.

In order to deal with formulas that are non-finitely satisfiable, in what follows we show how the search for an infinite model can be reduced to the search for a finite witness for it, within a finite search space. Decidability of the satisfiability problem for immediately follows.

4.1 Prompt Labeled Interval Structures

In this subsection we define labeled interval structures for formulas, which are, intuitively, extended models, where intervals are labeled with sets of sub-formulas (instead of sets of atomic propositions) of the considered formula. From now on, we let $\varphi$ be a generic formula.

Let $Sub(\varphi )$ be the set of all sub-formulas of $\varphi$ and let $Sub^{\lnot } (\varphi ) = \{ neg(\psi ) \mid \psi \in Sub(\varphi ) \}$. The closure of $\varphi$, denoted by $\mathcal {C} l (\varphi )$, is the set $Sub(\varphi ) \cup Sub^{\lnot }(\varphi ) \cup \{ \langle A \rangle \varphi , neg(\langle A \rangle \varphi ) \}$. Clearly, $| \mathcal {C} l (\varphi ) | \le 2 \cdot | \varphi | + 2$ holds.

A future temporal request of $\varphi$ is a formula in $\mathcal {C} l (\varphi )$ having one of the following forms: $\langle A \rangle \psi$, $neg(\langle A \rangle \psi )$, ${{ \langle A_{x} \rangle }} \psi$, $neg({{ \langle A_{x} \rangle }} \psi )$, ${{ [ A_{y} ]}} \psi$, $neg({{ [ A_{y} ]}} \psi )$, for some $\psi$. Analogously, a past temporal request of $\varphi$ is a formula in $\mathcal {C} l (\varphi )$ having one of the following forms: $\langle \overline{A} \rangle \psi$, $neg(\langle \overline{A} \rangle \psi )$, ${{ \langle \overline{A}_{x} \rangle }} \psi$, $neg({{ \langle \overline{A}_{x} \rangle }} \psi )$, ${{ [ \overline{A}_{y} ]}} \psi$, $neg({{ [ \overline{A}_{y} ]}} \psi )$, for some $\psi$. We denote by $TR _{f}(\varphi )$ (resp., $TR _{p}(\varphi )$) the set of future (resp., past) temporal requests of $\varphi$. In addition, the set of temporal requests of $\varphi$, denoted by $TR _{}(\varphi )$, is defined as ${ TR _{f}(\varphi )} \cup { TR _{p}(\varphi )}$.

A $\varphi$ -atom is a subset A of $\mathcal {C} l (\varphi )$ such that, for every $\psi , \psi _1, \psi _2 \in \mathcal {C} l (\varphi )$, (i) $\psi \in A$ if and only if $neg (\psi ) \notin A$, and (ii) $\psi _1 \vee \psi _2 \in A$ if and only if $\psi _1 \in A$ or $\psi _2 \in A$. Notice that conditions (i) and (ii) imply $\psi _1 \wedge \psi _2 \in A$ if and only if $\psi _1 \in A$ and $\psi _2 \in A$. We denote the set of $\varphi$-atoms by $\mathcal A_\varphi$.

A prompt $\varphi$ -labeled interval structure ($\text {pLIS}_\varphi$) is a 5-tuple $\mathbf L = \langle \mathbb {D}, \mathcal L, \delta , {\mathcal {X}_{}^{}}, {\mathcal {Y}_{}^{}} \rangle$, where $(\mathbb D, \delta )$ is a metric space, $\mathcal L : \mathbb {I(D)} \rightarrow \mathcal A_{\varphi }$ is a labeling function (or simply labeling) such that $\varphi \in \mathcal L([a,b])$ for some $[a,b] \in \mathbb {I(D)}$, and ${\mathcal {X}_{}^{}}, {\mathcal {Y}_{}^{}} \in {\mathbb {N}}$ are the existential and the universal bound, respectively. Sometimes, for the sake of brevity, we omit the last three components of the 5-tuple and we denote a $\text {pLIS}_\varphi$ as a 2-tuple $\langle \mathbb {D}, \mathcal L \rangle$ instead. Moreover, given a $\text {pLIS}_\varphi$ ${\mathbf L} = \langle \mathbb {D}, \mathcal L \rangle$, we denote by ${\mathbb {D}} _{{\mathbf L}}$ its underlying domain $\mathbb {D}$ and by $\mathcal L_{{\mathbf L}}$ the labeling function $\mathcal L$. A $\text {pLIS}_\varphi$ ${\mathbf L}$ is finite (resp., infinite) if so is $\mathbb D_{{\mathbf L}}$.

Given a ${\text {pLIS}_\varphi }$ ${\mathbf L}$ and a point $d \in \mathbb {D}_{{\mathbf L}}$ we define the set of future requests of d in ${\mathbf L}$, denoted by ${\mathsf {f\text {-}REQ}^{{\mathbf L}}} (d)$, as $\bigcup _{d' \in {\mathbb {D}} ^{< d}} (\mathcal L_{\mathbf L} (d',d) \cap { TR _{f}(\varphi )})$, the set of past requests of d in ${\mathbf L}$, denoted by ${\mathsf {p\text {-}REQ}^{{\mathbf L}}} (d)$, as $\bigcup _{d' \in {\mathbb {D}} ^{> d}} (\mathcal L_{\mathbf L} (d,d') \cap { TR _{p}(\varphi )})$, and the set of requests of d in ${\mathbf L}$, denoted by ${\mathsf {REQ}^{{\mathbf L}}} (d)$, as ${\mathsf {f\text {-}REQ}^{{\mathbf L}}} (d) \cup {\mathsf {p\text {-}REQ}^{{\mathbf L}}} (d)$. We denote by ${\mathsf {REQ}_\varphi }$ the class of all sets of requests, i.e., ${\mathsf {REQ}_\varphi } = \{ \mathcal {R}\mid \mathcal {R}= {\mathsf {REQ}^{{\mathbf L}}} (d) \text { for some } {\text {pLIS}_\varphi } \text { } \mathbf L \text { and } d \in \mathbb {D}_{\mathbf L} \}$. We have that $| {\mathsf {REQ}_\varphi } | \le 2^{|\mathcal {C} l (\varphi )|} \le 2^{2 \cdot | \varphi | + 2}$.

An existential request of $\varphi$ is a temporal request of $\varphi$ of one the following forms: $\langle A \rangle \psi$, $\langle \overline{A} \rangle \psi$, ${{ \langle A_{x} \rangle }} \psi$, ${{ \langle \overline{A}_{x} \rangle }} \psi$, $neg({{ [ A_{y} ]}}) \psi$, and $neg({{ [ \overline{A}_{y} ]}}) \psi$, for some $\psi$. A universal request of $\varphi$ is a temporal request of $\varphi$ that is not an existential one. Let $\mathbf L = \langle \mathbb {D}, \mathcal L, \delta , {\mathcal {X}_{}^{}}, {\mathcal {Y}_{}^{}} \rangle$ be a ${\text {pLIS}_\varphi }$ and $d \in \mathbb {D}$. We define ${\exists \text {-}\mathsf {REQ}^{{\mathbf L}}} (d) = \{ \psi \in {\mathsf {REQ}^{{\mathbf L}}} (d) \mid \psi \text { is an existential request of } \varphi \}$ and ${\forall \text {-}\mathsf {REQ}^{{\mathbf L}}} (d) = {\mathsf {REQ}^{{\mathbf L}}} (d) \setminus {\exists \text {-}\mathsf {REQ}^{{\mathbf L}}} (d)$.

For $\psi \in {\exists \text {-}\mathsf {REQ}^{{\mathbf L}}} (d)$, we say that $\psi$ is fulfilled in $(\mathbf L,d)$ by $d' \in {\mathbb {D}}$ if, and only if, one of the following holds:

• $\psi = \langle A \rangle \psi '$ for some $\psi '$ and $\psi ' \in \mathcal L([d,d'])$,

• $\psi = \langle \overline{A} \rangle \psi '$ for some $\psi '$ and $\psi ' \in \mathcal L([d',d])$,

• $\psi = {{ \langle A_{x} \rangle }} \psi '$ for some $\psi '$, $\psi ' \in \mathcal L([d,d'])$, and $\delta (d,d') \le {\mathcal {X}_{}^{}}$,

• $\psi = {{ \langle \overline{A}_{x} \rangle }} \psi '$ for some $\psi '$, $\psi ' \in \mathcal L([d',d])$, and $\delta (d',d) \le {\mathcal {X}_{}^{}}$,

• $\psi = neg({{ [ A_{y} ]}} \psi ')$ for some $\psi '$, $neg(\psi ') \in \mathcal L([d,d'])$, and $\delta (d,d') \le {\mathcal {Y}_{}^{}}$,

• $\psi = neg({{ [ \overline{A}_{y} ]}} \psi ')$ for some $\psi '$, $neg(\psi ') \in \mathcal L([d',d])$, and $\delta (d',d) \le {\mathcal {Y}_{}^{}}$.

$\psi$ is fulfilled in $({\mathbf L},d)$ if and only if there is $d'$ such that $\psi$ is fulfilled in $({\mathbf L},d)$ by $d'$.

For $\psi \in {\forall \text {-}\mathsf {REQ}^{{\mathbf L}}} (d)$, we say that $\psi$ is fulfilled in $(\mathbf L,d)$ if, and only if, one of the following holds:

• $\psi = [ A ]\psi '$ for some $\psi '$ and $\psi ' \in \mathcal L([d,d'])$ for every $d' \in {\mathbb {D}} ^{> d}$,

• $\psi = [ \overline{A} ]\psi '$ for some $\psi '$ and $\psi ' \in \mathcal L([d',d])$ for every $d' \in {\mathbb {D}} ^{< d}$,

• $\psi = {{ [ A_{y} ]}} \psi '$ for some $\psi '$ and $\psi ' \in \mathcal L([d,d'])$ for every $d' \in {\mathbb {D}} ^{> d}$ with $\delta (d,d') \le {\mathcal {Y}_{}^{}}$,

• $\psi = {{ [ \overline{A}_{y} ]}} \psi '$ for some $\psi '$ and $\psi ' \in \mathcal L([d',d])$ for every $d' \in {\mathbb {D}} ^{< d}$ with $\delta (d',d) \le {\mathcal {Y}_{}^{}}$,

• $\psi = neg({{ \langle A_{x} \rangle }} \psi ')$ for some $\psi '$ and $neg(\psi ') \in \mathcal L([d,d'])$ for every $d' \in {\mathbb {D}} ^{> d}$ with $\delta (d,d') \le {\mathcal {X}_{}^{}}$,

• $\psi = neg({{ \langle \overline{A}_{x} \rangle }} \psi ')$ for some $\psi '$ and $neg(\psi ') \in \mathcal L([d',d])$ for every $d' \in {\mathbb {D}} ^{> d}$ with $\delta (d',d) \le {\mathcal {X}_{}^{}}$.

d is $\exists$ -fulfilled in $\mathbf L$ if, and only if, every $\psi \in {\exists \text {-}\mathsf {REQ}^{{\mathbf L}}} (d)$ is fulfilled; d is $\forall$ -fulfilled in $\mathbf L$ if, and only if, every $\psi \in {\forall \text {-}\mathsf {REQ}^{{\mathbf L}}} (d)$ is fulfilled; d is fulfilled in $\mathbf L$ if, and only if, it is both $\exists$- and $\forall$-fulfilled in $\mathbf L$.

An existentially fulfilling (resp., universally fulfilling, fulfilling) $\text {pLIS}_\varphi$, aka $\exists \texttt {-}\text {pLIS}^{}_\varphi$ (resp., $\forall \texttt {-}\text {pLIS}^{}_\varphi$, $\exists \forall \texttt {-}\text {pLIS}^{}_\varphi$), is a ${\text {pLIS}_\varphi }$ ${\mathbf L}$ such that every $d \in {\mathbb {D}} _{\mathbf L}$ is $\exists$-fulfilled (resp., $\forall$-fulfilled, fulfilled) in it.

Proposition 2

$\varphi$ is satisfiable if and only if there exists a $\exists \forall \texttt {-}\text {pLIS}^{}_\varphi$, and it is finitely satisfiable if and only if there exists a finite $\exists \forall \texttt {-}\text {pLIS}^{}_\varphi$.

Before showing the decidability of , we prove a result that will later come in handy. A set of requests ${\mathsf {REQ}^{{\mathbf L}}} (d)$ (for a $\text {pLIS}_\varphi$ $\mathbf L$ and $d \in {\mathbb {D}} _{\mathbf L}$) is consistent if for each $\psi \in {\mathsf {REQ}^{{\mathbf L}}} (d)$, we have that $neg(\psi ) \notin {\mathsf {REQ}^{{\mathbf L}}} (d)$; otherwise, it is inconsistent.

Proposition 3

Let $\mathbf L$ be a $\text {pLIS}_\varphi$ and $d \in {\mathbb {D}} _{\mathbf L}$. The following properties hold, unless ${\mathsf {REQ}^{{\mathbf L}}} (d)$ is inconsistent:

• if ${\mathbb {D}} ^{< d} \ne \emptyset$, then ${\mathsf {f\text {-}REQ}^{{\mathbf L}}} (d) = \mathcal L_{\mathbf L} (d',d) \cap { TR _{f}(\varphi )}$, for any given $d' \in {\mathbb {D}} ^{< d}$, unless ${\mathsf {f\text {-}REQ}^{{\mathbf L}}} (d)$ is inconsistent;

• if ${\mathbb {D}} ^{> d} \ne \emptyset$, then ${\mathsf {p\text {-}REQ}^{{\mathbf L}}} (d) = \mathcal L_{\mathbf L} (d,d') \cap { TR _{p}(\varphi )}$, for any given $d' \in {\mathbb {D}} ^{> d}$, unless ${\mathsf {p\text {-}REQ}^{{\mathbf L}}} (d)$ is inconsistent.

4.2 A Bounded Witness for Non-finitely Satisfiable Formulas

Let ${\mathbf L}$ be a ${\text {pLIS}_\varphi }$ and $d \in {\mathbb {D}} _{\mathbf L}$. A set of essentials of d (in $\mathbf L$) is any minimal (with respect to set inclusion) set $E \subseteq {\mathbb {D}} _{\mathbf L}$ such that for every $\psi \in {\exists \text {-}\mathsf {REQ}^{{\mathbf L}}} (d)$ there is $d' \in E$ for which $\psi$ is fulfilled in $({\mathbf L}, d)$ by $d'$. We denote by $\mathcal {E}_{{\mathbf L}}(d)$ the class containing all sets of essentials of d in $\mathbf L$, i.e., ${\mathcal {E}_{{\mathbf L}}(d)} = {\{ E \subseteq {\mathbb {D}} _{\mathbf L} \mid E \text { is a set of essentials of } d \text { in } {\mathbf L} \}}$. Intuitively, a set of essentials of d is a collection of points that jointly make d $\exists$-fulfilled in $\mathbf L$. Clearly ${\mathcal {E}_{{\mathbf L}}(d)} \ne \emptyset$ if and only if d is $\exists$-fulfilled in $\mathbf L$. We lift this concept to a higher order: a set of essentials of essentials (or 2nd-order essentials) of d (in $\mathbf L$) is any minimal (with respect to set inclusion) set $E_2 \subseteq {\mathbb {D}} _{\mathbf L}$ such that (i) $E_1 \subseteq E_2$ for some $E_1 \in {\mathcal {E}_{{\mathbf L}}(d)}$ and (ii) for every $d' \in E_1$ there is $E_{d'} \in {\mathcal {E}_{{\mathbf L}}(d')}$ for which $E_{d'} \subseteq E_2$. We denote by $\mathcal {E}^2_{{\mathbf L}}(d)$ the class containing all sets of 2nd-order essentials of d in $\mathbf L$, i.e., ${\mathcal {E}^2_{{\mathbf L}}(d)} = {\{ E \subseteq {\mathbb {D}} _{\mathbf L} \mid E \text { is a set of 2nd-order essentials of } d \text { in } {\mathbf L} \}}$.

Definition 1

(representative). Let $\mathbf L$ be a finite $\text {pLIS}_\varphi$ and $d \in {\mathbb {D}} _{\mathbf L}$.

If $d \notin {\{ \min {\mathbb {D}} _{\mathbf L}, \max {\mathbb {D}} _{\mathbf L} \}}$, then a representative of d in $\mathbf L$ is a point $e \in {\mathbb {D}} _{\mathbf L}$ such that ${\mathsf {REQ}^{{\mathbf L}}} (d) = {\mathsf {REQ}^{{\mathbf L}}} (e)$, e is fulfilled in $\mathbf L$, and so are points in $E_2$, for some $E_2 \in {\mathcal {E}^2_{{\mathbf L}}(e)}$ with $E_2 \cap {\{ \min {\mathbb {D}}, \max {\mathbb {D}} \}} = \emptyset$.

If $d = \min {\mathbb {D}} _{\mathbf L}$ (resp., $d = \max {\mathbb {D}} _{\mathbf L}$), then a representative of d in $\mathbf L$ is a point $e \in {\mathbb {D}} _{\mathbf L}$ that is a representative of $d'$ in $\mathbf L$ for some $d' \in {\mathbb {D}} _{\mathbf L}$, with ${\mathsf {p\text {-}REQ}^{{\mathbf L}}} (d') = {\mathsf {p\text {-}REQ}^{{\mathbf L}}} (d)$ (resp., ${\mathsf {f\text {-}REQ}^{{\mathbf L}}} (d') = {\mathsf {f\text {-}REQ}^{{\mathbf L}}} (d)$).

A convex subset of a domain $\mathbb {D}$ is a subset $\mathbb {D'}$ of $\mathbb {D}$ such that for every $d',d'' \in {\mathbb {D'}}$ and $d \in {\mathbb {D}}$, if $d'< d < d''$, then $d \in {\mathbb {D'}}$. A right-convex (resp., left-convex) subset of a domain $\mathbb {D}$ is a convex subset $\mathbb {D'}$ of $\mathbb {D}$ such that $\max {\mathbb {D}} \in {\mathbb {D'}}$ (resp., $\min {\mathbb {D}} \in {\mathbb {D'}}$).

Given a ${\text {pLIS}_\varphi }$ $\mathbf L$ and ${\mathbb {D'}} \subseteq {\mathbb {D}} _{\mathbf L}$, we let ${\mathsf {request\text {-}sets}^{{\mathbf L}}({\mathbb {D'}})} = \{ \mathcal {R}\mid {\mathsf {REQ}^{{\mathbf L}}} (d) = \mathcal {R}\text { for some } d \in {\mathbb {D'}} \}$.

Definition 2

(left- and right-periodic ${\mathbf {pLIS}_{\varphi }}$ ). Let $\mathbf L$ be a finite $\text {pLIS}_\varphi$. A left-period for $\mathbf L$ is a left-convex subset $\mathbb {E}$ of ${\mathbb {D}} _{\mathbf L}$ such that, for every $d \in {\mathbb {E}}$, if d is not fulfilled in $\mathbf L$ or $d = \min {\mathbb {E}}$, then there is $d' \in {\mathbb {E}} ^{> d}$ for which the following holds:

• (a) $d'$ is a representative of d in $\mathbf L$;

• (b) ${\mathsf {request\text {-}sets}^{{\mathbf L}}({\mathbb {E}} \setminus {\{ \min {\mathbb {E}} \}})}$ is equal to ${\mathsf {request\text {-}sets}^{{\mathbf L}}({\mathbb {E}} ^{< d'} \setminus {\{ \min {\mathbb {E}} \}})}$, which is equal to ${\mathsf {request\text {-}sets}^{{\mathbf L}}({\mathbb {E}} ^{> d'})}$, and there are $d'' \in {\mathbb {E}} ^{< d'} \setminus {\{ \min {\mathbb {E}} \}}$ and $d''' \in {\mathbb {E}} ^{> d'}$ such that ${\mathsf {p\text {-}REQ}^{{\mathbf L}}} (\min {\mathbb {E}}) = {\mathsf {p\text {-}REQ}^{{\mathbf L}}} (d'') = {\mathsf {p\text {-}REQ}^{{\mathbf L}}} (d''')$;

• (c) every ${{ \langle A_{x} \rangle }} \psi \in {\mathsf {f\text {-}REQ}^{{\mathbf L}}} (d')$ is fulfilled in $({\mathbf L},d')$ by a point belonging to $\mathbb {E}$.

A right-period for $\mathbf L$ is defined symmetrically.

$\mathbf L$ is periodic if, and only if, there exist both a left- and a right-period for it.

Definition 3

( $\varphi$ -witness). A $\varphi$ -witness is a finite, periodic ${\forall \texttt {-}\text {pLIS}^{}_\varphi }$ $\mathbf L$, such that every $d \in {\mathbb {D}} _{{\mathbf L}} \setminus ({\mathbb {E}} \cup {\mathbb {F}})$ is fulfilled in $\mathbf L$, where $\mathbb {E}$ and $\mathbb {F}$ are, respectively, a left- and a right-period for $\mathbf L$, with ${\mathbb {E}} \cap {\mathbb {F}} = \emptyset$ and ${\mathbb {D}} _{{\mathbf L}} \setminus ({\mathbb {E}} \cup {\mathbb {F}}) \ne \emptyset$.

Lemma 9

An infinite $\exists \forall \texttt {-}\text {pLIS}^{}_\varphi$ $\mathbf L = \langle \mathbb D, \mathcal L, \delta , {\mathcal {X}_{}^{}}, {\mathcal {Y}_{}^{}} \rangle$ exists if and only if a $\varphi$-witness $\mathbf L' = \langle \mathbb D', \mathcal L', \delta ', {\mathcal {X'}_{}^{}}, {\mathcal {Y'}_{}^{}} \rangle$ exists.

Thanks to the previous lemma, we can reduce the search for an infinite model for a formula to the search for a finite witness. However, since such a finite witness can be arbitrarily large, the search space is still infinite. In what follows, we provide a bound on the size of the finite witness, thus obtaining a finite search space. Decidability of immediately follows.

Let ${\mathcal {B}_{\varphi }} = | {\mathsf {REQ}_\varphi } | \cdot (2 \cdot |\mathcal {C} l (\varphi )|^2 + 2 \cdot |\mathcal {C} l (\varphi )|) + |{\mathsf {REQ}_\varphi } | \cdot |\mathcal {C} l (\varphi )| + |\mathcal {C} l (\varphi )|$.

Lemma 10

Let ${\mathbf L} = \langle {\mathbb {D}}, \mathcal L, \delta , {\mathcal {X}_{}^{}}, {\mathcal {Y}_{}^{}} \rangle$ be a $\varphi$-witness, $\mathbb {E}$ and $\mathbb {F}$ being, respectively, a left- and a right-period for it. If $|{\mathbb {E}} | > {\mathcal {B}_{\varphi }}$ (resp., $|{\mathbb {F}} | > {\mathcal {B}_{\varphi }}$, $|{\mathbb {D}} \setminus ({\mathbb {E}} \cup {\mathbb {F}})| > {\mathcal {B}_{\varphi }}$), then there is a $\varphi$-witness ${\mathbf L'} = \langle {\mathbb {D'}}, \mathcal L', \delta ', {\mathcal {X}_{}^{}} ', {\mathcal {Y}_{}^{}} ' \rangle$ with $|{\mathbb {D'}} | = |{\mathbb {D}} | - 1$.

The size of a ${\text {pLIS}_\varphi }$ $\mathbf L$ is the size of the underlying domain $\mathbb D_{\mathbf L}$. The following corollary immediately follows from the above lemma.

Corollary 1

(small model property). A $\varphi$-witness exists if and only if there is one of size at most $3 \cdot {\mathcal {B}_{\varphi }} \le 3 \cdot [2^{2 \cdot | \varphi | + 2} \cdot (2 \cdot (2 \cdot | \varphi | + 2)^2 + 2 \cdot (2 \cdot | \varphi | + 2)) + 2^{2 \cdot | \varphi | + 2} \cdot (2 \cdot | \varphi | + 2) + (2 \cdot | \varphi | + 2)]$.

Theorem 3

The satisfiability problem for is NEXPTIME-complete.

5 Conclusions

In this paper, we have studied the problem of enriching the well-known propositional logic of temporal neighborhood PNL with support for prompt-liveness specifications. We first proved that the logic obtained from PNL by introducing “prompt” versions of its modalities with no restriction on the use of bounding variables, that we call PROMPT- PNL, is undecidable. Then, we showed that decidability can be recovered by introducing a partition of bounding variables into two classes, one for the existential modalities, the other for the universal ones. The satisfiability problem for the resulting logic, named , is indeed NEXPTIME-complete.

The work done can be further developed in various directions.

First, we are interested in identifying the minimum number of bounding variables that suffice to make PROMPT- PNL undecidable. We believe it possible to prove that when the set of variables is small enough, e.g., when it includes two bounding variables only, the logic is still expressive enough to capture some meaningful promptness conditions and remains decidable.

We also aim at investigating the more powerful setting of parametric extensions of PNL. Parametric PNL can be viewed as a natural generalization of PROMPT- PNL, as parametric modalities allow one to express both lower and upper bounds on the delay with which a request is fulfilled (PROMPT- PNL only copes with the latter).

Last but not least, we are interested in comparing the expressiveness of the logics PROMPT- PNL and with that of metric PNL , that is, the metric extension of PNL introduced and systematically studied in [7].