Metric Linear-Time Temporal Logic with Strict First-Time Semantics

Let $𝒫=\{p,q,\mathrm{\dots }\}$ be a non-empty, countable set of atomic propositions. Formulas of the linear-time temporal logic LTL are given by the following grammar.

where $q\in 𝒫$. Further Boolean operators like $𝗍𝗍,𝖿𝖿,\vee ,\to ,\leftrightarrow$ are introduced as abbreviations in the usual way, and so are the temporal operators $𝙵\phi :=𝗍𝗍𝚄\phi$, $𝙶\phi :=\neg 𝙵\neg \phi$, $\phi 𝚁\psi :=\neg (\neg \phi 𝚄\neg \psi )$.

The set $\mathrm{𝑆𝑢𝑏}(\phi )$ of subformulas of $\phi$ is defined in the usual way. The size of a formula $\phi$ is measured in terms of the number of its subformulas: $|\phi |:=|\mathrm{𝑆𝑢𝑏}(\phi )|$. For our purposes here, it makes no difference whether formulas with abbreviated operators are written out in the original syntax or the abbreviated operators are seen as first-class citizens. The size in the former case is only larger by a constant factor compared to the latter case.

Formulas of LTL are interpreted over traces of labelled transition systems which are just $\omega$-words over the alphabet $2^{𝒫}$. Note that any formula can contain only finitely many propositional symbols. Hence, the alphabet underlying any given formula can always be assumed to be finite. Let $w=a_0{a}_1\mathrm{\dots }\in {(2^{𝒫})}^{\omega }$ and $i\in \mathbb{N}$. Satisfaction of an LTL formula $\phi$ in $w$ at position $i$ is explained inductively as follows.

A word $w$ satisfies a formula $\phi$, written $w\vDash \phi$, if $\phi$ is satisfied in its initial position, i.e. $w,0\vDash \phi$. The language of a formula $\phi$ is the set of all words satisfying it: $L(\phi ):=\{w\mid w\vDash \phi \}$. Two formulas are equivalent, written $\phi \equiv \psi$, when their languages coincide, i.e. $L(\phi )=L(\psi )$. Note that this is the case if and only if they are satisfied by exactly the same positions in the same words, i.e. $w,i\vDash \phi$ iff $w,i\vDash \psi$. The “if”-direction is trivial because two formulas that are satisfied by the same words at arbitrary positions are clearly satisfied by the same words at initial positions. The “only if”-direction holds because LTL has future-only operators, so we have $a_0{a}_1\mathrm{\dots },i\vDash \phi$ iff $a_i{a}_{i+1}\mathrm{\dots },0\vDash \chi$ for any $\phi$. Thus, any position in a word is the initial position of another word, namely the suffix starting at this position.

A formula is valid, written $\vDash \phi$, if $L(\phi )={(2^{𝒫})}^{\omega }$, i.e. it is satisfied by any word. The satisfiability problem – given a formula $\phi$, decide whether $L(\phi )\ne \mathrm{\varnothing }$ – is well-known to be decidable. We write $\text{SAT}(ℒ)$ for the satisfiability problem for logic $ℒ$. We assume familiarity with standard complexity classes, in particular the space complexity classes NLogSpace, PSpace and ExpSpace. For further details we refer to standard textbooks in complexity theory, e.g. [2].

The term “metric” temporal logic usually refers to extensions of ordinary temporal logics (like LTL) with modifications of the temporal operators that impose restrictions on the moments that witness their satisfaction in case of an Until or a Finally, resp. relax the future moments under consideration of a Generally, resp. Release formula. The logic MTL is obtained by extending the syntax of LTL with a metric version of Until, written $\phi {𝚄}_I\psi$ for a non-empty interval $I$ over the natural numbers.

We use standard notation for closed, half-open and open intervals like $[x,y],(x,y],[x,y)$ and $(x,y)$ for $x,y\in \mathbb{N}\cup \{\mathrm{\infty }\}$ with $x\le y$. Because of the discrete nature of $\mathbb{N}$ and the lack of a direct predecessor of $\mathrm{\infty }$ in this structure, we can restrict our attention to intervals of the form $[x,y]$ for $x,y\in \mathbb{N}$, and of the form $[x,\mathrm{\infty })$ for $x\in \mathbb{N}$. Note that $(x,y]=[x+1,y]$ etc.

Intervals of the form $[0,y]$ or $[x,\mathrm{\infty })$ for some $x,y\in \mathbb{N}$ are called simple and written more compactly as $\le y$, resp. $\ge x$.

The semantics of formulas of MTL is extended accordingly for words $w=a_0{a}_1\mathrm{\dots }\in {(2^{𝒫})}^{\omega }$ and $i\in \mathbb{N}$ by

Hence, $\phi {𝚄}_I\psi$ note only requires a position $i$ in $w$ to satisfy $\phi 𝚄\psi$ in the usual sense that some future moment satisfies $\psi$ and all future moments before that satisfy $\phi$. It additionally requires that future moment to be found at a distance which falls into the interval $I$.

This clearly extends the non-metric version of LTL because $\phi 𝚄\psi \equiv \phi {𝚄}_{\ge 0}\psi$. The metric extension is then applied to the other derived temporal operators $𝙵,𝙶$ and $𝚁$ accordingly.

Because of the use of natural numbers as interval bounds in temporal operators, number of subformulas is not a realistic measure of the representation size of a formula anymore. Note that ${𝙵}_{[x,y]}p$, stating that $p$ occurs in a word at some distance between $x$ and $y$ would have constant size regardless of the values of $x$ and $y$. We assume that such interval bounds are given in binary encoding and therefore measure the size of a formula more appropriately as follows. Let $m(\phi ):=$

denote the largest integer constant that is used as an interval bound in a subformula of $\phi$. Then $|\phi |:=|\mathrm{𝑆𝑢𝑏}(\phi )|\cdot \lceil \log m(\phi )\rceil$.

Let $𝒫$ be a finite set of atomic propositions. A nondeterministic Streett automaton (NSA) is an $𝒜=(Q,𝒫,q_I,\delta ,ℱ)$ where $Q$ is a finite set of states, $q_I\in Q$ is the designated initial state, $\delta \subseteq Q\times 𝔹(𝒫)\times Q$ is a finite set of transition triples $(p,\beta ,q)$ with $𝔹(𝒫)$ denoting the set of Boolean formulas over $𝒫$ (with the usual Boolean operators $\wedge$, $\vee$, $\neg$, …). Finally, $ℱ=\{(F_1,G_1),\mathrm{\dots },(F_m,G_m)\}$ with $F_i,G_i\subseteq Q$ for all $i=1,\mathrm{\dots },m$ is the acceptance condition.

Note that here such finite automata have a symbolically represented transition table instead of the general $\delta \subseteq Q\times \mathrm{\Sigma }\times Q$ for a finite alphabet $\mathrm{\Sigma }$. The reason for this choice is their use in a decision procedure for a temporal logic whose formulas are naturally interpreted over $\omega$-words whose letters are finite sets of propositions, i.e. $\mathrm{\Sigma }=2^{𝒫}$. Instead of enumerating all such possible sets and explaining the automaton’s one-step behaviour for each step, the symbolic representation here is more convenient for such special cases. There are straightforward translations for the transition relations between symbolic and explicit representations, and for a fixed set of propositions, they are polynomial. Hence, we can safely use Streett automata in this form and still appeal to known results about them, even though they were perhaps formulated for the form with an explicit alphabet.

A run of the NSA $𝒜=(Q,𝒫,q_I,\delta ,ℱ)$ with $ℱ=\{(F_1,G_1),\mathrm{\dots },(F_m,G_m)\}$ on a word $w=a_0{a}_1\mathrm{\dots }\in {(2^{𝒫})}^{\omega }$ is a $\rho =q_0,q_1,\mathrm{\dots }\in Q^{\omega }$ such that $q_0=q_I$ and for all $i\in \mathbb{N}$ there is some $(p,\beta ,q)\in \delta$ such that $q_i=p$, $a_i\vDash \beta$ and $q=q_{i+1}$. Here, satisfaction of a Boolean formula $\beta$ over $𝒫$ by a set $a\subseteq 𝒫$, $a\vDash \beta$, is explained in the usual way: $\beta$ evaluates to true when all $q\in a$ are set to true and all $q\notin a$ are set to false.

We write $\mathrm{𝐼𝑛𝑓}(\rho )$ to denote the set of all states that occur infinitely often in $\rho$. By finiteness of $Q$, we always have $\mathrm{𝐼𝑛𝑓}(\rho )\ne \mathrm{\varnothing }$.

The run $\rho$ is accepting if it satisfies the Streett condition $ℱ$ in the sense that for all $i=1,\mathrm{\dots },m$: if $\mathrm{𝐼𝑛𝑓}(\rho )\cap F_i\ne \mathrm{\varnothing }$ then $\mathrm{𝐼𝑛𝑓}(\rho )\cap G_i\ne \mathrm{\varnothing }$. As usual, $L(𝒜)$ is the language of the NSA $𝒜$, and it consists of all words on which $𝒜$ has an accepting run.

So both NSA and formulas of linear-time temporal logics defines languages of $\omega$-words which is why these different formalisms can be compared to one another in terms of expressiveness, and satisfiability of a formula corresponds to non-emptiness of the language of an automaton. Algorithms for non-emptiness problems for $\omega$-automata are routinely used to obtain decision procedures for linear-time temporal logics [21, 20, 4]. It has been shown that non-emptiness for Streett automata can be decided in polynomial time [8, 12] and this requires an explicit construction. A polynomial (equivalence-preserving) translation into Büchi automata is not possible, let alone one computable in logarithmic space. This would immediately transfer the upper bound of NLogSpace to Streett automata. Nevertheless, it does hold, too; it simply needs to be shown directly.

The key observation is the following. The language of an NSA $𝒜=(Q,𝒫,q_I,\delta ,ℱ)$ with $n:=|Q|$ and $ℱ=\{(F_1,G_1),\mathrm{\dots },(F_k,G_k)\}$ is non-empty iff there is an ultimately periodic word $w=u{v}^{\omega }\in L(𝒜)$. This follows from finiteness of $n$ and $k$ by the pigeon hole principle. An accepting run on an arbitrary word must eventually traverse a state $q$ for the second time such that in between, for every $i=1,\mathrm{\dots },k$, either no state from $F_i$ or some state from $G_i$ has been seen.

This gives rise to a nondeterministic algorithm for deciding non-emptiness. It guesses, step-by-step, the states of a run and also nondeterministically remembers some state $q$ occurring in this simulation. It then maintains $2k$ bits to remember, for each $i=1,\mathrm{\dots },k$, whether some state in $F_i$ and some state in $G_i$ has been seen. It accepts, when $q$ occurs again, and the bits indicate that the Streett condition has been met in between.

In order to terminate and reject on computation paths with unsuccessful guesses, it counts the number of steps done in this simulation. It is not hard to see that the first occurrence of $q$ can be required to occur after at most $n$ steps. The second occurrence can be expected to occur after no more than a further $2nk$ steps, for otherwise the run contains parts that could be skipped. Hence, the space needed for the counter is at most logarithmic in $|𝒜|$. $◀$

We introduce Metric Linear-Time Temporal Logic with Strict First-Time Semantics (MTL¹) which, instead of metric Until formulas of the form $\phi {𝚄}_I\psi$, features a special modification $\phi {𝚄}_I^1\psi$ that is interpreted under strict first-time semantics. Intuitively, it does not just demand that some occurrence of $\psi$ in the future happens at a distance that falls into the interval $I$. Instead, it requires this to be the first time in the future that this happens.

The intuition behind the restriction to first-time occurrences is made formal as follows.

LTL trivially embeds into sMTL¹ which trivially embeds into MTL¹. The reason for this is the fact whenever an Until-formula gets satisfied somewhere then there is also a first time that this happens. A more interesting question concerns the other direction, and therefore also the connection to MTL. Since LTL can trivially be embedded into MTL, we immediately obtain a translation from MTL¹ into MTL, from one from MTL¹ into LTL.

We remark that the translations introduced in the following are not polynomial for formula length, measure in terms of length of string representations, but only for formula size, measured in terms of number of subformulas, as they often require the duplication of subformulas.

The first observation about expressiveness is the expressive equivalence between MTL¹ and sMTL¹. This is perhaps a little bit surprising as this principle does not apply to MTL.

We can define $\widehat{\phi }$ inductively. The only non-trivial case is that of an Until formula. Then we have

for $x,y\in \mathbb{N}$. Clearly, this increases the number of subformulas at most by factor $3$. Correctness of this translation is straightforward by inspection of the semantics. $◀$

Because of Thm. 7 we can restrict our attention to sMTL¹ formulas down below as this simplifies the technical details of various constructions slightly.

One reason for considering numerical values in formulas to be represented in binary (as opposed to unary), apart from this being natural, is the fact that the expressive power of sMTL¹– and that of MTL in fact – does not exceed that of LTL. However, translations back into LTL are polynomial in the value of interval bounds only, i.e. they are in fact exponential in the size of a formula.

We define a translation $\widehat{\cdot }:{\text{sMTL}}^1\to \text{LTL}$ as follows.
$\widehat{q}$ $:=q$ $\widehat{\phi \wedge \psi }$ $:=\widehat{\phi }\wedge \widehat{\psi }$ $\widehat{\neg \phi }$ $:=\neg \widehat{\phi }$ $\widehat{𝚇\phi }$ $:=𝚇\widehat{\phi }$ $\widehat{\phi {𝚄}_{\le k}^1\psi }$ $:=\widehat{\psi }\overrightarrow{\vee }\underset{k\text{ occurrences of }𝚇}{\underbrace{(\widehat{\phi }\wedge 𝚇(\widehat{\psi }\overrightarrow{\vee }\mathrm{\dots }\overrightarrow{\vee }𝚇(\widehat{\psi }\overrightarrow{\vee }(\widehat{\phi }\wedge 𝚇\widehat{\psi }}})\mathrm{\dots })))$ $\widehat{\phi {𝚄}_{\ge k}^1\psi }$ $:=\underset{k\text{ occurrences of }𝚇}{\underbrace{\widehat{\phi }\wedge \neg \widehat{\psi }\wedge 𝚇(\widehat{\phi }\wedge \neg \widehat{\psi }\wedge 𝚇(\mathrm{\dots }𝚇(\widehat{\phi }\wedge \neg \widehat{\psi }\wedge 𝚇(\phi 𝚄\psi ))}}\mathrm{\dots }))$
The translation of an operator ${𝚄}_{\sim k}^1$ clearly produces a formula whose size is linear in the value $k$, i.e. exponential in the representation size of $k$. Replacing the abbreviated biased disjunctions by plain Boolean formulas only incurs a further polynomial blow-up because formula size is measured in terms of number of subformulas.

Correctness of the translation is proved by a straightforward induction on the structure of $\phi$, showing that for all $w\in {(2^{𝒫})}^{\omega }$ and all $i\in \mathbb{N}$, we have $w,i\vDash \widehat{\phi }$ iff $w,i\vDash \phi$. $◀$

The exponential blow-up predicted by Thm. 8 may seem like a downside at first sight. However, it should be read as the possibility that certain properties, which are definable in LTL, can be defined in sMTL¹ with much shorter formulas. The same phenomenon is of course known from LTL. It is easy to show that every family of LTL formulas equivalent to the MTL formulas ${\phi }_n:={𝙵}_{\ge 2^n}q$ require size $𝒪(2^n)$. The proof can be re-used entirely to show that sMTL¹ is also exponentially more succinct than LTL. Note that $|{𝙵}_{\ge 2^n}^{1}q|=𝒪(n)$.

Consider the sMTL¹ formulas ${\phi }_n:={𝙵}_{\ge 2^n}^{1}q$ for $n\ge 1$. Clearly, $|{\phi }_n|=𝒪(n)$. By a standard induction on the structure of LTL formulas we can show that formulas of size cannot distinguish between the two words $w_n={\mathrm{\varnothing }}^{2^n-1}\{q\}{\mathrm{\varnothing }}^{\omega }$ and $w_n^{\prime }={\mathrm{\varnothing }}^{2^n}\{q\}{\mathrm{\varnothing }}^{\omega }$. Since $w_n\vDash {\phi }_n$ but $w_n^{\prime }\vDash ̸{\phi }_n$ for all $n\ge 1$, we get that any presumed LTL-formula equivalent to ${\phi }_n$ needs to have size $2^n$ at least. $◀$

For convenience, we work with sMTL¹ formulas in negation normal form (NNF), i.e. those that are built from literals $q,\neg q$ using the Boolean operators $\wedge ,\vee$ and the temporal operators $𝚇,{𝚄}^1$ and ${𝚁}^1$ where $\phi {𝚁}_{\sim k}^1\psi :=\neg (\neg \phi {𝚄}_{\sim k}^1\neg \psi )$. The following is a standard observation about the ability to push negations inwards in formulas to obtain NNF.

The construction of a Streett automaton recognising $L(\phi )$ for some sMTL¹ formula $\phi$ in NNF then follows the same principles as the standard construction of a Büchi automaton for an LTL formula. Temporal operators are typically handled by unfolding, not just in automata-theoretic decision procedures. The term denotes the two equivalences

These can be extended to the temporal operators in sMTL¹ as follows. The proof is just by close inspection of the semantics of MTL¹.

A formula $\chi$ of the form on one of the left-hand sides in these equations is called a temporal formula and we use $\mathrm{𝑢𝑛𝑓}(\chi )$ to denote the corresponding right-hand side. Temporal formulas of the form $\phi {𝚄}_{\ge k}^1\psi$, i.e. Until-formulas whose metric parameter is a half-open interval to the right, are called critical.

Later on we will need a second observation about temporal formulas. The proof is straightforward from an inspection of the semantics of MTL¹. The lemma already holds for MTL in fact.

The Fischer-Ladner closure of a formula $\chi$ is a collection of all subformulas and perhaps others derived from them that may play a role in determining the truth of $\chi$ at some point in a word.

The key concept in an automata construction for sMTL¹ formulas is that of a Hintikka set – a set of formulas that is closed under propositional logic consequence. We need to refine the standard definition slightly in order to obtain the intended complexity bound in the end.

While the Fischer-Ladner closure of an ${\text{sMTL}}^1$ formula $\chi$ is generally exponential in $|\chi |$ and there are, thus, doubly exponentially many Hintikka sets, there are only singly exponentially many lean Hintikka sets.

Note that there are at most $𝒪(|\chi |)$ many formula schemes, i.e. members of $\mathrm{𝐹𝐿}(\chi )$ modulo concrete metric parameters. A lean set can then be seen as a mapping for each such formula scheme to a value in $\{\perp ,0,\mathrm{\dots },m(\chi )\}$, indicating (non-)inclusion in the set and giving a concrete parameter value for a temporal formula. Since $m(\chi )\in 2^{𝒪(|\chi |)}$ due to binary encoding, there are at most ${(2^{𝒪(|\chi |)})}^{𝒪(|\chi |)}=2^{𝒪({|\chi |}^2)}$ many lean (Hintikka) sets. $◀$

We are now in a position to define a Streett automaton of singly exponential size that recognises exactly the models of an sMTL¹ formula in NNF.

Fix an sMTL¹ formula $\chi$ in NNF over some finite $𝒫$. We will need three constructions on (lean) Hintikka sets for $\chi$. The first one collects all literals in a lean Hintikka set.

It can be seen as the extraction of a propositional formula determining the letter at a position in a word where all formulas in $\mathrm{\Phi }$ are supposed to be true. On the other hand,

collects all “leanifications” of Hintikka sets that are potential successors to $\mathrm{\Phi }$ in the sense that they contain all formula $\psi$ which $\mathrm{\Phi }$ needs to be true at the next position. The leanification $\mathrm{𝑙𝑛}(\mathrm{\Psi })$ of $\mathrm{\Psi }$ is obtained by successively replacing temporal formulas as follows until no further steps are applicable.

• $\mathrm{■}$

  If $\{\phi {𝚄}_{\le k}^1\psi ,\phi {𝚄}_{\le \mathrm{\ell }}^1\psi \}\subseteq \mathrm{\Psi }$ or $\{\phi {𝚁}_{\ge k}^1\psi ,\phi {𝚁}_{\ge \mathrm{\ell }}^1\psi \}\subseteq \mathrm{\Psi }$ for some $\phi ,\psi$ and then replace all occurrences of the latter that do not occur under the scope of a $𝚇$-operator by the former.

• $\mathrm{■}$

  If $\{\phi {𝚄}_{\ge k}^1\psi ,\phi {𝚄}_{\ge \mathrm{\ell }}^1\psi \}\subseteq \mathrm{\Psi }$ or $\{\phi {𝚁}_{\le k}^1\psi ,\phi {𝚁}_{\le \mathrm{\ell }}^1\psi \}\subseteq \mathrm{\Psi }$ for some $\phi ,\psi$ and then replace all occurrences of the former that do not occur under the scope of a $𝚇$-operator by the latter.

It should be clear that $\mathrm{𝑁𝑥𝑡𝑠}(\mathrm{\Phi })$ is indeed a set of lean Hintikka sets for $\chi$.

The important observation about the leanification process is the preservation of the semantics in a strong sense.

This is proved in a straight-forward induction on the structure of $\phi$. The only non-trivial cases are those of temporal formulas. These are covered by Lemma 12. Since leanification also replaces subformulas, we also need the fact that $\chi$ (and all its subformulas) are given in NNF. Hence, if $\vDash {\phi }^{\prime }\to \phi$ then also $\vDash \psi \to \psi [\phi /{\phi }^{\prime }]$ for any $\psi$, i.e. all formulas are monotonic. $◀$

The acceptance condition of the NSA ${𝒜}_{\chi }$ is determined by the set of all critical temporal formulas that can occur in lean Hintikka sets for $\chi$. However, unfolding decreases interval bounds by one, so the number of critical temporal formulas in $\mathrm{𝐹𝐿}(\chi )$ is exponential: if $\chi$ contains the subformula $\phi {𝚄}_{\ge k}^1\psi$ for some $k\in \mathbb{N}$, then $\mathrm{𝐹𝐿}(\chi )$ contains $\phi {𝚄}_{\ge h}^1\psi$ for all $h\le k$, i.e. exponentially many in $|\chi |$ because of binary encodings of interval bounds.

The exact interval bounds are irrelevant for the acceptance condition. It is only used to ensure that no critical temporal formula $\phi {𝚄}_{\ge k}^1\psi$ gets unfolded forever without ever satisfying its right argument $\psi$. We introduce the notion of a critical formula scheme $\phi {𝚄}_{\ge \ast }^1\psi$ and write $(\phi {𝚄}_{\ge \ast }^1\psi )\in \mathrm{\Phi }$ if there is some $k\in \mathbb{N}$ such that $(\phi {𝚄}_{\ge k}^1\psi )\in \mathrm{\Phi }$.

Note that there is no need to treat the other three kinds of temporal formulas in the same way. A temporal Release-formula is a greatest fixpoint, and unfolding it infinitely often is a legitimate way of determining its truth. A non-critical, temporal Until-formula of the form $\phi {𝚄}_{\le k}^1\psi$ cannot get unfolded infinitely often because each unfolding step decreases the metric parameter in it until it eventually becomes $0$, and the formula is replaced by $\psi$ anyway. Note that this is not the case for critical Until-formulas. Unfolding them still decreases the metric parameter. However, the leanification process can increase it again, whereas leanification for non-critical Until-formulas can only decrease it further.

Let $\{{\gamma }_1,\mathrm{\dots },{\gamma }_n\}$ be the set of all schemes of critical temporal Until-formulas in $\mathrm{𝐹𝐿}(\chi )$, i.e. ${\gamma }_i={\alpha }_i{𝚄}_{\ge \ast }^1{\beta }_i$ for some ${\alpha }_i,{\beta }_i$. We define the NSA ${𝒜}_{\chi }$ as $({\mathscr{H}}_{\mathrm{𝗅𝗇}}(\chi ),𝒫,I,\delta ,ℱ)$ where

• $\mathrm{■}$

  $I:=\{\mathrm{\Phi }\in {\mathscr{H}}_{\mathrm{𝗅𝗇}}(\chi )\mid \chi \in \mathrm{\Phi }\}$,

• $\mathrm{■}$

  $\delta :=\{(\mathrm{\Phi },\mathrm{𝑁𝑜𝑤}(\mathrm{\Phi }),\mathrm{\Psi })\mid \mathrm{\Psi }\in \mathrm{𝑁𝑥𝑡𝑠}(\mathrm{\Phi })\}$,

• $\mathrm{■}$

  $ℱ:=\{(F_1,G_1),\mathrm{\dots },(F_n,G_n)\}$ with $F_i:=\{\mathrm{\Phi }\mid {\gamma }_i\in \mathrm{\Phi }\}$ and $G_i:=\{\mathrm{\Phi }\mid {\beta }_i\in \mathrm{\Phi }\}$. Note that ${\beta }_i$ may contain other temporal formulas, so ${\beta }_i$ is to be understood as a scheme potentially, and ${\beta }_i\in \mathrm{\Phi }$ means that some formula deviating from ${\beta }_i$ in metric parameters only is contained in $\mathrm{\Phi }$.

The next two lemmas are devoted to the soundness and completeness of the construction.

Let $w=a_0{a}_1\mathrm{\dots }{(2^{𝒫})}^{\omega }$ be such that there is an accepting run $\rho ={\mathrm{\Phi }}_0,{\mathrm{\Phi }}_1,\mathrm{\dots }$ of ${𝒜}_{\chi }$ on $w$. By the construction of ${𝒜}_{\chi }$ we have (i) $\chi \in {\mathrm{\Phi }}_0$ and, for all $i\ge 0$, (ii) $a_i\vDash \mathrm{𝑁𝑜𝑤}({\mathrm{\Phi }}_i)$ and (iii) there is ${\mathrm{\Psi }}_{i+1}\in \mathscr{H}(\chi )$ such that $\psi \in {\mathrm{\Psi }}_{i+1}$ for all $𝚇\psi \in {\mathrm{\Phi }}_i$ and ${\mathrm{\Phi }}_{i+1}=\mathrm{𝑙𝑛}({\mathrm{\Psi }}_{i+1})\in \mathrm{𝑁𝑥𝑡𝑠}({\mathrm{\Phi }}_i)$.

We show by induction on the structure of formulas $\phi$ that for all $i\in \mathbb{N}$ and all $\phi \in {\mathrm{\Phi }}_i$ we have $w,i\vDash \phi$. For literals $q$ or $\neg q$ this follows immediately from (ii). For conjunctions and disjunctions this follows by the hypothesis for both conjuncts, resp. one disjunct and the fact that each ${\mathrm{\Phi }}_i$ is a lean Hintikka set that behaves like a Hintikka set in this case, i.e. it contains both conjuncts of a conjunction etc. This is the case because leanification replaces either none or all occurrences that are not under the scope of a $𝚇$-operator. Hence, a replacement takes place in a conjunction iff it takes place in both conjuncts etc.

Suppose $\phi$ is of the form $𝚇\psi$. Because of (iii), there is a ${\mathrm{\Psi }}_{i+1}\in \mathscr{H}(\chi )$ with $\psi \in {\mathrm{\Psi }}_{i+1}$ with ${\mathrm{\Phi }}_{i+1}=\mathrm{𝑙𝑛}({\mathrm{\Psi }}_{i+1})$. According to Lemma 16, there is ${\psi }^{\prime }\in {\mathrm{\Phi }}_{i+1}$ that is structurally not greater than $\psi$. Hence, we can apply the induction hypothesis to it and obtain $w,i+1\vDash {\psi }^{\prime }$. According to Lemma 16, we then also have $w,i+1\vDash \psi$ and therefore $w,i\vDash \phi$.

Suppose $\phi$ is of the form ${\psi }_1{𝚄}_{\le k}^1{\psi }_2$. By inspection of the unfolding rule (Lemma 11) and successive applications of the principles (ii) and (iii) with the same kind of reasoning using Lemma 16, we get some $k^{\prime }\le k$ and a sequence ${\mathrm{\Psi }}_{i+1},\mathrm{\dots },{\mathrm{\Psi }}_{i+k^{\prime }}$ of Hintikka sets such that ${\mathrm{\Phi }}_{i+j}=\mathrm{𝑙𝑛}({\mathrm{\Psi }}_{i+j})$, ${\psi }^{\prime }\in {\mathrm{\Psi }}_{i+k^{\prime }}$ for some ${\psi }^{\prime }$ with $\vDash {\psi }_2^{\prime }\to {\psi }_2$ and ${\psi }_h^{\prime \prime }\in {\mathrm{\Phi }}_{i+h}$ for some ${\psi }_0^{\prime \prime },\mathrm{\dots },{\psi }_{k^{\prime }-1}^{\prime \prime }$ such that $\vDash {\psi }_h^{\prime \prime }\to {\psi }_1$. Applying the induction hypothesis to ${\psi }_2^{\prime }$ at position $i+k^{\prime }$ and for ${\psi }_0^{\prime \prime },\mathrm{\dots },{\psi }_{k^{\prime }-1}^{\prime \prime }$ at positions $i,\mathrm{\dots },i+k^{\prime }-1$ shows that these are satisfied at the respective positions in $w$. Lemma 16 then yields $w,i+k^{\prime }\vDash {\psi }_2$ and $w,i+h\vDash {\psi }_1$ for all $h=0,\mathrm{\dots },k^{\prime }-1$. Thus, $w,i\vDash \phi$.

Suppose $\phi$ is of the form ${\psi }_1{𝚄}_{\ge k}^1{\psi }_2$. Note that it is a critical temporal formula in this case. We can apply the same reasoning as in the previous case using Lemmas 11 and 16. However, here the leanification process may replace metric parameters by larger ones. Hence, this alone does not guarantee the existence of a $k^{\prime }\ge k$ such that ${\psi }_2\in {\mathrm{\Phi }}_{i+k^{\prime }}$. This is where ${𝒜}_{\chi }$’s acceptance condition comes into place. Since $\rho$ is accepting, it must either contain finitely many lean Hintikka sets containing $\phi$ or infinitely many containing ${\psi }_2$. The latter case immediately implies the existence of such a $k^{\prime }\ge k$. The former case does so, too, by inspection of Lemma 11 and the construction of Hintikka sets. It is only possible to have (the scheme) $\phi$ finitely often only when some ${\mathrm{\Phi }}_{i+k^{\prime }}$ contains ${\psi }_1{𝚄}_{\ge k}^1{\psi }_2$ and therefore also ${\psi }_2$. The rest of this case is handled as the previous one.

The remaining two cases of temporal Release-formulas are also handled in a way that is analogous to those of the Until-formulas.

At last, (i) says that $\chi \in {\mathrm{\Phi }}_0$. By the reasoning above we then have $w,0\vDash \chi$, i.e. $w\in L(\chi )$ which completes the claim. $◀$

Suppose $w=a_0{a}_1\mathrm{\dots }\in L(\chi )$. We need to construct an accepting run ${\mathrm{\Phi }}_0,{\mathrm{\Phi }}_1,\mathrm{\dots }$ of ${𝒜}_{\chi }$ on $w$. To this end, we construct a sequence ${\mathrm{\Phi }}_0^{\prime },{\mathrm{\Phi }}_1^{\prime },\mathrm{\dots }$ via ${\mathrm{\Phi }}_i^{\prime }:=\{\phi \in \mathrm{𝐹𝐿}(\chi )\mid w,i\vDash \phi \}$. It is not hard to see that each ${\mathrm{\Phi }}_i^{\prime }$ is indeed a propositionally consistent Hintikka set. Moreover, if $𝚇\phi \in {\mathrm{\Phi }}_i$ then $\phi \in {\mathrm{\Phi }}_{i+1}$. This therefore determines a sequence of lean Hintikka sets by leanification: ${\mathrm{\Phi }}_i:=\mathrm{𝑙𝑛}({\mathrm{\Phi }}_i^{\prime })$ for all $i\ge 0$, forming a run $\rho ={\mathrm{\Phi }}_0,{\mathrm{\Phi }}_1,\mathrm{\dots }$.

It remains to be seen that it is indeed an accepting run. Take some critical Until-formula scheme $\gamma =\alpha {𝚄}_{\ge \ast }^1\beta$ and suppose that $\rho$ contains an infinite subsequence ${\mathrm{\Phi }}_{i_1},{\mathrm{\Phi }}_{i_2},\mathrm{\dots }$ with ${\gamma }_j:=(\alpha {𝚄}_{\ge k_j}^1\beta )\in {\mathrm{\Phi }}_{i_j}$ for all $j\ge 1$. By construction, we have $w,i_j\vDash {\gamma }_j$. By the semantics of MTL¹ there are $k_1^{\prime },k_2^{\prime },\mathrm{\dots }$ with $k_j^{\prime }\ge k_j$ such that $w,i_j+k_j^{\prime }\vDash \beta$ and, again, by construction $\beta \in {\mathrm{\Phi }}_{i_j+k_j^{\prime }}^{\prime }$. Since , the set $\{i_j+k_j^{\prime }\mid j\ge 1\}$ is infinite. Hence, the sequence ${\mathrm{\Phi }}_0^{\prime },{\mathrm{\Phi }}_1^{\prime },\mathrm{\dots }$ has an infinite subsequence in which every Hintikka set contains $\beta$. Then the run $\rho$ has an infinite subsequence in which every lean Hintikka set either contains $\beta$ itself or an instantiation of the scheme $\beta$. In any case, the run $\rho$ satisfies the Streett pair associated with $\gamma$. Since this is the case for any critical $\gamma$, $\rho$ is indeed accepting and so we have $w\in L({𝒜}_{\chi })$. $◀$

Putting all of the above together we obtain that MTL¹ is not just decidable but that its satisfiability problem is no worse than that of ordinary LTL (and therefore exponentially easier than that of MTL), even though there is an exponential succinctness gap between MTL¹ and LTL.

The lower bound is straightforwardly inherited from LTL. For the upper bound, note that every MTL¹ formula $\chi$ can be translated into an equivalent sMTL¹ formula in NNF at a linear blow-up only (Thm. 7 and Lemma 10). This can in turn be translated into an equivalent NSA (Lemmas 17 and 18) of exponential size in $|\chi |$ (Lemma 15). Language equivalence entails particularly that its language is non-empty iff $\chi$ is satisfiable. Non-emptiness for NSA can be decided in NLogSpace (Thm. 4) which is NPSpace measured in the size of $\chi$. Savitch’s Theorem [15] then gives a PSpace upper bound. $◀$