Generalizing Non-punctuality for Timed Temporal Logic with Freeze Quantifiers

Abstract

Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are prominent real-time extensions of Linear Temporal Logic (LTL). In general, the satisfiability checking problem for these extensions is undecidable when both the future U and the past S modalities are used. In a classical result, the satisfiability checking for MITL[U,S], a non-punctual fragment of MTL[U,S], is shown to be decidable with EXPSPACE complete complexity. Given that this notion of non-punctuality does not recover decidability in the case of TPTL[U,S], we propose a generalization of non-punctuality called non-adjacency for TPTL[U,S], and focus on its 1-variable fragment, 1-TPTL[U,S]. While non-adjacent 1-TPTL[U,S] appears to be a very small fragment, it is strictly more expressive than MITL. As our main result, we show that the satisfiability checking problem for non-adjacent 1-TPTL[U,S] is decidable with EXPSPACE complete complexity.

This work is partially supported by the European Research Council through the SENTIENT project (ERC-2017-STG #755953).

1 Introduction

Metric Temporal Logic ($\mathsf {MTL}$) and Timed Propositional Temporal Logic ($\mathsf {TPTL}$) are natural extensions of Linear Temporal Logic ($\mathsf {LTL}$) for specifying real-time properties [3]. $\mathsf {MTL}$ extends the $\mathsf {U}$ and $\mathsf {S}$ modalities of $\mathsf {LTL}$ by associating a timing interval with these. $a \mathsf {U}_I b$ describes behaviours modeled as timed words consisting of a sequence of a’s followed by a b which occurs at a time within (relative) interval I. On the other hand, $\mathsf {TPTL}$ uses freeze quantification to store the current time stamp. A Freeze quantifier with clock variable x has the form $x.\varphi$. When it is evaluated at a point i on a timed word, the time stamp $\tau _i$ at i is frozen in x, and the formula $\varphi$ is evaluated using this value for x. Variable x is used in $\varphi$ in a constraint of the form $T-x \in I$; this constraint, when evaluated at a point j, checks if $\tau _j -\tau _i \in I$, where $\tau _j$ is the time stamp at point j.

For example, the formula $\mathsf {F}x.(a\wedge \mathsf {F}(b \wedge T-x \in [1,2] \wedge \mathsf {F}(c \wedge T-x \in [1,2])))$¹ asserts that there is a point in future where a holds and in its future within interval [1, 2], b and c occur, and the former occurs before the latter. This property is not expressible in $\mathsf {MTL}[\mathsf {U},\mathsf {S}]$ [4, 18]. Moreover, every property in $\mathsf {MTL}[\mathsf {U},\mathsf {S}]$ can be expressed in 1-$\mathsf {TPTL}[\mathsf {U},\mathsf {S}]$. Thus, 1-$\mathsf {TPTL}[\mathsf {U},\mathsf {S}]$ is strictly more expressive than $\mathsf {MTL}[\mathsf {U},\mathsf {S}]$. Unfortunately, both the logics have an undecidable satisfiability problem, making automated analysis for these logics theoretically impossible.

Exploring natural decidable variants of these logics has been an active area of research since the advent of these logics [2, 8,9,10, 21,22,23]. One line of work restricted itself to the future only fragments $\mathsf {MTL}[\mathsf {U}]$ and 1-$\mathsf {TPTL}[\mathsf {U}]$ which have both been shown to have decidable satisfiability over finite timed words, under a pointwise interpretation [7, 17]. The complexity however is non-primitive recursive. Reducing the complexity to elementary has been challenging. One of the most celebrated of such logics is the Metric Interval Temporal Logic ($\mathsf {MITL}[\mathsf {U},\mathsf {S}]$) [1], a subclass of $\mathsf {MTL}[\mathsf {U},\mathsf {S}]$ where the timing intervals are restricted to be non-punctual (i.e. intervals of the form $\langle x, y \rangle$ where $x < y$). The satisfiability checking for $\mathsf {MITL}$ formulae is decidable with EXPSPACE complete complexity [1]. While non-punctuality helps to recover the decidability of $\mathsf {MTL}[\mathsf {U},\mathsf {S}]$, it does not help $\mathsf {TPTL}[\mathsf {U},\mathsf {S}]$. The freeze quantifiers of $\mathsf {TPTL}$ enables us to trivially express punctual timing constraints using only the non-punctual intervals: for instance the 1-$\mathsf {TPTL}$ formula $x.(a \mathsf {U}(a \wedge T-x \in [1, \infty ) \wedge T-x \in [0, 1]))$ uses only non-punctual intervals but captures the $\mathsf {MTL}$ formula $a \mathsf {U}_{[1,1]} b$. Thus, a more refined notion of non-punctuality is needed to recover the decidability of 1-$\mathsf {TPTL}[\mathsf {U},\mathsf {S}]$.

Contributions. With the above observations, to obtain a decidable class of 1-$\mathsf {TPTL}[\mathsf {U},\mathsf {S}]$ akin to $\mathsf {MITL}[\mathsf {U},\mathsf {S}]$, we revisit the notion of non-punctuality as it stands currently. As our first contribution, we propose non-adjacency, a refined version of non-punctuality. Two intervals, $I_1$ and $I_2$ are non-adjacent if the supremum of $I_1$ is not equal to the infimum of $I_2$. Non-adjacent 1-$\mathsf {TPTL}[\mathsf {U},\mathsf {S}]$ is the subclass of 1-$\mathsf {TPTL}[\mathsf {U},\mathsf {S}]$ where, every interval used in clock constraints within the same freeze quantifier is non-adjacent to itself and to every other timing interval that appears within the same scope. (Wlog, we consider formulae in negation normal form only.) The non-adjacency restriction disallows punctual timing intervals: every punctual timing interval is adjacent to itself. It can be shown (Theorem 2) that non-adjacent 1-$\mathsf {TPTL}[\mathsf {U},\mathsf {S}]$, while seemingly very restrictive, is strictly more expressive than $\mathsf {MITL}$ and it can also express the counting and the Pnueli modalities [9]. Thus, the logic is of considerable interest in practical real-time specification. See the full version for an example.

Our second contribution is to give a decision procedure for the satisfiability checking of non-adjacent 1-$\mathsf {TPTL}[\mathsf {U},\mathsf {S}]$. We do this in two steps. 1) We introduce a logic $\mathsf {PnEMTL}$ which combines and generalises the automata modalities of [11, 22, 23] and the Pnueli modalities of [9, 10, 21], and has not been studied before to the best of our knowledge. We show that a formula of non-adjacent 1-$\mathsf {TPTL}[\mathsf {U},\mathsf {S}]$ can be reduced to an equivalent formula of non-adjacent $\mathsf {PnEMTL}$ (Theorem 5). 2) We prove that the satisfiability of non-adjacent $\mathsf {PnEMTL}$ is decidable with EXPSPACE complete complexity (Theorem 6). For brevity, some of the proof details are omitted here and can be found in the full version [13].

Related Work and Discussion. Much of the related work has already been discussed. $\mathsf {MITL}$ with counting and Pnueli modalities has been shown to have EXPSPACE-complete satisfiability [20, 21]. Here, we tackle even more expressive logics: namely non-adjacent 1-$\mathsf {TPTL}[\mathsf {U},\mathsf {S}]$ and non-adjacent $\mathsf {PnEMTL}$. We show that EXPSPACE-completeness of satisfiability checking is retained in spite of the additional expressive power. These decidability results are proved by equisatisfiable reductions to logic $\mathsf {EMITL}_{0,\infty }$ of Ho [11]. As argued by Ho, it is quite practicable to extend the existing model checking tools like UPPAAL to logic $\mathsf {EMITL}_{0,\infty }$ and hence to our logics too.

Addition of regular expression based modalities to untimed logics like LTL has been found to be quite useful for practical specification; even the IEEE standard temporal logic PSL has this feature. With a similar motivation, there has been considerable recent work on adding regular expression/automata based modalities to $\mathsf {MTL}$ and $\mathsf {MITL}$. Raskin as well as Wilke added automata modalities to $\mathsf {MITL}$ as well as an Event-Clock logic ECL [22, 23] and showed the decidability of satisfaction. The current authors showed that $\mathsf {MTL}[\mathsf {U},\mathsf {S}_{NP}]$ (where $\mathsf {U}$ can use punctual intervals but $\mathsf {S}$ is restricted to non-punctual intervals), when extended with counting as well as regular expression modalities preserves decidability of satisfaction [12, 14,15,16]. Recently, Ferrère showed the EXPSPACE decidability of MIDL which is $\mathsf {LTL}[\mathsf {U}]$ extended with a fragment of timed regular expression modality [5]. Moreover, Ho has investigated a PSPACE-complete fragment $\mathsf {EMITL}_{0,\infty }$ [11]. Our non-adjacent $\mathsf {PnEMTL}$ is a novel extension of MITL with modalities which combine the features of EMITL [11, 22, 23] and the Pnueli modalities [9, 10, 21].

2 Preliminaries

Let $\varSigma$ be a finite set of propositions, and let $\varGamma = 2^{\varSigma } \setminus \emptyset$. A word over $\varSigma$ is a finite sequence $\sigma = \sigma _1 \sigma _2 \ldots \sigma _n$, where $\sigma _i \in \varGamma$. A timed word $\rho$ over $\varSigma$ is a finite sequence of pairs $(\sigma , \tau ) \in \varSigma \times \mathbb {R}_{\ge 0}$; $\rho = (\sigma _1, \tau _1) \ldots (\sigma _n, \tau _n) \in (\varSigma \times \mathbb {R}_{\ge 0})^*$ where $\tau _1=0$ and $\tau _i \le \tau _j$ for all $1 \le i \le j \le n$. The $\tau _i$ are called time stamps. For a timed or untimed word $\rho$, let $dom(\rho ) = \{i | 1 \le i \le |\rho |\}$ where $|\rho |$ denotes the number of (event, timestamp) pairs composing the word $\rho$, and $\sigma [i]$ denotes the symbol at position $i \in dom(\rho )$. The set of timed words over $\varSigma$ is denoted $T\varSigma ^*$. Given a (timed) word $\rho$ and $i \in dom(\rho )$, a pointed (timed) word is the pair $\rho , i$. Let $\mathcal {I}_\mathsf {int}$ ($\mathcal {I}_\mathsf {nat}$) be the set of open, half-open or closed time intervals, such that the end points of these intervals are in $\mathbb {Z}\cup \{-\infty ,\infty \}$ ($\mathbb {N} \cup \{0,\infty \}$, respectively). We assume familiarity with $\mathsf {LTL}$.

Metric Temporal Logic ($\mathsf {MTL}$). $\mathsf {MTL}$ is a real-time extension of $\mathsf {LTL}$ where the modalities ($\mathsf {U}$ and $\mathsf {S}$) are guarded with intervals. Formulae of $\mathsf {MTL}$ are built from $\varSigma$ using Boolean connectives and time constrained versions $\mathsf {U}_I$ and $\mathsf {S}_I$ of the standard $\mathsf {U},\mathsf {S}$ modalities, where $I \in \mathcal {I}_\mathsf {nat}$. Intervals of the form [x, x] are called punctual; a non-punctual interval is one which is not punctual. Formulae in $\mathsf {MTL}$ are defined as follows. $\varphi :\,\!:=a ~|\top ~|\varphi \wedge \varphi ~|~\lnot \varphi ~| ~\varphi \mathsf {U}_I \varphi ~|~ \varphi \mathsf {S}_I \varphi$, where $a \in \varSigma$ and $I \in \mathcal {I}_\mathsf {nat}$. For a timed word $\rho = (\sigma _1, \tau _1 ) (\sigma _2, \tau _2) \ldots (\sigma _n, \tau _n) \in T\varSigma ^*$, a position $i \in dom(\rho )$, an $\mathsf {MTL}$ formula $\varphi$, the satisfaction of $\varphi$ at a position i of $\rho$, denoted $\rho , i \models \varphi$, is defined below. We discuss the time constrained modalities.

• $\rho ,i\ \models \ \varphi _{1} \mathsf {U}_{I} \varphi _{2}$ iff $\exists j > i$, $\rho ,j\ \models \ \varphi _{2}, \tau _{j} - \tau _{i} \in I$, and $\rho ,k\ \models \ \varphi _{1}\forall i< k <j$,

• $\rho ,i\ \models \ \varphi _{1} \mathsf {S}_{I} \varphi _{2}$ iff $\exists j < i$, $\rho ,j\ \models \ \varphi _{2}, \tau _{j} - \tau _{i} \in I$, and $\rho ,k\ \models \ \varphi _{1}\forall j< k <i$.

The language of an $\mathsf {MTL}$ formula $\varphi$ is defined as $L(\varphi ) = \{\rho | \rho , 1 \models \varphi \}$. Using the above, we obtain some derived formulae: the constrained eventual operator $\mathsf {F}_I \varphi \equiv true \mathsf {U}_I \varphi$ and its dual is $\mathcal {G}_I \varphi \equiv \lnot \mathsf {F}_I \lnot \varphi$. Similarly $\mathcal {H}_I \varphi \equiv true \mathsf {S}_I \varphi$. The next operator is defined as $\oplus _I \varphi \equiv \bot \mathsf {U}_I \varphi$. The non-strict versions of $\mathsf {F}, \mathcal {G}$ are respectively denoted $\mathsf {F}^w$ and $\mathcal {G}^w$ and include the present point. Symmetric non-strict versions for past operators are also allowed. The subclass of $\mathsf {MTL}$ obtained by restricting the intervals I in the until and since modalities to non-punctual intervals is denoted $\mathsf {MITL}$. We say that a formula $\varphi$ is satisfiable iff $L(\varphi )\ne \emptyset$.

Theorem 1

Satisfiability checking for $\mathsf {MTL}[\mathsf {U},\mathsf {S}]$ is undecidable [2]. Satisfiability Checking for $\mathsf {MITL}$ is EXPSPACE-complete [1].

Time Propositional Temporal Logic ($\mathsf {TPTL}$). The logic $\mathsf {TPTL}$ also extends $\mathsf {LTL}$ using freeze quantifiers. Like $\mathsf {MTL}$, $\mathsf {TPTL}$ is also evaluated on timed words. Formulae of $\mathsf {TPTL}$ are built from $\varSigma$ using Boolean connectives, modalities $\mathsf {U}$ and $\mathsf {S}$ of $\mathsf {LTL}$. In addition, $\mathsf {TPTL}$ uses a finite set of real valued clock variables $X = \{x_1,\ldots ,x_n\}$. Let $\nu : X \rightarrow \mathbb {R}_{\ge 0}$ represent a valuation assigning a non-negative real value to each clock variable. The formulae of $\mathsf {TPTL}$ are defined as follows. Without loss of generality we work with $\mathsf {TPTL}$ in the negation normal form. $\varphi :\,\!:=a~|~\lnot a ~|\top ~|~\bot ~|~ x.\varphi ~|~ T-x \in I ~|~x-T \in I~|~\varphi \wedge \varphi ~|~ \varphi \vee \varphi ~| ~\varphi \mathsf {U}\varphi ~|~ \varphi \mathsf {S}\varphi ~|~ \mathcal {G}\varphi ~|~ \mathcal {H}\varphi$, where $x \in X$, $a \in \varSigma$, $I \in \mathcal {I}_\mathsf {int}$. Here T denotes the time stamp of the point where the formula is being evaluated. $x. \varphi$ is the freeze quantification construct which remembers the time stamp of the current point in variable x and evaluates $\varphi$.

For a timed word $\rho =(\sigma _1,\tau _1)\dots (\sigma _n,\tau _n)$, $i \in dom(\rho )$ and a $\mathsf {TPTL}$ formula $\varphi$, we define the satisfiability relation, $\rho , i, \nu \models \varphi$ with valuation $\nu$ of all the clock variables. We omit the semantics of Boolean, $\mathsf {U}$ and $\mathsf {S}$ operators as they are similar to those of $\mathsf {LTL}$.

• $\rho , i, \nu \models a$ iff $a \in \sigma _{i}$, and $\rho ,i,\nu \models x.\varphi$ iff $\rho ,i,\nu [x \leftarrow \tau _i] \models \varphi$

• $\rho ,i,\nu \models T-x\ \in I$ iff $\tau _i - \nu (x) \in I$, and $\rho ,i,\nu \models x-T \in I$ iff $\nu (x) - \tau _i \in I$

• $\rho ,i,\nu \ \models \ \mathcal {G}\varphi$ iff $\forall j > i$, $\rho ,j,\nu \ \models \ \varphi$, and

• $\rho ,i,\nu \ \models \ \mathcal {H}\varphi$ iff $\forall j < i$, $\rho ,j,\nu \ \models \ \varphi$

Let $\overline{0}=(0,0,\dots ,0)$ represent the initial valuation of all clock variables. For a timed word $\rho$ and $i \in dom(\rho )$, we say that $\rho , i$ satisfies $\varphi$ denoted $\rho , i \models \varphi$ iff $\rho ,i,\overline{0}\models \varphi$. The language of $\varphi$, $L(\varphi ) = \{\rho | \rho , 1 \models \varphi \}$. The Pointed Language of $\varphi$ is defined as $L_{pt}(\varphi ) = \{\rho ,i | \rho , i \models \varphi \}$. Subclass of $\mathsf {TPTL}$ that uses only 1 clock variable (i.e. $|X| = 1$) is known as 1-$\mathsf {TPTL}$. The satisfiability checking for 1-$\mathsf {TPTL}[\mathsf {U}, \mathsf {S}]$ is undecidable, which is implied by Theorem 1 and the fact that 1-$\mathsf {TPTL}[\mathsf {U}, \mathsf {S}]$ trivially generalizes $\mathsf {MTL}[\mathsf {U},\mathsf {S}]$. As an example, the formula $\varphi =x.(a \mathsf {U}(b \mathsf {U}(c \wedge T-x \in [1,2])))$ is satisfied by the timed word $\rho =(a,0)(a,0.2)(b,1.1)(b,1.9)(c,1.91)(c,2.1)$ since $\rho , 1 \models \varphi$. The word $\rho '=(a,0)(a,0.3)(b,1.4)(c,2.1)(c,2.5)$ does not satisfy $\varphi$. However, $\rho ',2 \models \varphi$: if we start from the second position of $\rho '$, we assign $\nu (x)=0.3$, and when we reach the position 4 of $\rho '$ with $\tau _4=2.1$ we obtain $T-x=2.1-0.3 \in [1,2]$.

3 Introducing Non-adjacent 1-$\mathsf {TPTL}$ and $\mathsf {PnEMTL}$

In this section, we define non-adjacent 1-$\mathsf {TPTL}$ and $\mathsf {PnEMTL}$ logics. Let x denote the unique freeze variable we use in 1-$\mathsf {TPTL}$.

Non-Adjacent 1-$\mathsf {TPTL}$ is defined as a subclass of 1-$\mathsf {TPTL}$ where adjacent intervals within the scope of any freeze quantifier is disallowed. Two intervals $I_1, I_2 \in \mathcal {I}_\mathsf {int}$ are non-adjacent iff $\sup (I_1) = \inf (I_2) \Rightarrow \sup (I_1) = 0$. A set $\mathcal {I}_{na}$ of intervals is non-adjacent iff any two intervals in $\mathcal {I}_{na}$ are non-adjacent. It does not contain punctual intervals other than [0, 0] as every punctual interval is adjacent to itself. For example, the set $\{[1,2), (2,3], [5,6)\}$ is not a non-adjacent set, while $\{[0,0], [0,1), (3,4], [5,6)\}$ is. Let $\mathcal {I}_{na}$ denote a set of non-adjacent intervals with end points in $\mathbb {Z} \cup \{-\infty ,\infty \}$. See full version for an example specification using this logic. The freeze depth of a $\mathsf {TPTL}$ formula $\varphi$, $\mathsf {fd}(\varphi )$ is defined inductively. For a ptopositional formula prop, $\mathsf {fd}(prop)=0$. Also, $\mathsf {fd}(x.\varphi )=\mathsf {fd}(\varphi )+1$, and $\mathsf {fd}(\varphi _1 \mathsf {U}\varphi _2)=\mathsf {fd}(\varphi _1 \mathsf {S}\varphi _2) =\mathsf {fd}(\varphi _1 \wedge \varphi _2)=\mathsf {fd}(\varphi _1 \vee \varphi _2)=\mathsf {Max(\mathsf {fd}(\varphi _1),\mathsf {fd}(\varphi _2))}, \mathsf {fd}(\mathcal {G}(\varphi ))=\mathsf {fd}(\mathcal {H}(\varphi ))=\mathsf {fd}(\varphi )$.

Theorem 2

Non-Adjacent 1-$\mathsf {TPTL}[\mathsf {U},\mathsf {S}]$ is more expressive than $\mathsf {MITL}[\mathsf {U}, \mathsf {S}]$. It can also express the Counting and the Pnueli modalities of [9, 10].

The straightforward translation of MITL into TPTL in fact gives rise to non-adjacent 1-TPTL formula. Let $\widehat{I}$ abbreviate $T-x \in I$. E.g. MITL formula $a \mathsf {U}_{[2,3]} (b \mathsf {U}_{[3,4]} c)$ translates to $x.(a \mathsf {U}(\widehat{[2,3]} \wedge x.(b \mathsf {U}(\widehat{[3,4]} \wedge c)))$. It has been previously shown that $\mathsf {F}[x.(a \wedge \mathsf {F}(b \wedge \widehat{(1,2)} \wedge \mathsf {F}(c \wedge \widehat{(1,2)})))]$, which is in fact a formula of non-adjacent 1-TPTL, is inexpressible in $\mathsf {MTL}[\mathsf {U},\mathsf {S}]$ [18]. The Pnueli modality $\mathsf {Pn}_I(\phi _1, \ldots , \phi _k)$ expresses that there exist positions $i_1 \le \ldots \le i_k$ within (relative) interval I where each $i_j$ satisfies $\phi _j$. This is equivalent to the non-adjacent 1-TPTL formula $x. (\mathsf {F}(\hat{I} \wedge \phi _1 \wedge \mathsf {F}(\hat{I} \wedge \phi _2 \wedge \mathsf {F}( \ldots ))))$. Similarly the (simpler) counting modality can also be expressed.

Pnueli $\mathsf {EMTL}$: There have been several attempts to extend logic $\mathsf {MTL}[\mathsf {U}]$ with regular expression/automaton modalities [5, 11, 14, 23]. We use a generalization of these existing modalities to give the logic $\mathsf {PnEMTL}$. For any finite automaton A, let L(A) denote the language of A.

Given a finite alphabet $\varSigma$, formulae of $\mathsf {PnEMTL}$ have the following syntax:

$\varphi :\,\!:=a~|\varphi \wedge \varphi ~|~\lnot \varphi ~| \mathcal {F}^k_{I_1,\ldots ,I_k} (\mathsf {A}_1,\ldots , \mathsf {A}_{k+1})(S)~|~ \mathcal {P}^k_{I_1,\ldots ,I_k} (\mathsf {A}_1,\ldots ,\mathsf {A}_{k+1})(S)$ where $a \in \varSigma$, $I_1, I_2, \ldots I_k \in \mathcal {I}_\mathsf {nat}$ and $\mathsf {A}_1, \ldots \mathsf {A}_{k+1}$ are automata over $2^S$ where S is a set of formulae from $\mathsf {PnEMTL}$. $\mathcal {F}^k$ and $\mathcal {P}^k$ are the new modalities called future and past Pnueli Automata Modalities, respectively, where k is the arity of these modalities.

Let $\rho = (a_1, \tau _1),\ldots (a_n, \tau _n) \in T\varSigma ^*$, $x,y \in dom(\rho )$, $x{\le } y$ and $S = \{\varphi _1,\ldots , \varphi _n\}$ be a given set of $\mathsf {PnEMTL}$ formulae. Let $S_i$ be the exact subset of formulae from S evaluating to true at $\rho , i$, and let $\mathsf {Seg^+}({\rho },{x},{y},S)$ and $\mathsf {Seg^{-}}({\rho },{y},{x},S)$ be the untimed words $S_x S_{x+1} \ldots S_y$ and $S_y S_{y{-}1} \ldots S_x$ respectively. Then, the satisfaction relation for $\rho ,i_0$ satisfying a $\mathsf {PnEMTL}$ formula $\varphi$ is defined recursively as follows:

• $\rho ,i_0{\models }\mathcal {F}^k_{I_1,\ldots ,I_k}(\mathsf {A}_1,\ldots ,\mathsf {A}_{k+1})(S)$ iff ${\exists } {i_0{ {\le } }i_1{\le } i_2 \ldots {\le } i_k {\le } n}$ s.t.

  $\bigwedge \limits _{w=1}^{k}{[(\tau _{i_w} {-} \tau _{i_0} \in I_w)} \wedge \mathsf {Seg^+}(\rho , i_{w{-}1}, i_w,S) \in L({\mathsf {A}_w})] \wedge \mathsf {Seg^+}(\rho , i_{k}, n,S) \in L({\mathsf {A}_{k+1}})$

• $\rho ,i_0 \models \mathcal {P}^k_{I_1,I_2,\ldots ,I_k} (\mathsf {A}_1,\ldots ,\mathsf {A}_k, \mathsf {A}_{k+1})(S)$ iff ${\exists } i_0 {\ge } i_1 {\ge } i_2 \ldots {\ge } i_k {\ge } n$ s.t.

  $\bigwedge \limits _{w=1}^{k}[(\tau _{i_0} {-} \tau _{i_w} \in I_w) \wedge \mathsf {Seg^{-}}(\rho , i_{w{-}1}, i_w,S) \in L({\mathsf {A}_{w}})] \wedge \mathsf {Seg^{-}}(\rho , i_{k}, n,S) \in L({\mathsf {A}_{k+1}})$.

Language of any $\mathsf {PnEMTL}$ formula $\varphi$, as $L(\varphi ) = \{\rho | \rho ,1 \models \varphi \}$. The Pointed Language of $\varphi$ is defined as $L_{pt}(\varphi ) = \{\rho ,i | \rho , i \models \varphi \}$. Given a $\mathsf {PnEMTL}$ formula $\varphi$, its arity is the maximum number of intervals appearing in any $\mathcal {F}, \mathcal {P}$ modality of $\varphi$. For example, the arity of $\varphi =\mathcal {F}^2_{I_1,I_2}(\mathsf {A}_1,\mathsf {A}_2, \mathsf {A}_3)(S_1) \wedge \mathcal {P}^1_{I_1} (\mathsf {A}_1,\mathsf {A}_2)(S_2)$ for some sets of formulae $S_1, S_2$ is 2. For the sake of brevity, $\mathcal {F}^k_{I_1,\ldots ,I_k}(\mathsf {A}_1,\ldots ,\mathsf {A}_{k})(S)$ denotes $\mathcal {F}^k_{I_1,\ldots ,I_k}(\mathsf {A}_1,\ldots ,\mathsf {A}_{k}, \mathsf {A}_{k+1})(S)$ where automata $\mathsf {A}_{k+1}$ accepts all the strings over S. We define non-adjacent $\mathsf {PnEMTL}$, as a subclass where every modality $\mathcal {F}^{k}_{\mathsf {I_1,\ldots , I_k}}$ and $\mathcal {P}^{k}_{\mathsf {I_1,\ldots , I_k}}$ is such that $\{\mathsf {I_1, \ldots , I_k}\}$ is a non-adjacent set of intervals.

$\mathsf {EMITL}$ of [23] (and variants of it studied in [5, 11, 14, 15]) are special cases of the non-adjacent $\mathsf {PnEMTL}$ modality where the arity is restricted to 1 and the second automata in the argument accepts all the strings. Hence, automaton modality of [23] is of the form $\mathsf {\mathcal {F}_I}(A)(S)$. Let $\mathsf {EMITL_{0,\infty }}$ denote the logic $\mathsf {EMITL}$ extended with $\mathcal {F}$ and $\mathcal {P}$ modality where the timing intervals are restricted to be of the form $\langle l, \infty )$ or $\langle 0, u \rangle$.

We conclude this section defining size of a temporal logic formula.

Size of Formulae. Size of a formula $\varphi$ denoted by $|\varphi |$ is a measure of how many bits are required to store it. The size of a $\mathsf {TPTL}$ formula is defined as the sum of the number of $\mathsf {U}$, $\mathsf {S}$ and Boolean operators and freeze quantifiers in it. For $\mathsf {PnEMTL}$ formulae, |op| is defined as the number of Boolean operators and variables used in it. $|(\mathcal {F}^{k}_{I_1,\ldots ,I_k}(\mathsf {A}_1, \ldots , \mathsf {A}_{k+1})(S)|=\sum \limits _{\varphi \in S}(|\varphi |)+ |\mathsf {A}_1|{+}\ldots {+}|\mathsf {A}_{k+1}|$ where $|\mathsf {A}|$ denotes the size of the automaton $\mathsf {A}$ given by sum of number of its states and transitions.

4 Anchored Interval Word Abstraction

All the logics considered here have the feature that a sub-formula asserts timing constraints on various positions relative to an anchor position; e.g. the position of freezing the clock in TPTL. Such constraints can be symbolically represented as an interval word with a unique anchor position and all other positions carry a set of time intervals constraining the time stamp of the position relative to the time stamp of the anchor. See interval word $\kappa$ in Fig. 1. We now define these interval words formally. Let $I_{\nu }\subseteq \mathcal {I}_\mathsf {int}$. An $I_{\nu }$-interval word over $\varSigma$ is a word $\kappa$ of the form $a_1 a_2 \dots a_n \in (2^{\varSigma \cup \{\mathsf {anch}\} \cup I_\nu })^*$. There is a unique $i \in dom(\kappa )$ called the anchor of $\kappa$ and denoted by $\mathsf {anch}(\kappa )$. At the anchor position i, $a_i \subseteq \varSigma \cup \{\mathsf {anch}\}$, and $\mathsf {anch}\in a_i$. Let J be any interval in $\mathcal {I}_\nu$. We say that a point $i \in dom(\kappa )$ is a J-time restricted point if and only if, $J \in a_i$. i is called time restricted point if and only if either i is J-time restricted for some interval J in $I_\nu$ or $\mathsf {anch}\in a_i$.

From $I_\nu$-interval word to Timed Words: Given a $I_\nu$-interval word $\kappa =a_1 \dots a_n$ over $\varSigma$ and a timed word $\rho =(b_1, \tau _1)\dots (b_m, \tau _m)$, the pointed timed word $\rho , i$ is consistent with $\kappa$ iff $dom(\rho )=dom(\kappa )$, $i=\mathsf {anch}(\kappa )$, for all $j\in dom(\kappa )$, $b_j=a_j\cap \varSigma$ and for $j \ne i$, $I \in a_j \cap I_\nu$ implies $\tau _j - \tau _i \in I$. Thus, $\kappa$ and $\rho ,i$ agree on propositions at all positions, and the time stamp of a non-anchor position j in $\rho$ satisfies every interval constraint in $a_j$ relative to $\tau _i$, the time stamp of anchor position. $\mathsf {Time(\kappa )}$ denotes the set of all the pointed timed words consistent with a given interval word $\kappa$, and for a set of interval words $\varOmega$. Note that the “consistency relation” is a many-to-many relation.

Example. Let $\kappa ={\{a,b, (-1,0)\} \{b, (-1,0)\} \{a, \mathsf {anch}\} \{b,[2, 3]\}}$ be an interval word over the set of intervals $\{(-1,0),[2,3]\}$. Consider timed words $\rho$ and $\rho '$ s.t. $\rho \,=\,{(\{a,b\}, 0)(\{b\}, .5), (\{a\}, .95) (\{b\}, 3)}$, $\rho '={(\{a,b\},0)(\{b\},0.8)(\{a\},0.9)}{(\{b\},2.9)}$.

Then $\rho ,3$ as well as $\rho ',3$ are consistent with $\kappa$ while $\rho ,2$ is not. Likewise, for the timed word $\rho '' = (\{a,b\}, 0), (\{b\}, 0.5), (\{a\}, 1.1) (\{b\}, 3)$, $\rho '', 3$ is not consistent with $\kappa$ as $\tau _1-\tau _3 \notin (-1,0)$, as also $\tau _4-\tau _3 \notin [2,3]$.

Let $I_\nu , I_\nu ' \subseteq \mathcal {I}_\mathsf {int}$. Let $\kappa =a_1\dots a_n$ and $\kappa '=b_1 \dots b_m$ be $I_\nu$ and $I_\nu '$-interval words, respectively. $\kappa$ is similar to $\kappa '$, denoted by $\kappa \sim \kappa '$ if and only if,

(i) $dom(\kappa )=dom(\kappa ')$, (ii) for all $i \in dom(\kappa )$, $a_i \cap \varSigma =b_i\cap \varSigma$, and (iii)$\mathsf {anch}(\kappa )=\mathsf {anch}(\kappa ')$. Additionally, $\kappa$ is congruent to $\kappa '$, denoted by $\kappa \cong \kappa '$, iff $\mathsf {Time}(\kappa )=\mathsf {Time}(\kappa ')$. I.e., $\kappa$ and $\kappa '$ abstract the same set of pointed timed words.

Collapsed Interval Words. The set of interval constraints at a position can be collapsed into a single interval by taking the intersection of all the intervals at that position giving a Collapsed Interval Word. Given an $I_{\nu }$-interval word $\kappa =a_1 \dots a_n$, let $\mathcal {I}_j = a_j \cap I_{\nu }$. Let $\kappa '=\mathsf {Col}(\kappa )$ be the word obtained by replacing $\mathcal {I}_j$ with $\bigcap _{I \in \mathcal {I}_j} I$ in $a_j$, for all $j{\in }dom(\kappa )$. Note that $\kappa '$ is an interval word over $\mathsf {CL}(I_\nu )=\{I | I=\bigcap I', I' \subseteq I_\nu \}$. Note that if for any j, the set $\mathcal {I}_j$ contains two disjoint intervals (like [1, 2] and [3, 4]) then $\mathsf {Col}(\kappa )$ is undefined. It is clear that $\mathsf {Time}(\kappa )=\mathsf {Time}(\kappa ')$. An interval word $\kappa$ is called collapsed iff $\kappa =\mathsf {Col}(\kappa )$.

Fig. 1.

Point within the triangle has more than one interval. The encircled points are intermediate points and carry redundant information. The required timing constraint is encoded by first and last time restricted points of all the intervals (within boxes).

Normalization of Interval Words. An interval I may repeat many times in a collapsed interval word $\kappa$. Some of these occurrences are redundant and we can only keep the first and last occurrence of the interval in the normalized form of $\kappa$. See Fig. 1. For a collapsed interval word $\kappa$ and any $I \in I_\nu$, let $\mathsf {first}(\kappa , I)$ and $\mathsf {last}(\kappa ,I)$ denote the positions of first and last occurrence of I in $\kappa$. If $\kappa$ does not contain any occurrence of I, then both $\mathsf {first}(\kappa , I)=\mathsf {last}(\kappa ,I)=\bot$. We define, $\mathsf {Boundary}(\kappa )=\{i | i{\in }dom(\kappa ){\wedge }\exists I{\in }I_\nu$ s.t. $(i=\mathsf {first}(\kappa ,I) {\vee }i=\mathsf {last}(\kappa ,I){\vee }i=\mathsf {anch}(\kappa )) \}$

The normalized interval word corresponding to $\kappa$, denoted $\mathsf {Norm}(\kappa )$, is defined as $\kappa _{nor}=b_1 \dots b_m,$ such that (i) $\kappa _{nor} \sim \mathsf {Col}(\kappa )$, (ii) for all $I \in \mathsf {CL}(I_\nu )$, $\mathsf {first}(\kappa , I)=\mathsf {first}(\kappa _{nor}, I)$, $\mathsf {last}(\kappa , I)=\mathsf {last}(\kappa _{nor}, I)$, and for all points $j \in dom(\kappa _{nor})$ with $\mathsf {first}(\kappa , I)< j < \mathsf {last}(\kappa ,I)$, j is not a I-time constrained point. See Fig. 1. Hence, a normalized word is a collapsed word where for any $J\in \mathsf {CL}(I_\nu )$ there are at most two J-time restricted points. This is the key property which will be used to reduce 1-$\mathsf {TPTL}$ to a finite length $\mathsf {PnEMTL}$ formulae.

Lemma 1

$\kappa \cong \mathsf {Norm}(\kappa )$. Note, $\mathsf {Norm}(\kappa )$ has at most $2{\times }|I_\nu |^2{+}1$ restricted points.

The proof follows from the fact that $\kappa \cong \mathsf {Col}(\kappa )$ and since $\mathsf {Col}(\kappa ) \sim \mathsf {Norm}(\kappa )$, the set of timed words consistent with any of them will have identical untimed behaviour. For the timed part, the key observation is as follows. For some interval $I \in I_{\nu }$, let $i'=\mathsf {first}(\kappa ,I), j'=\mathsf {last}(\kappa , I)$. Then for any $\rho ,i$ in $\mathsf {Time}(\kappa )$, points $i'$ and $j'$ are within the interval I from point i. Hence, any point $i' \le i'' \le j'$ is also within interval I from i. Thus, the interval I need not be explicitly mentioned at intermediate points. The full proof can be found in the full version.

5 1-$\mathsf {TPTL}$ to $\mathsf {PnEMTL}$

In this section, we reduce a 1-$\mathsf {TPTL}$ formula into an equisatisfiable $\mathsf {PnEMTL}$ formula. First, we consider 1-$\mathsf {TPTL}$ formula with a single outermost freeze quantifier (call these simple $\mathsf {TPTL}$ formulae) and give the reduction. More complex formulae can be handled by applying the same reduction recursively as shown in the first step. For any set of formulae S, let $\bigvee S$ denote $\bigvee \limits _{s\in S}s$. A $\mathsf {TPTL}$ formula is said to be simple if it is of the form $x.\varphi$ where, $\varphi$ is a 1-$\mathsf {TPTL}$ formula with no freeze quantifiers. Let $\mathcal {I}_\nu \subseteq \mathcal {I}_\mathsf {int}$. Let $\psi =x.\varphi$ be a simple $\mathcal {I}_\nu$-$\mathsf {TPTL}$ formula and let $\mathsf {CL}(\mathcal {I}_\nu )=I_\nu$. We construct a $\mathsf {PnEMTL}$ formula $\phi$, such that $\rho ,i \models \psi {\iff }\rho , i \models \phi$. We break this construction into the following steps:

• 1) We construct an $\mathsf {LTL}$ formula $\alpha$ s.t. $L(\alpha )$ contains only $I_\nu$-interval words and $\rho ,i \models \psi$ iff $\rho , i \in \mathsf {Time}(L(\alpha ))$. Let A be the NFA s.t. $L(A)=L(\alpha )$. Let W be the set of all $I_\nu$-interval words.

• 2) We partition W into finitely many types, each type, capturing a certain relative ordering between first and last occurrences of intervals from $I_\nu$ as well as $\mathsf {anch}$. Let $\mathcal {T}(I_\nu )$ be the finite set of all types.

• 3) For each type $\mathsf {seq}\in \mathcal {T}$, we construct an NFA $A_{\mathsf {seq}}$ such that $L(A_\mathsf {seq})=\mathsf {Norm}(L(A) \cap W_\mathsf {seq})$, where $W_\mathsf {seq}$ is the set of all the $I_\nu$-interval words of type $\mathsf {seq}$.

• 4) For every type $\mathsf {seq}$, using the $A_{\mathsf {seq}}$ above, we construct a $\mathsf {PnEMTL}$ formula $\phi _\mathsf {seq}$ such that, $\rho , i \models \phi _\mathsf {seq}$ if and only if $\rho , i \in \mathsf {Time}(L(A_\mathsf {seq}))$. The desired $\phi = \bigvee \limits _{\mathsf {seq}\in \mathcal {T}(I_\nu )} ~\phi _\mathsf {seq}$. Hence, $L_{pt}(\phi )=\bigcup \limits _{\mathsf {seq}\in \mathcal {T}} \mathsf {Time}(L(A_\mathsf {seq})) =\mathsf {Time}(L(A)) = L_{pt}(\psi )$.

1a) Simple $\mathsf {TPTL}$ to $\mathsf {LTL}$ over Interval Words: As above, $\psi =x.\varphi$. Consider an $\mathsf {LTL}$ formula $\alpha =\mathsf {F}[\mathsf {LTL}(\varphi ) \wedge \mathsf {anch}\wedge \lnot (\mathsf {F}(\mathsf {anch}) \vee \mathsf {P}(\mathsf {anch}))] \wedge \mathcal {G}(\bigvee \varSigma )$ over $\varSigma '=\varSigma \cup \mathcal {I}_\nu \cup \{\mathsf {anch}\}$, where $\mathsf {LTL}(\varphi )$ is the LTL formula obtained from $\varphi$ by replacing clock constraints $T-x \in I$ with I and $x-T \in I$ with $-I$. Then all words in $L(\alpha )$ are $\mathcal {I}_\nu$-interval words.

Theorem 3

For any timed word $\rho$, $i\in dom(\rho )$, and any clock valuation v, $\rho , i, v \models \psi {\iff }\rho , i \in \mathsf {Time}(L(\alpha ))$.

Proof Sketch. Note that for any timed word $\rho$ and $i \in dom(\rho )$, $\rho ,i, [x \leftarrow \tau _i] \models \varphi$ is equivalent to $\rho , i \models \psi$ since $\psi =x.\varphi$. Let $\kappa$ be any $\mathcal {I}_\nu$-interval word over $\varSigma$ with $\mathsf {anch}(\kappa )=i$. It can be seen that if $\kappa , i \models \mathsf {LTL}(\varphi )$ then for all $\rho ,i \in \mathsf {Time}({\kappa })$ we have $\rho ,i \models \psi$. Likewise, if $\rho ,i \models \psi$ for a timed word $\rho$, then there exists some $\mathcal {I}_\nu$-interval word over $\varSigma$ such that $\rho , i \in \mathsf {Time}(\kappa )$ and $\kappa , i \models \mathsf {LTL}(\varphi )$.

Illustrated on an example, if $\psi =x.\varphi$ and $\varphi =\mathsf {F}(x \in I \wedge a)$. Then $\rho ,i \models \varphi$ iff there exists a point j within an interval I from i, where a holds. Now consider $\alpha =\mathsf {F}^{w}[(I \wedge a) \wedge \mathsf {anch}\wedge \lnot (\mathsf {F}(\mathsf {anch}) \vee \mathsf {P}(\mathsf {anch}))] \wedge \mathcal {G}^w(\bigvee \varSigma )$ whose language consists of interval words $\kappa$ such that there is a point ahead of the anchor point i where both a and I holds. Clearly, words in $\mathsf {Time}({\kappa })$ are such that they contain a point $j>i$ within an interval I from point i where a holds. Hence, $\rho , i \models \psi$ if and only if $\rho , i \in \mathsf {Time}(\{\kappa ~\mid ~ \kappa , i \models \mathsf {LTL}(\varphi )\})$. Moreover, $\kappa \in L(\alpha )$ if and only if $\kappa , i \models \mathsf {LTL}(\varphi )$ and $\mathsf {anch}(\kappa )=i$. The full proof is in the full version.

1b) $\mathsf {LTL}$ to NFA over Collapsed Interval Words. It is known that for any $\mathsf {LTL}[\mathsf {U},\mathsf {S}]$ formula, one can construct an equivalent NFA with at most exponential number of states [6]. We reduce the LTL formula $\alpha$ to an equivalent NFA $A_\alpha =(Q, \mathsf {init}, 2^{\varSigma '}, \delta ', F)$ over $I_{\nu }$-interval words, where $\varSigma '=2^{\varSigma \cup I_{\nu } \cup \{\mathsf {anch}\}}$. From $A_{\alpha }$, we construct an automaton $A=(Q, \mathsf {init}, 2^{\varSigma '}, \delta , F)$ s.t. $L(A)=\mathsf {Col}(L(A_\alpha ))$. Automaton A is obtained from $A_\alpha$ by replacing the set of intervals $\mathcal {I}$ on the transitions by the single interval $\bigcap \mathcal {I}$. In case $\exists I_1, I_2 \in \mathcal {I}$ s.t. $I_1 \cap I_2 = \emptyset$ (i.e. with contradictory interval constraints), the transition is omitted in A. This gives $L(A)=\mathsf {Col}(L(A_\alpha ))$.

2) Partitioning Interval Words. We discuss here how to partition W, the set of all collapsed $I_\nu$-interval words, into finitely many classes. Each class is characterized by its type given as a finite sequences $\mathsf {seq}$ over $I_{\nu } \cup \{\mathsf {anch}\}$. For any collapsed $w \in W$, its type $\mathsf {seq}$ gives an ordering between $\mathsf {anch}(w)$, $\mathsf {first}(w,I)$ and $\mathsf {last}(w,I)$ for all $I \in I_\nu$, such that, any $I \in I_{\nu }$ appears at most twice and $\mathsf {anch}$ appears exactly once in $\mathsf {seq}$. For instance, $\mathsf {seq}=I_1 I_1 \mathsf {anch}I_2 I_2$ is a sequence different from $\mathsf {seq}'=I_1I_2 \mathsf {anch}I_2I_1$ since the relative orderings between the first and last occurrences of $I_1, I_2$ and $\mathsf {anch}$ differ in both. Let the set of types $\mathcal {T}(I_\nu )$ be the set of all such sequences; by definition, $\mathcal {T}(I_\nu )$ is finite. Given $w \in W$, let $\mathsf {Boundary}(w)=\{i_1, i_2, \ldots , i_k\}$ be the positions of w which are either $\mathsf {first}(w,I)$ or $\mathsf {last}(w,I)$ for some $I \in I_{\nu }$ or is $\mathsf {anch}(w)$. Let $w\downarrow _{\mathsf {Boundary}(w)}$ be the subword of w obtained by projecting w to the positions in $\mathsf {Boundary}(w)$, restricted to the sub alphabet $2^{I_{\nu }}\cup \{\mathsf {anch}\}$. For example, $w=\{a,I_1\}\{b,I_1\}\{c,I_2\}\{\mathsf {anch},a\}\{b,I_1\}\{b,I_2\}\{c,I_2\}$ gives $w\downarrow _{\mathsf {Boundary}(w)}$ as $I_1I_2\mathsf {anch}I_1I_2$. Then w is in the partition $W_{\mathsf {seq}}$ iff $w\downarrow _{\mathsf {Boundary}(w)}=\mathsf {seq}$. Clearly, $W=\bigcup _{\mathsf {seq}\in \mathcal {T}(I_\nu )}W_{\mathsf {seq}}$. Continuing with the example above, w is a collapsed $\{I_1, I_2\}$-interval word over $\{a,b,c\}$, with $\mathsf {Boundary}(w)=\{1,3,4,5,7\}$, and $w{\in } W_{\mathsf {seq}}$ for $\mathsf {seq}=I_1I_2\mathsf {anch}I_1 I_2$, while $w\notin W_{\mathsf {seq}'}$ for $\mathsf {seq}'=I_1I_1\mathsf {anch}I_2 I_2$.

3) Construction of NFA for each type: Let $\mathsf {seq}$ be any sequence in $\mathcal {T}(I_\nu )$. In this section, given $A=(Q, \mathsf {init}, 2^{\varSigma '}, \delta , F)$ as constructed above, we construct an NFA $A_\mathsf {seq}=(Q \times \{1,2,\ldots |\mathsf {seq}|+1\}\cup \{\bot \}, (\mathsf {init}, 1), 2^{\varSigma '}, \delta _\mathsf {seq}, F \times \{|\mathsf {seq}|+1\})$ such that $L(A_\mathsf {seq})=\mathsf {Norm}(L(A) \cap W_\mathsf {seq})$. Thus, $\bigcup _{\mathsf {seq}\in \mathcal {T}(I_\nu )}L(A_\mathsf {seq}) = \mathsf {Norm}(L(A))$. Thus, $\bigcup _{\mathsf {seq}\in \mathcal {T}(I_\nu )} \mathsf {Time}(L(A_\mathsf {seq})) = \mathsf {Time}(\mathsf {Norm}(L(A))) = \mathsf {Time}(L(A)) = L(\psi )$. Intuitively, the second element of the state makes sure that only normalized words of type $\mathsf {seq}$ are accepted. From (q, j), $A_\mathsf {seq}$ is allowed to read a set $S \subseteq \varSigma$ (containing no time interval or $\mathsf {anch}$ and hence an unrestricted point) or it can read a set $S\cup \{I\}$ where $S \subseteq \varSigma$ and $J = \mathsf {seq}[j]$ (containing time interval/anchor $\mathsf {seq}[j]$). In case of latter, the $A_\mathsf {seq}$ ends up with a state of the form $(q',j+1)$ if and only if there is a transition in A of the form $q {\mathop {\rightarrow }\limits ^{S\cup {J}}}q'$. In case of the former, it non-determinstically proceeds to a state $(q',j)$ if and only if, in automaton A, there is a transition of the form $q {\mathop {\rightarrow }\limits ^{S}}q'$ or $q {\mathop {\rightarrow }\limits ^{S\cup {J}}}q'$ where $\mathsf {first}(J,w)$ has already been read and $\mathsf {last}(J,w)$ is yet to be read in the future (that is, $\exists j'' j', j'< j \le j'' \wedge \mathsf {seq}[j'] = \mathsf {seq}[j''] = J$). The detailed construction as well as the proof for Lemma 2 can be found in the full version. Let $W_\mathsf {seq}$ denote set of $I_\nu$-interval words of type $\mathsf {seq}$.

Lemma 2

$L(A_\mathsf {seq})=\mathsf {Norm}(L(A) \cap W_\mathsf {seq})$. Hence, $\bigcup \limits _{\mathsf {seq}\in \mathcal {T}(I_\nu )} L(A_\mathsf {seq}) =\mathsf {Norm}(L(A))$.

Our next step is to reduce the NFAs $A_{\mathsf {seq}}$ corresponding to each type $\mathsf {seq}$ to $\mathsf {PnEMTL}$. The words in $L(A_{\mathsf {seq}})$ are all normalized, and have at most $2|I_\nu |+1$-time restricted points. Thanks to this, its corresponding timed language can be expressed using $\mathsf {PnEMTL}$ formulae with arity at most $2|I_\nu |$.

4) Reducing NFA of each type to $\mathsf {PnEMTL}$: Next, for each $A_\mathsf {seq}$ we construct $\mathsf {PnEMTL}$ formula $\phi _\mathsf {seq}$ such that, for a timed word $\rho$ with $i \in dom(\rho ), \rho , i \models \phi _\mathsf {seq}$ iff $\rho , i {\in } \mathsf {Time}(L(A_\mathsf {seq}))$. For any NFA $N = (St,\varSigma , i,Fin,\varDelta )$, $q \in Q$ $F' \subseteq Q$, let $N[q,F'] = (St,\varSigma , q, F', \varDelta )$. For brevity, we denote $N[q,\{q'\}]$ as $N[q,q']$. We denote by $\mathsf {Rev}(N)$, the NFA $N'$ that accepts the reverse of L(N). The right/left concatenation of $a{\in }\varSigma$ with L(N) is denoted $N{\cdot }a$ and $a{\cdot }N$ respectively.

Lemma 3

We can construct a $\mathsf {PnEMTL}$ formula $\phi _\mathsf {seq}$ with arity $\le |I_\nu |^2$ and size $\mathcal {O}(|A_\mathsf {seq}|^{|\mathsf {seq}|})$ containing intervals from $I_\nu$ s.t. $\rho , i \models \phi _\mathsf {seq}$ iff $\rho , i \in \mathsf {Time}(L(A_\mathsf {seq}))$.

Fig. 2.

Figure representing set of runs $A_{\mathsf {I_1 \mathsf {anch}I_3 I_4}}$ of type Qseq where each $S_i \subseteq \varSigma$ and each sub-automaton $Q_i$ has only transitions without any intervals. Here $Qseq = T_1 T_2 T_3 T_4$, for $1\le i \le 4$, $T_i = (p_{i-1} {\mathop {\rightarrow }\limits ^{S_i\cup \{I_i\}}} q_i),$ $I_2 = \{\mathsf {anch}\}$.

Proof

Let $\mathsf {seq}=I_1\ I_2\ \ldots \ I_n$, and $I_j=\mathsf {anch}$ for some $1{\le }j {\le }n$. Let $\varGamma =2^{\varSigma }$ and $\mathsf {Qseq}=T_1\ T_2\ \ldots T_n$ be a sequence of transitions of $A_{\mathsf {seq}}$ where for any $1 \le i \le n$, $T_i=p_{i-1} {\mathop {\rightarrow }\limits ^{S'_{i}}} q_{i}$, $S'_i=S_i \cup \{I_i\}$, $S_i \subseteq \varSigma$, $p_{i-1} \in Q \times \{i-1\}$, $q_{i} \in Q \times \{i\}$. Let $q_0=(\mathsf {init}, 1)$. We define $\mathsf {R}_{\mathsf {Qseq}}$ as set of accepting runs containing transitions $T_1\ T_2\ \ldots T_n$. Hence the runs in $\mathsf {R}_{\mathsf {Qseq}}$ are of the following form:

$T_{0,1}~T_{0,2} \ldots T_{0,m_0}~T_1~~T_{1,1}~ \ldots T_{1,m_1}~T_{2}~~\cdots \cdots ~~T_{n{-}1,1}~T_{n{-}1,2} \ldots T_{n}~~T_{n,1} \ldots T_{n{+}1}$ where the source of the transition $T_{0,1}$ is $q_0$ and the target of the transition $T_{n+1}$ is any accepting state of $A_\mathsf {seq}$. Moreover, all the transitions $T_{i,j}$ for $0\le i\le n$, $1\le j \le n_i$ are of the form $(p' {\mathop {\rightarrow }\limits ^{S_{i,j}}} q')$ where $S_{i,j} \subseteq \varSigma$ and $p',q' \in Q_{i+1}$. Hence, only $T_1, T_2, \ldots T_n$ are labelled by any interval from $I_\nu$. Moreover, only on these transitions the counter (second element of the state) increments. Let $\mathsf {A}_i = (Q_{i}, 2^{\varSigma }, q_{i-1}, \{p_{i-1}\}, \delta _\mathsf {seq}) \equiv A_{\mathsf {seq}}[q_{i-1},p_{i-1}]$ for $1 \le i \le n$ and $\mathsf {A}_{n+1}= (Q_{n+1}, 2^{\varSigma }, q_{n}, F_{\mathsf {seq}},\delta _{\mathsf {seq}}){\equiv }A[q_n,F]$. Let $\mathcal {W}_{Qseq}$ be set of words associated with any run in $\mathsf {R}_{Qseq}$. In other words, any word w in $\mathcal {W}_{Qseq}$ admits an accepting run on A which starts from $q_0$ reads letters without intervals (i.e., symbols of the form $S \subseteq \varSigma$)ends up at $p_0$, reads $S'_1$, ends up at $q_1$ reads letters without intervals, ends up and $p_1$, reads $S'_2$ and so on. Refer Fig. 2 for illustration. Hence, $w \in W_{Qseq}$ if and only if $w \in L(\mathsf {A}_1).S'_1. L(\mathsf {A}_2).S'_2. \cdots . L(\mathsf {A}_n).S'_n.L(\mathsf {A}_{n+1})$.

Let $\mathsf {A}'_{k}=S_{k-1}\cdot {\mathsf {A}_{k}}\cdot S_k$ for $1{\le }k{\le }n{+}1$, with $S_0=S_{n+1}=\epsilon$². Let $\rho =(b_1, \tau _1) \ldots (b_m, \tau _m)$ be a timed word over $\varGamma$. Then $\rho ,i_j \in \mathsf {Time}(W_{Qseq})$ iff $\exists$ $0{\le } i_1 {\le } i_2 {\le } \ldots {\le } i_{j-1} {\le } i_j {\le } i_{j+1} {\le } \ldots {\le } i_n {\le } m$ s.t. $\bigwedge \limits _{k =1}^{j-1}[(\tau _{i_k}{-}\tau _{i_j} \in I_k) \wedge \mathsf {Seg^-}(\rho , i_{k+1}, i_{k},\varGamma ) \in L(\mathsf {Rev}({\mathsf {A}'_{k}}))] \wedge \bigwedge \limits _{k=j}^{n}[(\tau _{i_k}{-}\tau _{i_j} \in I_k) \wedge \mathsf {Seg^+}(\rho , i_{k}, i_{k+1},\varGamma ) \in L(\mathsf {A}'_k)]$, where $i_0=0$ and $i_{n+1}=m$. Hence, by semantics of $\mathcal {F}^{k}$ and $\mathcal {P}^{k}$ modalities, $\rho ,i \in \mathsf {Time}(\mathcal {W}_{Qseq})$ if and only if $\rho , i{\models } \phi _{\mathsf {qseq}}$ where $\phi _{\mathsf {qseq}}=\mathcal {P}^{j}_{I_{j-1},\ldots ,I_{1}} (\mathsf {Rev}(\mathsf {A}'_1),\ldots ,\mathsf {Rev}(\mathsf {A}'_j))(\varGamma ) \wedge \mathcal {F}^{n-j}_{I_{j+1},\ldots ,I_{n}} (\mathsf {A}'_{j+1},\ldots ,\mathsf {A}'_{n+1})(\varGamma )$. Let $\mathsf {State{-}seq}$ be set of all possible sequences of the form $\mathsf {Qseq}$. As $A_\mathsf {seq}$ accepts only words which has exactly n time restricted points, the number of possible sequences of the form $\mathsf {Qseq}$ is bounded by $|Q|^{n}$. Hence any word $\rho , i \in \mathsf {Time}(L(A_\mathsf {seq}))$ iff $\rho , i \models \phi _{\mathsf {seq}}$ where $\phi _{\mathsf {seq}} = \bigvee \limits _{\mathsf {qseq} \in \mathsf {State{-}seq}} \phi _{\mathsf {qseq}}$. Disjuncting over all possible sequences $\mathsf {seq}{\in }\mathcal {T}(I_\nu )$ we get formula $\phi$ and the following lemma.

Lemma 4

Let L(A) be the language of $I_\nu$-interval words definable by a NFA A. We can construct a $\mathsf {PnEMTL}$ formula $\phi$ s.t. $\rho ,i \models \phi$ iff $\rho ,i \in \mathsf {Time}(L(A))$.

Note that, if $\psi$ is a simple 1-$\mathsf {TPTL}$ formula with intervals in $\mathcal {I}_\nu$, then the equivalent $\mathsf {PnEMTL}$ formula $\phi$ constructed above contains only interval in $\mathsf {CL}(\mathcal {I}_\nu )$. Hence, we have the following theorem.

Theorem 4

For a simple non-adjacent 1-$\mathsf {TPTL}$ formula $\psi$ containing intervals from $\mathcal {I}_\nu$, we can construct a non-adjacent $\mathsf {PnEMTL}$ formula $\phi$, s.t. for any valuation v, $\rho ,i,v {\models } \psi$ iff $\rho , i {\models } \phi$ where, $|\phi |=O(2^{Poly(|\psi |)})$ and arity of $\phi$ is $O(|\mathcal {I}_\nu |^2)$.

This is a consequence of Theorem 3, Lemma 2 and Lemma 4. A formal proof appears in the full version For the complexity: The size $\mathsf {LTL}$ formula $\alpha$ constructed from $\psi$ (in 1a))) is linear in $\psi$. The translation from LTL formula $\alpha$ to NFA A has a complexity $\mathcal {O}(2^{|\alpha |}) = \mathcal {O}(2^{|\psi |})$. Let $I_\mu = \mathsf {CL}(\mathcal {I}_\nu )$. Hence, $|I_\mu | = \mathcal {O}(|\mathcal {I}_\nu |^2)$. The size of $A_{\mathsf {seq}}$ is $\mathcal {O}(|\mathsf {seq}| \times 2^{(|\psi |)}) = \mathcal {O}(2^{Poly(|\psi |)})$ as $|\mathsf {seq}| \le 2 \times |I_\mu | = \mathcal {O}(|\mathcal {I}_\nu |^2) = \mathcal {O}(|\psi |^2)$. Next, $|\phi _\mathsf {seq}| = \mathcal {O}(|A_\mathsf {seq}|^{|\mathsf {seq}|}) = \mathcal {O}(2^{Poly(|\psi |)})$. $|T(\mathcal {I}_\nu )| = O(2^{Poly(n)})$. Hence, $|\phi |=O(2^{Poly(n, |Q|)}) = O(2^{Poly(|A|)})$. Moreover, the arity of $\phi$ is also bounded by $2\times |\mathsf {CL}(I_\nu )|$. Note that, $|\mathsf {CL}(I_\nu )| \le |\mathcal {I}_\nu |^2$. Moreover, $\mathsf {CL}(I_\nu )$ is non-adjacent iff $I_\nu$ is. This result is lifted to a (non-simple) 1-$\mathsf {TPTL}$ formula $\psi$ as follows: for each occurrence of a subformula $x.\varphi _i$ in $\psi$, introduce a new propositional variable $a_i$ and replace $x.\varphi _i$ with $a_i$. After replacing all such, we are left with the outermost freeze quantifier. Conjunct $\bigwedge \limits _{i=1}^{m} \mathcal {G}^w(a_i \leftrightarrow x.\varphi _i)$ to the replaced formula obtaining a simple 1-$\mathsf {TPTL}$ formula $\psi '$, equisatisfiable to $\psi$. Apply the procedure above to each of the $m+1$ conjuncts of $\psi '$ resulting in $m+1$ equivalent non-adjacent $\mathsf {PnEMTL}$ formulae $\varphi '_i$. The conjunction of $\varphi '_i$ is the non-adjacent $\mathsf {PnEMTL}$ formula equisatisfiable with $\psi$, giving Theorem 5.

Theorem 5

Any non-adjacent 1-$\mathsf {TPTL}$ formula $\psi$ with intervals in $\mathcal {I}_\nu$, can be reduced to a non-adjacent $\mathsf {PnEMTL}$, $\phi$, with $|\phi |= 2^{Poly(|\psi |)}$ and arity of $\phi =O(|\mathcal {I}_\nu |^2)$ such that $\psi$ is satisfiable if and only if $\phi$ is.

6 Satisfiability Checking for Non-adjacent $\mathsf {PnEMTL}$

Theorem 6

Satisfiability Checking for non-adjacent $\mathsf {PnEMTL}$ and non- adjacent 1-$\mathsf {TPTL}$ are decidable with EXPSPACE complete complexity.

The proof is via a satisfiability preserving reduction to logic $\mathsf {EMITL}_{(0,\infty )}$ resulting in a formula whose size is at most exponential in the size of the input non-adjacent $\mathsf {PnEMTL}$ formula. Satisfiability checking for $\mathsf {EMITL}_{0,\infty }$ is PSPACE complete [11]. This along with our construction implies an EXPSPACE decision procedure for satisfiability checking of non-adjacent $\mathsf {PnEMTL}$. The EXPSPACE lower bound follows from the EXPSPACE hardness of sublogic $\mathsf {MITL}$. The same complexity also applies to non-adjacent 1-$\mathsf {TPTL}$, using the reduction in the previous section. We now describe the technicalities associated with our reduction. We use the technique of equisatisfiability modulo oversampling [12, 16]. Let $\varSigma$ and $\mathsf {OVS}$ be disjoint set of propositions. Given any timed word $\rho$ over $\varSigma$, we say that a word $\rho '$ over $\varSigma \cup \mathsf {OVS}$ is an oversampling of $\rho$ if $|\rho | \le |\rho '|$ and when we delete the symbols in $\mathsf {OVS}$ from $\rho '$ we get back $\rho$. Intuitively, $\mathsf {OVS}$ are set of propositions which are used to label oversampling points only. Informally, a formulae $\alpha$ is equisatisfiable modulo oversampling to formulae $\beta$ if and only if for every timed word $\rho$ excepted by $\beta$ there exists an oversampling of $\rho$ accepted by $\alpha$ and, for every timed word $\rho '$ accepted by $\alpha$ its projection is accepted by $\alpha$. Note that when $|\rho '| > |\rho |$, $\rho '$ will have some time points where no proposition from $\varSigma$ is true. These new points are called oversampling points. Moreover, we say that any point $i' \in dom(\rho ')$ is an old point of $\rho '$ corresponding to i iff $i'$ is the $i^{th}$ point of $\rho '$ when we remove all the oversampling points. For the rest of this section, let $\phi$ be a non-adjacent $\mathsf {PnEMTL}$ formula over $\varSigma$. We break down the construction of an $\mathsf {EMITL}_{0,\infty }$ formula $\psi$ as follows.

• 1) Add oversampling points at every integer timestamp using $\varphi _{\mathsf {ovs}}$ below,

• 2) Flatten the $\mathsf {PnEMTL}$ modalities to get rid of nested automata modalities, obtaining an equisatisfiable formula $\phi _{flat}$,

• 3) With the help of oversampling points, assert the properties expressed by $\mathsf {PnEMTL}$ subformulae $\phi _i$ of $\phi _{flat}$ using only $\mathsf {EMITL}$ formulae,

• 4) Get rid of bounded intervals with non-zero lower bound, getting the required $\mathsf {EMITL}_{0,\infty }$ formula $\psi _i$. Replace $\phi _i$ with $\psi _i$ in $\phi _{flat}$ getting $\psi$.

Let $\mathsf {Last}=\mathcal {G}\bot$ and $\mathsf {LastTS}=\mathcal {G}\bot \vee (\bot \mathsf {U}_{(0,\infty )} \top )$. $\mathsf {Last}$ is true only at the last point of any timed word. Similarly, $\mathsf {LastTS}$, is true at a point i if there is no next point $i+1$ with the same timestamp $\tau _i$. Let $\mathsf {cmax}$ be the maximum constant used in the intervals appearing in $\phi$.

1) Behaviour of Oversampling Points. We oversample timed words over $\varSigma$ by adding new points where only propositions from $\mathsf {Int}$ holds, where $\mathsf {Int}\cap \varSigma = \emptyset$. Given a timed word $\rho$ over $\varSigma$, consider an extension of $\rho$ called $\rho '$, by extending the alphabet $\varSigma$ of $\rho$ to $\varSigma ' = \varSigma \cup \mathsf {Int}$. Compared to $\rho$, $\rho '$ has extra points called oversampling points, where $\lnot \bigvee \varSigma$ (and $\bigvee \mathsf {Int}$) hold. These extra points are added at all integer timestamps, in such a way that if $\rho$ already has points with integer time stamps, then the oversampled point with the same time stamp appears last among all points with the same time stamp in $\rho '$. We will make use of these oversampling points to reduce the $\mathsf {PnEMTL}$ modalities into $\mathsf {EMITL}_{0,\infty }$. These oversampling points are labelled with a modulo counter $\mathsf {Int}=\{\mathsf {int}_0,\mathsf {int}_1,\ldots , \mathsf {int}_{\mathsf {cmax}-1}\}$. The counter is initialized to be 0 at the first oversampled point with timestamp 0 and is incremented, modulo $\mathsf {cmax}$, after exactly one time unit till the last point of $\rho$. Let $i \oplus j=(i+ j) \% \mathsf {cmax}$. The oversampled behaviours are expressed using the formula $\varphi _{\mathsf {ovs}}$: $\{\lnot \mathsf {F}_{(0,1)} \bigvee \mathsf {Int}\wedge \mathsf {F}_{[0,1)} \mathsf {int}_{0}\} \wedge$ $\{\bigwedge \limits _{i=0}^{\mathsf {cmax}-1}\mathcal {G}^w\{(\mathsf {int}_i{\wedge }\mathsf {F}(\bigvee \varSigma ))\rightarrow (\lnot \mathsf {F}_{(0,1)} (\bigvee \mathsf {Int}) \wedge \mathsf {F}_{(0,1]} (\mathsf {int}_{i \oplus 1} \wedge (\lnot \bigvee \varSigma ) \wedge \mathsf {LastTS}))\}$. to an extension $\rho '$ given by $\mathsf {ext}(\rho )=\rho '$ iff (i)$\rho$ can be obtained from $\rho '$ by deleting oversampling points and (ii)$\rho ' \models \varphi _{\mathsf {ovs}}$. Map $\mathsf {ext}$ is well defined as for any $\rho$, $\rho '=\mathsf {ext}(\rho )$ if and only if $\rho '$ can be constructed from $\rho$ by appending oversampling points at integer timestamps and labelling $k^{th}$ such oversampling point (appearing at time $k{-}1$) with $\mathsf {int}_{k{\%}\mathsf {cmax}}$.

2) Flattening. Next, we flatten $\phi$ to eliminate the nested $\mathcal {F}^{k}_{\mathsf {I_1,\ldots , I_k}}$ and $\mathcal {P}^{k}_{\mathsf {I_1,\ldots , I_k}}$ modalities while preserving satisfiability. Flattening is well studied [11, 12, 16, 19]. The idea is to associate a fresh witness variable $b_i$ to each subformula $\phi _i$ which needs to be flattened. This is achieved using the temporal definition $T_i=\mathcal {G}^w((\bigvee \varSigma \wedge \phi _i) \leftrightarrow b_i)$ and replacing $\phi _i$ with $b_i$ in $\phi$, $\phi ''_i=\phi [b_i /\phi _i]$, where $\mathcal {G}^w$ is the weaker form of $\mathcal {G}$ asserting at the current point and strict future. Then, $\phi '_i=\phi ''_i \wedge T_i \wedge \bigvee \varSigma$ is equisatisfiable to $\phi$. Repeating this across all subformulae of $\phi$, we obtain $\phi _{flat}=\phi _t \wedge T$ over the alphabet $\varSigma '=\varSigma \cup W$, where W is the set of the witness variables, $T=\bigwedge _i T_i$, $\phi _t$ is a propositional logic formula over W. Each $T_i$ is of the form $\mathcal {G}^w(b_i \leftrightarrow (\phi _f \wedge \bigvee \varSigma ))$ where $\phi _f=\mathcal {F}^{n}_{\mathsf {I_1,\ldots , I_n}}(\mathsf {A}_1, \ldots , \mathsf {A}_{n+1})(S)$ (or uses $\mathcal {P}^{n}_{\mathsf {I_1,\ldots , I_n}}$) and $S \subseteq \varSigma '$. For example, consider the formula $\phi =\mathcal {F}^2_{(0,1)(2,3)}(\mathcal {A}_1, \mathcal {A}_2,\mathcal {A}_3)(\{\phi _1 , \phi _2\})$, where $\phi _1 = \mathcal {P}^2_{(0,2)(3,4)}(A_4,A_5, A_6)(\varSigma ),\phi _2 = \mathcal {P}^2_{(1,2)(4,5)}(A_7,A_8, A_9)(\varSigma )$. Replacing the $\phi _1, \phi _2$ modality with witness propositions $b_1, b_2$, respectively, we get $\phi _t=\mathcal {F}^2_{(0,1)(2,3)}(A_1,A_2,A_3)(\{b_1, b_2\}) \wedge T$, where $T=\mathcal {G}^w(b_1 \leftrightarrow (\bigvee \varSigma \wedge \phi _1)) \wedge \mathcal {G}^w(b_2 \leftrightarrow (\bigvee \varSigma \wedge \phi _2))$, $A_1,A_2,A_3$ are automata constructed from $\mathcal {A}_1, \mathcal {A}_2, \mathcal {A}_3$, respectively, by replacing $\phi _1$ by $b_1$ and $\phi _2$ by $b_2$ in the labels of their transitions. Hence, $\phi _{flat}=\phi _t \wedge T$ is obtained by flattening the $\mathcal {F}^{k}_{\mathsf {I_1,\ldots , I_k}},\mathcal {P}^{k}_{\mathsf {I_1,\ldots , I_k}}$ modalities.

3) Obtaining equisatisfiable $\mathsf {EMITL}$ formula $\psi _f$ for the $\mathsf {PnEMTL}$ formula $\phi _f$ in each $T_i=\mathcal {G}^w(b_i \leftrightarrow (\phi _f \wedge \bigvee \varSigma ))$. The next step is to replace all the $\mathsf {PnEMTL}$ formulae occurring in temporal definitions $T_i$. We use oversampling to construct the formula $\psi _f$: for a timed word $\rho$ over $\varSigma$, $i \in dom(\rho )$, there is an extension $\rho '=\mathsf {ext}(\rho )$ over an extended alphabet $\varSigma '$, and a point $i' \in dom(\rho ')$ which is an old point corresponding to i such that $\rho ', i' \models \psi _f$ iff $\rho , i \models \phi _f$. Consider $\phi _f=\mathcal {F}^{n}_{\mathsf {I_1,\ldots , I_n}}(\mathsf {A}_1, \ldots , \mathsf {A}_{n+1})(S)$ where $S \subseteq \varSigma '$. Wlg, we assume:

• [Assumption1]: $\inf (\mathsf {I_1}) \le \inf (\mathsf {I_2}) \le \ldots \le \inf (\mathsf {I_n})$ and $\sup (\mathsf {I_1}) \le \ldots \le \sup (\mathsf {I_n})$. This is wlog, since the check for $\mathsf {A}_{j+1}$ cannot start before the check of $\mathsf {A}_{j}$ in case of $\mathcal {F}^{n}_{\mathsf {I_1,\ldots , I_n}}$ modality (and vice-versa for $\mathcal {P}^{n}_{\mathsf {I_1,\ldots , I_n}}$ modality) for any $1\le j \le n$.

• [Assumption 2]: Intervals $\mathsf {I_1, \ldots I_{n-1}}$ are bounded intervals. Interval $\mathsf {I_{n}}$ may or may not be bounded. This is also wlog³.

Let $\rho =(a_1, \tau _1) \dots (a_n, \tau _n)\in T\varSigma ^*$, $i \in dom(\rho )$. Let $\rho '=\mathsf {ext}(\rho )$ be defined by $(b_1, \tau '_1)\dots (b_m, \tau '_m)$ with $m \ge n$, and each $\tau '_i$ is a either a new integer timestamp not among $\{\tau _1, \dots , \tau _n\}$ or is some $\tau _j$. Let $i'$ be an old point in $\rho '$ corresponding to i. Let $i'_0=i'$ and $i'_{n+1} = |\rho '|$. $\rho , i \models \phi _f$ iff $\mathsf {cond} \equiv \exists i'\le i_1' \le \ldots \le i'_{n+1} \bigwedge \limits _{g=1}^n (\tau '_{i'_g} -\tau '_{i'} {\in } \mathsf {I}_g \wedge \rho ',i'_g{\models }\bigvee \varSigma \wedge \mathsf {Seg^+}(\rho ', i'_{g-1}, i'_g, S'){\in }L(\mathsf {A}'_g)) \wedge \mathsf {Seg^+}(\rho ', i'_{n}, i'_{n+1}, S'){\in }L(\mathsf {A}'_{n+1})$ where for any $1\le j \le n+1$, $\mathsf {A}'_j$ is the automata built from $\mathsf {A}_j$ by adding self loop on $\lnot \bigvee \varSigma$ (oversampling points) and $S' = S \cup \{\lnot \bigvee \varSigma \}$. This self loop makes sure that $\mathsf {A}'_j$ ignores(or skips) all the oversampling points while checking for $\mathsf {A}_j$. Hence, $\mathsf {A}'_j$ allows arbitrary interleaving of oversampling points while checking for $\mathsf {A}_j$. Hence, for any $g,h \in dom(\rho )$ with $g',h'$ being old action points of $\rho '$ corresponding to g, h, respectively, $\mathsf {Seg^{s}} (\rho , g, h, S){\in }L(\mathsf {A}_i)$ iff $\mathsf {Seg^{s}} (\rho ', g', h', S\cup \{\lnot \bigvee \varSigma \}) \in L(\mathsf {A}'_i)$ for $s \in \{+,-\}$. Note that the question, “$\rho ,i\models \phi _f?$”, is now reduced to checking $\mathsf {cond}$ on $\rho '$.

Checking the conditions for $\rho , i \models \phi _f$. Let $I_g=\langle l_g, u_g \rangle$ for any $1 \le g \le n$ (Here, $\langle \rangle$ denotes half-open, closed, or open). We discuss only the case where $\{I_1, \ldots , I_n\}$ are pairwise disjoint and $\inf (I_1) \ne 0$ in $\phi _f=\mathcal {F}^{n}_{\mathsf {I_1,\ldots , I_n}}(\mathsf {A}_1, \ldots , \mathsf {A}_{n+1})(S)$. The case of overlapping intervals can be found in the full version. The disjoint interval assumption along with [Assumption 1] implies that for any $1 \le g \le n$, $u_{g-1} < l_g$. By construction of $\rho '$, between $i'_{g-1}$ and $i'_g$, we have an oversampling point $k_g$. The point $k_g$ is guaranteed to exist between $i'_{g-1}$ and $i'_g$, since these two points lie within two distinct non-overlapping, non-adjacent intervals $\mathsf {I}_{g-1}$ and $\mathsf {I}_{g}$ from $i'$. Hence their timestamps have different integral parts, and there is always a uniquely labelled oversampling point $k_g$ with timestamp $\lceil \tau '_{i'_{g-1}} \rceil$ between $i'_{g-1}$ and $i'_{g}$ for all $1{\le } g {\le } n$. Let for all $1{\le } g {\le } n+1$, $\mathsf {A}'_g = (Q_g,2^S,init_g, F_g, \delta '_g)$. Let the unique label for $k_g$ be $\mathsf {int}_{j_g}$. For any $1\le g \le n$, we assert that the behaviour of propositions in S between points $i'_{g-1}$ and $i'_g$ (of $\rho '$) should be accepted by $\mathsf {A}'_g$. This is done by splitting the run at the oversampling point $k_g$(labelled as $\mathsf {int}_{j_g}$) with timestamp $\tau '_{k_g}=\lceil \tau '_{i'_{g-1}}\rceil$, $i'_{g-1}< k_g < i'_g$.

• (1) Concretely, checking for $\mathsf {cond}$, for each $1 \le g \le n$, we start at $i'_{g-1}$ in $\rho '$, from the initial state $init_g$ of $\mathsf {A}_g$, and move to the state (say $q_g$) that is reached at the closest oversampling point $k_g$. Note that we use only $\mathsf {A}_g$ (we disallow the $\lnot \bigvee \varSigma$ self loops) to move to the closest oversampling point.

• (2) Reaching $q_g$ from $init_g$ we have read a behaviour between $i'_{g-1}$ and $k_g$; this must to the full behaviour, and hence must also be accepted by $\mathsf {A}'_g$(we use $\mathsf {A}'_g$ instead of $\mathsf {A}_g$ to ignore the oversampling points that could be encountered while checking the latter part). Towards this, we guess a point $i'_g$ which is within interval $\mathsf {I}_g$ from $i'$, such that, the automaton $\mathsf {A}'_g$ starts from state $q_g$ reading $\mathsf {int}_{k_g}$ and reaches a final state in $F_g$ at point $i'_g$. Then indeed, the behaviour of propositions from S between $i'_{g-1}$ and $i'_g$ respect $\mathsf {A}'_g$, and also $\tau '_{i'_g} -\tau '_{i'} \in \mathsf {I}_g$.

• (1) amounts to $\mathsf {Seg^+}(\rho ', i'_{g-1}, k_g, S){\in } L(\mathsf {A}_g[init_g,q_g])\cdot \mathsf {int}_{j_g}$. This is defined by the formula $\psi ^+_{g-1, \mathsf {int}_{j_g},Q_g}$ which asserts $\mathsf {A}_{g+1}[init_{g},q_g] \cdot \mathsf {int}_{j_g}$ from point $i'_{g-1}$ to the next nearest oversampling point $k_g$ where $\mathsf {int}_{j_g}$ holds.

• (2) amounts to checking from point i, within interval $\mathsf {I}_g$ in its future, the existence of a point $i'_g$ such that $\mathsf {Seg^-}(\rho ', i'_g, k_g, S){\in }L(\mathsf {Rev}(\mathsf {int}_{j_g} \cdot \mathsf {A}'_g[q_g,F_g]))$. This is defined by the formula $\varphi ^-_{g, \mathsf {int}_{j_g},q_g}$ which asserts $\mathsf {Rev}(\mathsf {int}_{j_g}\cdot \mathsf {A}'_g[q_g, F_g])$, from point $i'_g$ to an oversampling point $k_g$ which is the earliest oversampling point s.t. $i'_{g-1}< k_g < i'_g$. For $\mathsf {cond}$, we define the formula $\psi =\mathsf {F}_{[0,1)} \mathsf {int}_{j_0} \wedge \bigvee \limits _{g=1}^{n} [\psi ^+_{g-1, \mathsf {int}_{j_g},q_g} \wedge \psi ^-_{g,\mathsf {int}_{j_g},q_g}] \wedge \psi ^+_n$.

• For $1\le g \le n$, $\psi ^+_{g-1, \mathsf {int}_{j_g},q_g}=\mathsf {F}_{I_g}( \bigvee \varSigma \wedge \mathcal {F}(\mathsf {A}_{g}[init_{g},q_g] \cdot \{\mathsf {int}_{j_g}\})(S \cup \{\mathsf {int}_{j_g}\}))$,

• $\psi ^+_{n}=\mathsf {F}_{I_n}(\bigvee \varSigma \wedge \mathcal {F}(\mathsf {A}_{n+1}\cdot \{\mathsf {Last}\})(S \cup \{\mathsf {Last}\}))$, and

• For $1 \le g \le n$, $\psi ^-_{g, \mathsf {int}_{j_g}, q_g}=\mathsf {F}_{I_g}(\bigvee \varSigma \wedge \mathcal {P}(\mathsf {Rev}(\mathsf {int}_{j_g} \cdot \mathsf {A}_{g}[q_g,F_g]))( S \cup \{\mathsf {int}_{j_g}\}))$.

Note that there is a unique point between $i'_{g-1}$ and $i'_{g}$ labelled $\mathsf {int}_{j_g}$. This is because, $\tau '_{i'_g} - \tau '_{i'_{g-1}} < \tau '_{i'_g} - \tau '_{i'} \le \mathsf {cmax}$. Hence, we can ensure that the meeting point for the check (1) and (2) is indeed characterized by a unique label. Note that there is exactly one point labeled $\mathsf {int}_y$ from any point within future $\mathsf {cmax}$ or past $\mathsf {cmax}$ time units (by $\varphi _{\mathsf {ovs}}$). This is the reason we used the counter modulo $\mathsf {cmax}$ to label the oversampling points. We encourage the readers to see the Fig. 3. The full $\mathsf {EMITL}$ formula $\psi _f$, is obtained by disjuncting over all n length sequences of states reachable at oversampling points $k_g$ between $i'_{g-1}$ and $i'_g$, and all possible values of the unique label $\mathsf {int}_{j_g}\in \mathsf {Int}$ holding at point $k_g$.

Fig. 3.

Figure showing elimination of $\mathcal {F}^2$ modality from temporal definition of the form $\mathcal {G}^w(b \leftrightarrow \mathcal {F}^2_{(1,2), (3,4)}(A_1, A_2, A_3)(\varSigma ')$. This is done by (i) checking for the first part of $A_1$, $A_{1,1}$, from present point to the next oversampling point at timestamp $\lceil \tau _i \rceil$, labelled, $\mathsf {int}_j$, (ii) jumping to a non-deterministically chosen point within (1, 2) and asserting the remaining part of $A_1$ skipping oversampling points, $A'_{1,2}$, in reverse till $\mathsf {int}_j$, (iii) Following the steps similar to (i) and (ii) for checking $A_2$ but starting the check of first part of $A_2$ from the point chosen in (ii).

4) Converting the $\mathsf {EMITL}$ to $\mathsf {EMITL}_{0,\infty }$: We use the reduction from $\mathsf {EMITL}$ to equivalent $\mathsf {EMITL}_{0,\infty }$ formula [16]. In $\psi _f$, only the $\mathsf {F}$ operators are timed with intervals of the form $\langle l, u \rangle$ where $l>0$ and $u \ne \infty$, but the $\mathsf {\mathcal {F}_I}$ and $\mathsf {\mathcal {P}_I}$ modalities are untimed. We can reduce these time intervals into purely lower bound ($\langle l, \infty )$) or upper bound ($\langle 0, u \rangle$) constraints using these oversampling points, preserving satisfiability, by reduction showed in [16] Chap. 5 lemma 5.5.2 Page 90–91.

The above 4 step construction shows that (i) the equisatisfiable $\mathsf {EMITL}_{0,\infty }$ formula $\psi$ is of the size $(\mathcal {O}(|\phi |^{Poly(n)})$ where, n is the arity $\phi$. (ii) For a non-adjacent 1-$\mathsf {TPTL}$ formula $\gamma$, applying the reduction in Sect. 5 yields $\phi$ of size $\mathcal {O}(2^{Poly|\gamma |})$ and, arity of $\phi = \mathcal {O}(|\gamma |^2)$. Also, after applying the reduction of Sect. 6 by plugging the value of $|\phi |$ from and its arity from (ii) in (i), we get the $\mathsf {EMITL_{0,\infty }}$ formula $\psi$ of size $\mathcal {O}(2^{Poly(|\gamma |)*Poly(n)})= \mathcal {O}(2^{Poly(|\gamma |)})$.

7 Conclusion

We generalized the notion of non-punctuality to non-adjacency in $\mathsf {TPTL}$. We proved that satisfiabilty checking for non-adjacent 1-variable fragment of $\mathsf {TPTL}$ is EXPSPACE Complete. This gives us a strictly more expressive logic than $\mathsf {MITL}$ while retaining its satisfaction complexity. An interesting open problem is to compare the expressive power of non-adjacent 1-$\mathsf {TPTL}$ with that of $\mathsf {MITL}$ with Pnueli modalities (and hence Q2MLO) of [10]. We also leave open the satisfiabilty checking problem for non-adjacent $\mathsf {TPTL}$ with multiple variables.