On the Expressiveness of Temporal Equilibrium Logic

Abstract

We investigate expressiveness issues of Temporal Equilibrium Logic (TEL), a promising nonmonotonic logical framework for temporal reasoning. TEL shares the syntax of standard linear temporal logic LTL, but its semantics is an orthogonal combination of the LTL semantics with the nonmonotonic semantics of Equilibrium Logic. We establish that TEL is more expressive than LTL, and captures a strict subclass of $\omega$-regular languages. We illustrate the expressive power of $\textsf {TEL}$ by showing that $\textsf {LTL}$-conformant planning, which is not expressible in $\textsf {LTL}$, can be instead expressed in $\textsf {TEL}$. Additionally, we provide a systematic study of the expressiveness comparison between the LTL semantics and the TEL semantics for various natural syntactical fragments.

An authors’ online version of this paper is available at https://www.dropbox.com/s/x0fnjzhjwira780/TEL%20Expression.pdf?dl=0. Its appendix includes proofs that are omitted here for lack of space.

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

1 Introduction

Answer Set Programming (ASP) is now well established as a successful paradigm for declarative programming, with its roots in the fields of knowledge representation (KR), logic programming, and nonmonotonic reasoning (NMR) [3]. An adequate and well-known logical foundation for ASP is provided by Equilibrium Logic [19, 20], a nonmonotonic extension of the superintuitionistic logic of here-and-there (HT) [17]. This provides useful logical tools for the metatheory of ASP and a framework for defining extensions of the basic ASP language, for example to arbitrary propositional and first-order theories, to languages with intensional functions, and to hybrid theories that combine classical and rule-based reasoning [7, 10, 14, 21].

ASP has been applied to a wide range of temporal reasoning problems, including prediction, planning, diagnosis and verification. However, since it is not an intrinsically temporal formalism, it suffers some important limitations. Most ASP solvers deal with finite domains, which hampers the solution of temporal reasoning problems dealing with unbounded time, like proving the non-existence of a plan. Temporal scenarios dealing with unbounded time are typically best suited for modal temporal logics, a fundamental framework for the specification of the dynamic behavior of reactive systems. However, standard modal temporal logics, such as propositional linear-time temporal logic LTL [22], are not designed to deal with many issues in KR. These logics (like classical logics) have a monotonic consequence relation, meaning that adding a formula to a theory never produces a reduction of its set of consequences. A monotonic logic cannot handle various commonsense reasoning tasks such as reasoning by default.

Temporal Equilibrium Logic ( TEL ). TEL was proposed by Cabalar and Vega [8] as a nonmonotonic temporal logic, able to capture temporal reasoning problems not representable in ASP. It is apparently the only nonmonotonic extension of a standard modal temporal logic (viz. LTL) that does not use additional operators or constructions.

TEL shares the syntax of standard LTL, but its semantics is an orthogonal combination of the LTL semantics with the nonmonotonic semantics of Equilibrium Logic. As for Equilibrium Logic, the non-monotonic semantics of TEL is based on a selection criterion (a kind of minimization) among the models of the intermediate monotonic temporal logic of Here-and-There (THT), a combination of LTL and the propositional superintuitionistic logic of Here-and-There (HT).

Many works have been dedicated to the theoretical study of TEL, and some tools have been developed for computing models of temporal programs under TEL semantics (see e.g. [5]). Theoretical key results include the use of TEL to translate action languages [8], an automata-theoretic approach for checking the existence of TEL models [4], a decidable criterion for proving strong equivalence of two TEL theories [6], and a systematic study of the computational cost of TEL satisfiability [2] (a problem which is in general Expspace-complete).

Our Contribution. We investigate expressiveness issues for the TEL framework. It is known [4] that like LTL, TEL allows to specify only $\omega$-regular temporal properties. As a first contribution, we show that TEL is in general more expressive than LTL. In particular, the class of $\textsf {TEL}$-definable languages strictly includes the class of LTL-definable languages and is strictly included in the class of $\omega$-regular languages. We also illustrate the expressive power of TEL by considering the problem of finding conformant plans for temporal goals in dynamic systems in the presence of incomplete information¹ when the goal and the system behavior are specified in LTL [9]. We show that this problem, which is not expressible in $\textsf {LTL}$ [9], can be instead expressed in $\textsf {TEL}$.

As an additional non-trivial theoretical contribution, we provide a systematic study of the expressiveness comparison between the LTL semantics and the TEL semantics for various natural syntactical fragments. The considered fragments are obtained by restricting the set of allowed temporal modalities and/or by imposing a bound on the nesting depth of temporal modalities. The expressive power of LTL semantics for these fragments has been made relatively clear by numerous researchers. Thus, since for some of these fragments, TEL satisfiability is known to be relatively tractable [2], the aim is also to understand what kind of temporal reasoning problems can be captured by these fragments under the TEL semantics. Furthermore, we consider the class of splittable temporal programs [5], a $\textsf {TEL}$ fragment which is known to be $\textsf {LTL}$-expressible and for which a solver has been implemented [5]. We show that a slight syntactical generalization of this fragment, obtained by relaxing a constraint on the use of temporal literals in the dynamic rules (intuitively ensuring that “the past does not depend on the future”), already leads to a fragment more expressive than $\textsf {LTL}$.

Some of the expressiveness results obtained also point to a peculiar difference between LTL and TEL: due to the interpretation of the implication connective, in TEL, a temporal modality cannot be expressed in terms of its ‘dual’ modality. Thus, in TEL, dual temporal modalities, such as $\textsf {F}$ (‘eventually’) and $\textsf {G}$ (‘always’), need to be considered independently from one another. This is illustrated by one of our results: while for the syntactical fragment whose allowed temporal modalities are $\textsf {F}$ and $\textsf {X}$ (‘next’), the TEL semantics is less expressive than the LTL semantics, for the dual fragment, the TEL semantics already allows one to express non-LTL-definable requirements.

Related Work. Several research areas of AI have combined modal temporal logics with formalisms from knowledge representation for reasoning about actions and planning (see e.g. [12]). Combinations of NMR with modal logics designed for temporal reasoning are much more infrequent in the literature. The few exceptions are typically modal action languages with a nonmonotonic semantics defined under some syntactical restrictions. Recently, an alternative to TEL has been introduced, namely, Temporal Answer Sets (TAS), which relies on dynamic linear-time temporal logic [16], a modal approach more expressive than LTL. However, while the non-monotonic semantics of TEL covers any arbitrary theory in the syntax of LTL, TAS uses a syntactic transformation that is only defined for theories with a rather restricted syntax. A framework unifying TEL and TAS has been proposed in [1].

2 Preliminaries

Let $\mathbb {N}$ be the set of natural numbers and for all $i,j\in \mathbb {N}$, let $[i,j] := \{h\in \mathbb {N}\mid i\le h \le j\}$. For an infinite word w over some alphabet and for all $i\ge 0$, w(i) is the $i^{th}$ symbol of w. Let P and $P'$ be two disjoint finite sets of atomic propositions. Given an infinite word w over $2^{P}$ and an infinite word $w'$ over $2^{P'}$, $w\oplus w'$ denotes the infinite word over $2^{P\cup P'}$ given by $w(0)\cup w'(0),w(1)\cup w'(1),\ldots$, and $w\oplus P'$ denotes the infinite word over $2^{P\cup P'}$ given by $w(0)\cup P',w(1)\cup P',\ldots$. A proposition p is flat in w if $p\in w(i)$ for all $i\ge 0$. Note that each proposition $p'\in P'$ is flat in $w\oplus P'$. We extend the operator $\oplus$ to $\omega$-languages $\mathcal {L}$ over $2^{P}$ in the obvious way: $\mathcal {L}\oplus P'$ denotes the $\omega$-language over $2^{P\cup P'}$ consisting of the infinite words of the form $w \oplus P'$ where $w\in \mathcal {L}$.

2.1 Temporal Equilibrium Logic

We recall the framework of Temporal Equilibrium Logic (TEL) [8]. TEL is defined by first introducing a monotonic and intermediate version of standard linear temporal logic LTL  [22], the so-called logic of Temporal Here-and-There (THT) [8]. The nonmonotonic semantics of TEL is then defined by introducing a criterion for selecting models of THT.

Syntax and Semantics of ${\mathbf {\mathsf{{THT}}}}$ . While the syntax of THT coincides with that of LTL, the semantics of THT is instead an orthogonal combination of the superintuitionistic propositional logic of Here-and-There (HT) [17] and LTL. Fix a finite set P of atomic propositions. The set of THT formulas $\varphi$ over P is defined by the following abstract syntax.

$$ \varphi := p \;\big |\;\bot \;\big |\;\varphi \vee \varphi \;\big |\;\varphi \wedge \varphi \;\big |\;\varphi \rightarrow \varphi \;\big |\;\textsf {X}\,\varphi \;\big |\;\varphi \,\textsf {U}\varphi \;\big |\;\varphi \,\textsf {R}\varphi $$

where $p\in P$ and $\textsf {X}$, $\textsf {U}$, and $\textsf {R}$, are the standard ‘next’, ‘until’, and ‘release’ temporal modalities. Negation is defined as $\lnot \varphi \,\mathop {=}\limits ^{\text {def}}\,\varphi \rightarrow \bot$ while $\top \,\mathop {=}\limits ^{\text {def}}\,\lnot \bot$. The classical temporal operators $\textsf {G}$ (‘always’) and $\textsf {F}$ (‘eventually’) can be defined in terms of $\textsf {U}$ and $\textsf {R}$ as follows: $\textsf {F}\varphi \,\mathop {=}\limits ^{\text {def}}\,\top \textsf {U}\varphi$ and $\textsf {G}\varphi \,\mathop {=}\limits ^{\text {def}}\,\bot \textsf {R}\varphi$. The size $|\varphi |$ of a formula $\varphi$ is the number of distinct subformulas of $\varphi$. The temporal depth of $\varphi$ is the maximum number of nested temporal modalities in $\varphi$.

Recall that LTL over P is interpreted on infinite words over $2^{P}$, called in the following ${{{\textsf {\textit{LTL}}}}}$ interpretations. By contrast, the semantics of THT is defined in terms of infinite words over $2^{P}\times 2^{P}$, which can also be viewed as pairs of LTL-interpretations. Formally, a ${{{\textsf {\textit{THT}}}}}$ interpretation is a pair $\textsf {M}= (\textsf {H},\textsf {T})$ consisting of two LTL interpretations: $\textsf {H}$ (the ‘here’ interpretation) and $\textsf {T}$ (the ‘there’ interpretation) such that

$$ \text {for all } i\ge 0,\text { } \textsf {H}(i)\subseteq \textsf {T}(i) $$

Intuitively, $\textsf {H}(i)$ represents the set of propositions which are true at position i, while $\textsf {T}(i){\setminus } \textsf {H}(i)$ is the set of propositions which may be true (i.e. which are not falsified in an intuitionistic sense). A THT interpretation $\textsf {M}= (\textsf {H},\textsf {T})$ is said to be total whenever $\textsf {H}=\textsf {T}$. In the following, for interpretation, we mean a THT interpretation. Given an interpretation $\textsf {M}= (\textsf {H},\textsf {T})$, a position $i\ge 0$, and a THT formula $\varphi$, the satisfaction relation $\textsf {M},i\,\models \,\varphi$ is inductively defined as follows:

$$ \begin{array}{lll} \textsf {M},i\,\nvDash \, \bot &{}&{}\\ \textsf {M},i\,\models \, p &{} \Leftrightarrow &{} \,p\in \textsf {H}(i)\\ \textsf {M},i\,\models \, \varphi \vee \psi &{} \Leftrightarrow &{} \text {either } \textsf {M},i\,\models \, \varphi \text { or } \textsf {M},i\,\models \, \psi \\ \textsf {M},i\,\models \, \varphi \wedge \psi &{} \Leftrightarrow &{} \textsf {M},i\,\models \, \varphi \text { and } \textsf {M},i\,\models \,\psi \\ \textsf {M},i\,\models \, \varphi \rightarrow \psi &{} \Leftrightarrow &{} \text {for all } \textsf {H}'\in \{\textsf {H},\textsf {T}\}, \text {either } (\textsf {H}',\textsf {T}),i\,\nvDash \, \varphi \text { or } (\textsf {H}',\textsf {T}),i\,\models \, \psi \\ \textsf {M},i\,\models \, \textsf {X}\varphi &{} \Leftrightarrow &{} \textsf {M},i+1\,\models \, \varphi \\ \textsf {M},i\,\models \, \varphi \,\textsf {U}\psi &{} \Leftrightarrow &{} \text {there is } j\ge i \text { so that } \textsf {M},j\,\models \, \psi \text { and } \text {for all } k\in [i,j-1],\, \textsf {M},k\,\models \,\varphi \\ \textsf {M},i\,\models \, \varphi \,\textsf {R}\psi &{} \Leftrightarrow &{} \text {for all } j\ge i, \text { either } \textsf {M},j\,\models \, \psi \text { or } \textsf {M},k\,\models \, \varphi \text { for some } k\in [i,j-1] \end{array} $$

We say that $\textsf {M}$ is a ($\textsf {THT}$) model of $\varphi$, written $\textsf {M}\,\models \, \varphi$, whenever $\textsf {M},0\,\models \,\varphi$. A $\textsf {THT}$ formula $\varphi$ is $\textsf {THT}$ satisfiable if it admits a $\textsf {THT}$ model. A formula $\varphi$ is $\textsf {THT}$ valid if every interpretation $\textsf {M}$ is a $\textsf {THT}$ model of $\varphi$. Note that the semantics of THT is defined similarly to that of LTL except for the clause for the implication connective $\rightarrow$ which must be checked in both the components $\textsf {H}$ and $\textsf {T}$ of $\textsf {M}$. As a consequence $\textsf {M},i \,\nvDash \, \varphi$ does not correspond to $\textsf {M},i \,\models \, \lnot \varphi$ (i.e., $\textsf {M},i \,\models \, \lnot \varphi$ implies that $\textsf {M},i \,\nvDash \, \varphi$, but the converse direction does not hold in general). However, if we restrict the semantics to total interpretations, $(\textsf {T},\textsf {T})\,\models \, \varphi$ corresponds to the satisfaction relation $\textsf {T}\,\models \, \varphi$ in LTL. More precisely, the LTL models $\textsf {T}$ of $\varphi$ correspond to the total interpretations $(\textsf {T},\textsf {T})$ which are $\textsf {THT}$ models of $\varphi$. With regard to $\textsf {THT}$ validity, a $\textsf {THT}$ valid formula is also an $\textsf {LTL}$ valid formula, but the converse in general does not hold. For example, the excluded middle axiom $\varphi \vee \lnot \varphi$ is not a valid $\textsf {THT}$ formula since, as highlighted above, for an interpretation $\textsf {M}=(\textsf {H},\textsf {T})$, $\textsf {M}\,\nvDash \, \varphi$ does not imply that $\textsf {M}\,\models \,\lnot \varphi$. Similarly, the temporal formulas $\textsf {F}\varphi \leftrightarrow \lnot \textsf {G}\lnot \varphi$ and $\varphi _1\textsf {U}\varphi _2 \leftrightarrow \lnot \varphi _1\textsf {R}\lnot \varphi _2$, which are well-known valid LTL formulas (and allow to express, in LTL, a temporal modality in terms of its dual modality), are not $\textsf {THT}$ valid formulas. Thus, in $\textsf {THT}$, dual temporal modalities, like $\textsf {F}$ and $\textsf {G}$, or $\textsf {U}$ and $\textsf {R}$, need to be considered independently from one another. The following proposition summarizes some observations made above, where we use $\models _\textsf {LTL}$ to denote the satisfaction relation in LTL.

Proposition 1

Let $(\textsf {H},\textsf {T})$ be an interpretation and $\varphi$ be a THT formula.

• 1. If $(\textsf {H},\textsf {T}),i\,\models \, \varphi$, then $(\textsf {T},\textsf {T}),i\,\models \,\varphi$ (for all $i\ge 0$).

• 2. $(\textsf {H},\textsf {T}),i\,\models \,\lnot \varphi$ iff $(\textsf {T},\textsf {T}),i\,\models \,\lnot \varphi$ (for all $i\ge 0$).

• 3. $(\textsf {T},\textsf {T})\,\models \,\varphi$ iff $\textsf {T}\models _\textsf {LTL} \varphi$.

The non-monotonic logic ${\mathbf {\mathsf{{TEL}}}}$ . This logic is obtained from THT by restricting the semantics to a subclass of models of the given formula, called temporal equilibrium models. For LTL interpretations $\textsf {H}$ and $\textsf {T}$, $\textsf {H}\sqsubseteq \textsf {T}$ means that $\textsf {H}(i) \subseteq \textsf {T}(i)$ for all $i\ge 0$, and $\textsf {H}\sqsubset \textsf {T}$ means that $\textsf {H}\sqsubseteq \textsf {T}$ and $\textsf {H}\ne \textsf {T}$.

Definition 1 (Temporal Equilibrium Model)

Given a THT formula $\varphi$, a (temporal) equilibrium model of $\varphi$ is a total model $(\textsf {T},\textsf {T})$ of $\varphi$ satisfying the following minimality requirement: whenever $\textsf {H}\sqsubset \textsf {T}$, then $(\textsf {H},\textsf {T})\,\nvDash \,\varphi$.

If we restrict the syntax to HT formulas (i.e., $\textsf {THT}$ formulas where no temporal modality is allowed) and the semantics to HT interpretations $(\textsf {H}(0),\textsf {T}(0))$, then (non-temporal) equilibrium models coincide with stable models of answer set programs in their most general form [13]. In particular, the interpretation of negation is that of default negation in logic programming: formula $\lnot \varphi$ holds ($\varphi$ is false by default) if there is no evidence regarding $\varphi$, i.e., $\varphi$ cannot be derived by the rules of the logic program. As a first example, let us consider the THT formula $\varphi$ given by $\varphi =\textsf {G}(\lnot p \rightarrow \textsf {X}p)$. Its intuitive meaning corresponds to the first-order logic program consisting of rules of the form $p(s(X)) \leftarrow \textit{not}\, p(X)$, where time has been reified as an extra parameter $X=0,s(0),s(s(0)),\ldots$. Thus, at any time instant, if there is no evidence regarding p, then p will become true at the next instant. Initially, we have no evidence regarding p, so this will imply $\textsf {X}p$. To derive $\textsf {X}\textsf {X}p$, the only possibility would be the rule $\lnot \textsf {X}p \rightarrow \textsf {X}\textsf {X}p$, an instance of $\varphi$. As the body of this rule is false, $\textsf {X}\textsf {X}p$ becomes false by default, and so on. It is easy to see that the unique equilibrium model of $\varphi$ is $((\emptyset \{p\})^{\omega },(\emptyset \{p\})^{\omega })$.

Note that an LTL satisfiable formula may have no temporal stable model. As an example, consider the formula $\varphi$ given by $\varphi =\textsf {G}(\lnot \textsf {X}p \rightarrow p) \wedge \textsf {G}(\textsf {X}p \rightarrow p)$. The unique LTL model is $\textsf {T}=\{p\}^{\omega }$. However, $(\textsf {T},\textsf {T})$ is not an equilibrium model of $\varphi$, since the interpretation $(\textsf {H},\textsf {T})$, where $\textsf {H}=(\emptyset )^{\omega }$ is a THT model of $\varphi$.

For a $\textsf {THT}$ formula $\varphi$, we denote by $\mathcal {L}_\textsf {TEL} (\varphi )$ (resp., $\mathcal {L}_\textsf {LTL} (\varphi )$) the $\omega$-language over $2^{P}$ consisting of the $\textsf {LTL}$ interpretations $\textsf {T}$ such that $(\textsf {T},\textsf {T})$ is an equilibrium model of $\varphi$ (resp., $\textsf {T}$ is an $\textsf {LTL}$ model of $\varphi$). Note that by Proposition 1, $\mathcal {L}_\textsf {TEL} (\varphi )\subseteq \mathcal {L}_\textsf {LTL} (\varphi )$. A $\textsf {TEL}$ language (resp., $\textsf {LTL}$ language) is an $\omega$-language of the form $\mathcal {L}_\textsf {TEL} (\varphi )$ (resp., $\mathcal {L}_\textsf {LTL} (\varphi )$) for some $\textsf {THT}$ formula $\varphi$. We now observe the following.

Remark 1

$\textsf {LTL}$-definable languages are $\textsf {TEL}$-definable.

Indeed, by Proposition 1, the set of $\textsf {LTL}$ models of a $\textsf {THT}$ formula $\varphi$ over P corresponds to the set of $\textsf {TEL}$ models of $\varphi \wedge \psi _\textit{Tot}(P)$, where formula $\psi _\textit{Tot}(P)$ (we exploit this formula in many parts of the paper) captures, under the $\textsf {THT}$ semantics, the total interpretations over P.

$$ \psi _\textit{Tot}(P):=\displaystyle {\bigwedge _{p\in P}\textsf {G}(p\vee \lnot p)} $$

Next, we observe that like $\textsf {LTL}$, the class of languages definable by $\textsf {TEL}$ is strictly included in the class of $\omega$-regular languages. Indeed, by [4], every $\textsf {TEL}$ language is effectively $\omega$-regular. Moreover, let us consider the $\omega$ -regular language $\mathcal {L}_\textit{even}$ consisting of the $\textsf {LTL}$ interpretations $\textsf {T}$ over $P=\{a\}$ of the form $\emptyset ^{2n}\cdot \{a\} \cdot \emptyset ^{\omega }$ for some $n\ge 0$ (where the maximal prefix preceding the unique a-position has even length). One can trivially check that $\mathcal {L}_\textit{even}$ is not $\textsf {TEL}$ definable. Hence:

Proposition 2

The class of $\textsf {TEL}$ languages is strictly included in the class of $\omega$-regular languages.

2.2 Problems Investigated and Summary of the Main Results

In this paper, we compare the expressive power of the $\textsf {LTL}$ semantics and the $\textsf {TEL}$ semantics for full $\textsf {THT}$ and various syntactical $\textsf {THT}$ fragments.

In particular, we consider the syntactical fragments of THT obtained by restricting the set of allowed temporal modalities and/or by bounding the temporal depth. Formally, given $O_1,O_2,\ldots \in \{\textsf {X},\textsf {F},\textsf {G},\textsf {U},\textsf {R}\}$, we denote by $\textsf {THT}(O_1,O_2,\ldots )$ the fragment of $\textsf {THT}$ for which only the temporal modalities $O_1,O_2,\ldots$ are allowed. For $k\ge 0$, $\textsf {THT}_k(O_1,O_2,\ldots )$ denotes the fragment of $\textsf {THT}(O_1,O_2,\ldots )$ where the temporal depth is at most k. We write nothing for k when no bound is imposed. For instance, $\textsf {THT}_2(\textsf {G})$ denotes the fragment where the unique allowed temporal modality is $\textsf {G}$ and the temporal depth is at most 2. We also consider a syntactical fragment of $\textsf {THT}$, we call splittable $\textsf {THT}$, corresponding to a generalization of splittable temporal programs introduced in [5]. A temporal literal is either an ordinary literal or a literal preceded by the next operator $\textsf {X}$. A splittable $\textsf {THT}$ formula is a conjunction of formulas of the following types:

• Initial rules: a formula of the form $B \rightarrow H$, where B is a conjunction of temporal literals and H is a disjunction of temporal literals.

• Dynamic rules: formulas of the form $\textsf {G}\,r$, where r is an initial rule.

• Constraints: formulas of the form $\lnot \varphi$ for arbitrary $\textsf {THT}$ formulas $\varphi$ (such formulas impose constraints only on the ‘there’ part of an interpretation).

Fig. 1.

Expressive comparison between $\textsf {TEL}$ fragments and full $\textsf {LTL}$

For two $\textsf {THT}$ fragments $\mathcal {F}$ and $\mathcal {F'}$ and $\mathcal {S},\mathcal {S'}\in \{\textsf {LTL},\textsf {TEL} \}$, we say that $\mathcal {F}$ under the $\mathcal {S}$-semantics is subsumed by $\mathcal {F'}$ under the $\mathcal {S}'$-semantics, written $(\mathcal {F})_\mathcal {S}\le (\mathcal {F}')_{\mathcal {S}'}$, if for each $\mathcal {F}$-formula $\varphi$, there is a $\mathcal {F}'$-formula $\varphi '$ s.t. $\mathcal {L}_{\mathcal {S}'}(\varphi ')=\mathcal {L}_\mathcal {S}(\varphi )$. Moreover, $\mathcal {F}'$ under the $\mathcal {S}'$-semantics is more expressive than $\mathcal {F}$ under the $\mathcal {S}$-semantics, denoted by $(\mathcal {F})_\mathcal {S}< (\mathcal {F}')_{\mathcal {S}'}$, if $(\mathcal {F})_\mathcal {S}\le (\mathcal {F}')_{\mathcal {S}'}$ but not $(\mathcal {F}')_{\mathcal {S}'}\le (\mathcal {F})_{\mathcal {S}}$. Additionally, we say that $\mathcal {F}$ under the $\mathcal {S}$-semantics is expressively incomparable with $\mathcal {F'}$ under the $\mathcal {S}'$-semantics, written $(\mathcal {F}')_\mathcal {S}'\,\bot \, (\mathcal {F})_{\mathcal {S}}$, if neither $(\mathcal {F})_\mathcal {S}\le (\mathcal {F}')_{\mathcal {S}'}$ nor $(\mathcal {F}')_\mathcal {S}'\le (\mathcal {F})_{\mathcal {S}}$. Sometime, we simply write $\textsf {LTL}$ to mean $(\textsf {THT})_\textsf {LTL}$.

Figure 1 summarises some of the obtained results concerning the expressiveness comparison between the considered $\textsf {THT}$ fragments under the $\textsf {TEL}$ semantics and full $\textsf {THT}$ under the $\textsf {LTL}$ semantics.

3 Expressing ${{\mathbf {\mathsf{{LTL}}}}}$-conformant Planning in ${{\mathbf {\mathsf{{TEL}}}}}$

In this section, we illustrate the expressive power of $\textsf {TEL}$ by showing that the $\textsf {LTL}$-conformant planning problem considered in [9], which is not expressible in $\textsf {LTL}$ [9], can be instead expressed in $\textsf {TEL}$. Some other approaches in ASP for the formalization of conformant planning can be reformulated in the $\textsf {LTL}$-conformant planning framework such as the one based on Gelfond’s action language [15].

In the context of reasoning about actions and planning, we consider a setting where we have incomplete information on the dynamic system and the knowledge about the system is represented in $\textsf {LTL}$. In particular, the system is described by introducing a set of atomic facts, called fluents, whose truth value changes as the system evolves, and by specifying through $\textsf {LTL}$ the effects of actions on such a set of facts. Thus, we consider two disjoint finite sets of atomic propositions: F – the set of fluents – and A – the set of actions. The behavior of the given system is specified by an $\textsf {LTL}$ formula $\varphi _s$ over $A\cup F$ which describes the set of possible evolutions of the system, each of which is represented as an infinite sequence of situations, where transitions from one situation to the next are caused by actions. Note that with this formalization, we may have incomplete information both on the initial situation and on the actual effects of actions so that, given a sequence of actions, we will have multiple possible evolutions, one of which is the actual one. The $\textsf {LTL}$-conformant planning problem consists in constructing a plan, i.e. a sequence of actions that guarantees the satisfaction of a temporal goal expressed in $\textsf {LTL}$ whenever the conditions specified by $\varphi _s$ are satisfied.

Formally, the $\textsf {LTL}$-conformant planning problem is the problem of finding, given two $\textsf {LTL}$ formulas $\varphi _s$ and $\varphi _g$ over $A\cup F$ (representing the system specification and the temporal goal, respectively), an infinite sequence $\textsf {T}_A = \{a_0\},\{a_1\},\ldots$ of actions such that for all $\textsf {LTL}$ interpretations $\textsf {T}_F$ over F (i.e. for all the possible infinite sequences of truth assignments to fluents), it holds that

$$ \textsf {T}_A\oplus \textsf {T}_F \,\models \,\varphi _s \rightarrow \varphi _g $$

Let $\textit{Con}(\varphi _s,\varphi _g)$ be the set of such conformant plans $\textsf {T}_A$. Such a set cannot be in general expressed in $\textsf {LTL}$ [9]. Here, we show that, unless an additional set of flat propositions, $\textit{Con}(\varphi _s,\varphi _g)$ can be instead expressed in $\textsf {TEL}$. We construct in linear-time a $\textsf {THT}$ formula $\varphi _\textit{con}$ whose set of equilibrium models corresponds to $\textit{Con}(\varphi _s,\varphi _g)\oplus F'$, where $F' = F\cup \{u\}$, and u is a fresh (dummy) proposition non in $A\cup F$.

Before defining $\varphi _\textit{con}$, we need additional definitions. A $\textsf {THT}$ formula is in negation normal form (NNF) if the implication connective occurs only as negation and, additionally, negation is applied only to atomic propositions. By using De Morgan’s laws, the duality between $\textsf {U}$ and $\textsf {R}$, and the fact that in $\textsf {LTL}$, $\xi _1 \rightarrow \xi _2$ can be rewritten as $\lnot \xi _1\vee \xi _2$, we can convert the $\textsf {THT}$ formula $\lnot (\varphi _s \rightarrow \varphi _g)$ into a $\textsf {THT}$ formula $\overline{\psi }_{sg}$ in $\textit{NNF}$ having the same set of $\textsf {LTL}$ models.

Let $K_u(\overline{\psi }_{sg})$ be the $\textsf {THT}$ formula obtained from the $\textit{NNF}$ formula $\overline{\psi }_{gs}$ by replacing each occurrence of a negative literal $\lnot p$ with $p \rightarrow u$. Intuitively, $p \rightarrow u$ is used to express negation on the ‘here’ part $\textsf {H}$ of an interpretation $(\textsf {H},\textsf {T})$ such that u is flat in $\textsf {T}$ and $u\notin \textsf {H}(i)$ for all $i\ge 0$. Formally, one can easily show by structural induction that for such an interpretation, $(\textsf {H},\textsf {T})\,\models \, K_u(\overline{\psi }_{gs})$ iff $\textsf {H}\models _\textsf {LTL} \overline{\psi }_{gs}$. Hence, $(\textsf {H},\textsf {T})\,\models \,K_u(\overline{\psi }_{gs})$ iff $\textsf {H}\,\nvDash \,_\textsf {LTL} \varphi _s \rightarrow \varphi _g$.

The $\textsf {THT}$ formula $\varphi _\textit{con}$ over $A\cup F'$ is then defined as follows:

$$ \begin{array}{lcl} \varphi _\textit{con} &{} := &{} \displaystyle {\textsf {G}(\bigvee _{a\in A}(a\wedge \bigwedge _{a'\in A{\setminus } \{a\}} \lnot \,a)) \,\wedge \, (\psi _\textit{Tot}\,(A\cup F') \rightarrow \bigwedge _{p\in F'}\textsf {G}p)\,\wedge }\\ &{}&{} \displaystyle {(\textsf {F}u \rightarrow \psi _\textit{Tot}\,(A\cup F')) \,\wedge \, (u \vee K_u(\overline{\psi }_{gs}))} \end{array} $$

The first conjunct captures the $\textsf {THT}$ interpretations $(\textsf {H},\textsf {T})$ such that $\textsf {H}$ and $\textsf {T}$ agree over the set A of actions, and exactly one action occurs at any timestamp. The second and third conjuncts ensure that every proposition in $F'=F\cup \{u\}$ is flat in $\textsf {T}$ and whenever $\textsf {H}\ne \textsf {T}$, $u\notin \textsf {H}(i)$ for every $i\ge 0$. Finally, the last conjunct is fulfilled iff whenever $\textsf {H}\ne \textsf {T}$, $\textsf {H}\models _\textsf {LTL} K_u(\overline{\psi }_{gs})$. Formally, the following holds, which proves the result (for details see the online version of this paper at https://www.dropbox.com/s/x0fnjzhjwira780/TEL%20Expression.pdf?dl=0).

Claim. $\mathcal {L}_\textsf {TEL} (\varphi _\textit{con} ) = \textit{Con}(\varphi _s,\varphi _g)\oplus F'$.

4 Maximal Fragments Expressible in LTL

In this section, we individuate maximal $\textsf {THT}$ fragments which under the $\textsf {TEL}$ semantics are subsumed by full $\textsf {LTL}$.

The fragment ${\mathbf {\mathsf{{THT(F,G)}}}}$ . We show that full $\textsf {THT}$ under the $\textsf {LTL}$ semantics is more expressive than the fragment $\textsf {THT}(\textsf {F},\textsf {G})$ under the $\textsf {TEL}$ semantics. On the other hand, we additionally establish that for the considered fragment, the $\textsf {TEL}$ semantics is more expressive than the $\textsf {LTL}$ semantics. For the first result, we exploit a well-known characterization of the $\omega$-regular languages which are LTL-expressible [18, 24]. In the following, we also consider finite ($\textsf {THT}$) interpretations which are non-empty prefixes of ($\textsf {THT}$) interpretations.

Definition 2

( N -stutter Closure [18, 24]). For $N\ge 1$, an $\omega$-language $\mathcal {L}$ over an alphabet $\Sigma$ is N -stutter closed if for all finite words x, y, u, w and infinite words v over $\Sigma$,

$$\begin{aligned} \begin{array}{l} u\cdot w^{N}\cdot v\in \mathcal {L}\textit{ iff } u\cdot w^{N+1}\cdot v\in \mathcal {L}\\[2mm] x\cdot (u\cdot w^{N}\cdot y)^{\omega }\in \mathcal {L}\textit{ iff } x\cdot (u\cdot w^{N+1}\cdot y)^{\omega }\in \mathcal {L}\end{array} \end{aligned}$$

Proposition 3

([18, 24]). If $\mathcal {L}$ is an $\omega$-regular language over $2^{P}$ which is N-stutter closed for some $N\ge 1$, then $\mathcal {L}$ is LTL-expressible.

For $\varphi \in \textsf {THT}(\textsf {F},\textsf {G})$, let $N_\varphi := n^{2}(h+1)^{2^{n}}$, where $n= 2^{2|P|}$ and h is the temporal depth of $\varphi$. We demonstrate that the language $\mathcal {L}_\textsf {TEL} (\varphi )$ is $N_\varphi$-stutter closed. For this, we use an additional notion, we call h-bisimilarity.

Definition 3

( h -bisimilarity). Let w and $w'$ be two finite words over an alphabet $\Sigma$ and i and $i'$ be two positions of w and $w'$, respectively. Given $h\ge 0$, (w, i) and $(w',i')$ are h -bisimilar if $w(i)=w'(i')$ and whenever $h>0$, then:

• for all $i\le j < |w|$ (resp., $i'\le j'<|w'|$ $)$, there exists $i'\le j'<|w'|$ (resp., $i\le j < |w|$) such that (w, j) and $(w',j')$ are $(h-1)$-bisimilar.

We say that w and $w'$ are h-bisimilar if (w, 0) and $(w',0)$ are h-bisimilar.

For each $h\ge 0$, a formula in $\textsf {THT}_h(\textsf {F},\textsf {G})$ cannot distinguish under the THT semantics two interpretations where one is obtained from the other one by replacing finite segments with h-bisimilar ones. Formally, we establish the following result.

Lemma 1

Let $h\ge 0$, $\varphi \in \textsf {THT}_h(\textsf {F},\textsf {G})$, and $\textsf {N}$ and $\textsf {N}\,'$ be two finite h-bisimilar interpretations. For all finite interpretations $\textsf {M}_1,\textsf {M}_2,\textsf {M}_3$ and infinite interpretations $\textsf {M}_4$,

$$ \begin{array}{l} \textsf {M}_1 \textsf {N}\textsf {M}_4\,\models \, \varphi \textit{ iff } \textsf {M}_1 \textsf {N}\,' \textsf {M}_4\,\models \, \varphi \\ \textsf {M}_1 (\textsf {M}_2\textsf {N}\textsf {M}_3)^{\omega }\,\models \, \varphi \textit{ iff } \textsf {M}_1 (\textsf {M}_2\textsf {N}\,' \textsf {M}_3)^{\omega }\,\models \, \varphi \end{array} $$

The following lemma is based on a counting argument, asserts that for all $h\ge 1$ and finite interpretations consisting of concatenations of N segments, where $N\ge n^{2}(h+1)^{2^{n}}$ and $n= 2^{2|P|}$, there always exists a segment whose removal or pumping preserves h-bisimilarity.

Lemma 2

Let $h\ge 1$ and $\textsf {M}$ be a finite interpretation of the form $\textsf {M}= \textsf {M}_1 \ldots \textsf {M}_N$ such that $N\ge n^{2}(h+1)^{2^{n}}$, where $n= 2^{2|P|}$. Then,

• for some $j\in [1,N]$, $\textsf {M}$ and $\textsf {M}\,'=\textsf {M}_1 \ldots \textsf {M}_{j-1}\cdot \textsf {M}_{j+1}\ldots \textsf {M}_{N}$ are h-bisimilar. Moreover, $\textsf {M}\,'$ is non-total if $\textsf {M}$ is non-total.

• for some $j\in [1,N]$, $\textsf {M}$ and $\textsf {M}_1 \ldots \textsf {M}_{j}\cdot \textsf {M}_{j}\cdot \textsf {M}_{j+1}\ldots \textsf {M}_{N}$ are h-bisimilar.

By Lemmas 1 and 2, we deduce the desired result.

Theorem 1

For each $\varphi \in \textsf {THT}(\textsf {F},\textsf {G})$, $\mathcal {L}_\textsf {TEL} (\varphi )$ is $N_\varphi$-stutter closed.

Proof

Let $\varphi \in \textsf {THT}(\textsf {F},\textsf {G})$ and h be the temporal height of $\varphi$. We assume that $h>0$ (otherwise, the result is obvious). Recall that $N_\varphi = n^{2}(h+1)^{2^{n}}$, where $n= 2^{2|P|}$. Let $\textsf {T}$ and $\textsf {T}'$ be two LTL interpretations such that

$$ \begin{array}{l} \textsf {T}= u \cdot w^{N} \cdot v \textit{ and } \textsf {T}' = u \cdot w^{N+1} \cdot v\\ (\text {resp., }\textsf {T}= x \cdot (u \cdot w^{N} \cdot y)^{\omega } \textit{ and } \textsf {T}' = x \cdot (u \cdot w^{N+1} \cdot y)^{\omega }) \end{array} $$

for some finite words x, u, y, w and infinite words v, where $N\ge N_\varphi$ and $n= 2^{2|P|}$. We show that $\textsf {T}\in \mathcal {L}_\textsf {TEL} (\varphi )$ iff $\textsf {T}'\in \mathcal {L}_\textsf {TEL} (\varphi )$. By Lemma 2, $w^{N}$ and $w^{N+1}$ are h-bisimilar. Thus, by Lemma 1, $(\textsf {T},\textsf {T})$ is a THT model of $\varphi$ iff $(\textsf {T}',\textsf {T}')$ is a THT model of $\varphi$. We prove the following, hence, the result follows:

• 1. for all $\textsf {H}\sqsubset \textsf {T}$, there is $\textsf {H}' \sqsubset \textsf {T}'$ such that $(\textsf {H},\textsf {T})\,\models \,\varphi$ iff $(\textsf {H}',\textsf {T}')\,\models \,\varphi$.

• 2. for all $\textsf {H}' \sqsubset \textsf {T}'$, there is $\textsf {H}\sqsubset \textsf {T}$ such that $(\textsf {H},\textsf {T})\,\models \,\varphi$ iff $(\textsf {H}',\textsf {T}')\,\models \,\varphi$.

We focus on Condition 1 (the proof of Condition 2 being similar). Let $\textsf {H}\sqsubset \textsf {T}$ and $\textsf {M}=(\textsf {H},\textsf {T})$. Assume that $\textsf {T}= u \cdot w^{N} \cdot v$ (the other case, where $\textsf {T}= x \cdot (u \cdot w^{N} \cdot y)^{\omega }$, being similar). Then, $\textsf {M}$ can be written in the form $\textsf {M}=\textsf {M}_1\, \textsf {N}_1\ldots \textsf {N}_N\,\textsf {M}_2$ such that $|\textsf {M}_1|=|u|$ and $|\textsf {N}_i|=|w|$ for all $i\in [1,N]$. By Lemma 2, there exists $j\in [1,N]$ such that $\textsf {N}_1\,\ldots \,\textsf {N}_N$ is h-bisimilar to $\textsf {N}_1\,\ldots \,\textsf {N}_j\cdot \textsf {N}_j\,\textsf {N}_{j+1}\ldots \textsf {N}_N$. Let $\textsf {M}' =\textsf {M}_1 \textsf {N}_1\,\ldots \,\textsf {N}_j\, \textsf {N}_j\,\textsf {N}_{j+1}\ldots \textsf {N}_N\,\textsf {M}_2$. Since $\textsf {M}$ is non-total, $\textsf {M}'$ is non-total too, and by Lemma 1, $\textsf {M}\,\models \,\varphi$ iff $\textsf {M}'\,\models \,\varphi '$. Moreover, since $\textsf {T}' =u \cdot w^{N+1} \cdot v$, the non-total interpretation $\textsf {M}'$ is of the form $(\textsf {H}',\textsf {T}')$, and we are done. $\square$

We now establish the main result for the fragment $\textsf {THT}(\textsf {F},\textsf {G})$.

Theorem 2

$(\textsf {THT}(\textsf {F},\textsf {G}))_\textsf {TEL} < \textsf {LTL}$ and $(\textsf {THT}(\textsf {F},\textsf {G}))_\textsf {TEL} > (\textsf {THT}(\textsf {F},\textsf {G}))_\textsf {LTL}$.

Proof

One can easily show that the $\textsf {LTL}$-expressible $\omega$-language consisting of the $\textsf {LTL}$ interpretation $\emptyset \cdot \{a\}\cdot \emptyset ^{\omega }$ cannot be expressed by any $\textsf {THT}(\textsf {F},\textsf {G})$ formula under the $\textsf {TEL}$ semantics. Thus, since $\textsf {TEL}$ languages are $\omega$-regular, by Proposition 3 and Theorem 1, we obtain that $(\textsf {THT}(\textsf {F},\textsf {G}))_\textsf {TEL} < \textsf {LTL}$. For the second part of the theorem, first, we observe that for a $\textsf {THT}(\textsf {F},\textsf {G})$ formula $\varphi$, the set of $\textsf {LTL}$ models of $\varphi$ corresponds to the set of $\textsf {TEL}$ models of the $\textsf {THT}(\textsf {F},\textsf {G})$ formula $\varphi \wedge \psi _\textit{Tot}(P)$. Hence, $(\textsf {THT}(\textsf {F},\textsf {G}))_\textsf {TEL} \ge (\textsf {THT}(\textsf {F},\textsf {G}))_\textsf {LTL}$. It remains to show that $(\textsf {THT}(\textsf {F},\textsf {G}))_\textsf {TEL} \not \le (\textsf {THT}(\textsf {F},\textsf {G}))_\textsf {LTL}$. For this, let $P=\{b,u\}$ and $(\textsf {T}_1,\textsf {T}_1)$ and $(\textsf {T}_2,\textsf {T}_2)$ be two total interpretations defined as follows: $\textsf {T}_1 =\{u\}\{b,u\}^{2}\{u\}^{\omega }$ and $\textsf {T}_2 = \{u\}\{b,u\}\{u\}^{\omega }$. No $\textsf {THT}(\textsf {F},\textsf {G})$ formula can distinguish $\textsf {T}_1$ and $\textsf {T}_2$ under the $\textsf {LTL}$ semantics. On the other hand, we show that there exists a $\textsf {THT}_1(\textsf {F},\textsf {G})$ formula $\varphi$ such that $(\textsf {T}_2,\textsf {T}_2)$ is a $\textsf {TEL}$ model of $\varphi$, and $(\textsf {T}_1,\textsf {T}_1)$ is not.

$$ \text {Let } \varphi :=\textsf {G}(\lnot \lnot u) \wedge \textsf {F}b \wedge (\textsf {F}u \rightarrow \psi _\textit{Tot}(P)) \wedge \textsf {F}((b \rightarrow u) \wedge \lnot \lnot b) $$

Under the $\textsf {THT}$ semantics, the first three conjuncts capture the interpretations $(\textsf {H},\textsf {T})$ such that (i) for all $i\ge 0$, $u\in \textsf {T}(i)$, (ii) if $\textsf {H}\ne \textsf {T}$, then for all $i\ge 0$, $u\notin \textsf {H}(i)$, and (iii) there is $h\ge 0$ such that $b\in \textsf {H}(h)$. Additionally, the fourth conjunct is fulfilled whenever either $\textsf {T}=\textsf {H}$, or there is $k\ge 0$ such that $b\notin \textsf {H}(k)$ and $b\in \textsf {T}(k)$. It easily follows that the set of $\textsf {TEL}$ models of $\varphi$ is $\{ u\}^{*}\cdot \{b,u\}\cdot \{u\}^{\omega }$, where there is exactly one occurrence of $\{b,u\}$, and the result follows.$\square$

The fragment ${\mathbf {\mathsf{{THT(X,F)}}}}$ . For the fragment $\textsf {THT}(\textsf {X},\textsf {F})$, we crucially use the following known result [2], where for a total interpretation $(\textsf {T},\textsf {T})$, a position $i\ge 0$ is non-empty in $(\textsf {T},\textsf {T})$ if $\textsf {T}(i)\ne \emptyset$.

Lemma 3

([2]). Let $\varphi$ be a $\textsf {THT}(\textsf {X},\textsf {F})$ formula. Then, every equilibrium model of $\varphi$ has at most $|\varphi |^{2}$ non-empty positions.

Since there are $\textsf {THT}(\textsf {X},\textsf {F})$ formulas whose $\textsf {LTL}$ models contain infinite occurrences of non-empty positions (for example, the formula $\lnot \textsf {F}\lnot p$), by Lemma 3 we easily deduce the following result.

Theorem 3

Given a $\textsf {THT}(\textsf {X},\textsf {F})$ formula $\varphi$, one can build a $\textsf {THT}(\textsf {X},\textsf {F})$ formula $\psi$ such that $\mathcal {L}_\textsf {LTL} (\psi ) =\mathcal {L}_\textsf {TEL} (\varphi )$. Moreover, $(\textsf {THT}(\textsf {X},\textsf {F}))_\textsf {TEL} < (\textsf {THT}(\textsf {X},\textsf {F}))_\textsf {LTL}$.

The fragment ${\mathbf {\mathsf{{THT}}}}_1$ . For the fragment $\textsf {THT}_1$, where there is no nesting of temporal modalities, we first establish the following result.

Theorem 4

Given a $\textsf {THT}_1$ formula $\varphi$, one can construct a $\textsf {THT}$ formula whose $\textsf {LTL}$ models correspond to the $\textsf {TEL}$ models of $\varphi$.

Sketched Proof. For the fixed finite set P of atomic propositions, it is possible to define an equivalence relation of finite index on total interpretations such that the following holds: (1) each equivalence class C is finitely representable and no $\textsf {THT}_1$ formula over P can distinguish elements of C under the $\textsf {TEL}$ semantics, (2) given an equivalence class C and a $\textsf {THT}_1$ formula $\varphi$ over P, one can effectively check whether C is associated with $\textsf {TEL}$ models of $\varphi$, and (3) each equivalence class C is effectively $\textsf {LTL}$-characterizable. $\square$

The construction in Theorem 4 cannot be done remaining in $\textsf {THT}_1$. Indeed, the following holds.

Theorem 5

$(\textsf {THT}_1)_\textsf {TEL} < \textsf {LTL}$ and $(\textsf {THT}_1)_\textsf {TEL} > (\textsf {THT}_1)_\textsf {LTL}$.

Proof

Let us consider the $\textsf {LTL}$-expressible $\omega$-language consisting of the $\textsf {LTL}$ interpretation $\emptyset ^{3} \cdot \{a\}\cdot \emptyset ^{\omega }$. One can easily show that such a language cannot be expressed by any $\textsf {THT}_1$ formula under the $\textsf {TEL}$ semantics. Thus, by Theorem 4, we obtain that $(\textsf {THT}_1)_\textsf {TEL} < \textsf {LTL}$. For the second part of the theorem, first, we observe that for a $\textsf {THT}_1$ formula $\varphi$, the set of $\textsf {LTL}$ models of $\varphi$ corresponds to the set of $\textsf {TEL}$ models of the $\textsf {THT}_1$ formula $\varphi \wedge \psi _\textit{Tot}(P)$. Hence, $(\textsf {THT}_1)_\textsf {TEL} \ge (\textsf {THT}_1)_\textsf {LTL}$. It remains to show that there exists a $\textsf {THT}_1$ formula whose set of $\textsf {TEL}$ models cannot be captured by any $\textsf {THT}_1$ formula under the $\textsf {LTL}$ semantics. For this, let $P=\{b,u\}$, $\textsf {T}_1 = \{u\}\{b,u\}^{2}\{u\}^{\omega }$, and $\textsf {T}_2 = \{u\}\{b,u\}\{u\}^{\omega }$. Evidently, no $\textsf {THT}_1$ formula can distinguish $\textsf {T}_1$ and $\textsf {T}_2$ under the $\textsf {LTL}$ semantics. On the other hand, by the proof of Theorem 2, there exists a $\textsf {THT}_1(\textsf {F},\textsf {G})$ formula $\varphi$ such that $(\textsf {T}_2,\textsf {T}_2)$ is a $\textsf {TEL}$ model of $\varphi$, and $(\textsf {T}_1,\textsf {T}_1)$ is not. Hence, the result follows.$\square$

5 ${{\mathbf {\mathsf{{TEL}}}}}$ Fragments Non-subsumed by LTL

In this section, we derive an almost complete picture of the $\textsf {TEL}$ fragments (w.r.t. the considered $\textsf {THT}$ syntactical hierarchy) which are expressively incomparable with LTL. We also show that under the $\textsf {TEL}$ semantics, the fragment $\textsf {THT}(\textsf {X},\textsf {R})$ and splittable $\textsf {THT}$ are more expressive than $\textsf {LTL}$. We conclude the section by providing a characterization of $\omega$-regular languages in terms of $\textsf {TEL}$ languages.

We first individuate minimal $\textsf {THT}$ fragments which under the $\textsf {TEL}$ semantics are not subsumed by $\textsf {LTL}$.

Proposition 4

Let $\mathcal {F}$ denote any of the following $\textsf {THT}$ fragments: $\textsf {THT}_2(\textsf {X},\textsf {U})$, $\textsf {THT}_3(\textsf {U})$, $\textsf {THT}_3(\textsf {R})$, and splittable $\textsf {THT}_2(\textsf {X},\textsf {G})$. Then $(\mathcal {F})_\textsf {TEL} \not \le \textsf {LTL}$.

Proof

Here, we focus on splittable $\textsf {THT}_2(\textsf {X},\textsf {G})$ (for the other fragments, see the authors’ full paper online). Let $\mathcal {L}_\textit{odd}$ be the $\omega$-regular language given by

$$ \mathcal {L}_\textit{odd}:= \{\textsf {T}\mid \textsf {T}=\{a,b,u\}^{2n+1}\,\emptyset ^{\omega }\text { for some } n>0\} $$

where a, b,  and u are distinct atomic propositions. One can easily show that $\mathcal {L}_\textit{odd}$ is not $\textsf {LTL}$ expressible (see e.g. [11]). We exhibit a splittable $\textsf {THT}_2(\textsf {X},\textsf {G})$ formula $\varphi _\textit{odd}$ over $P=\{a,b,u\}$ whose set of TEL models corresponds to $\mathcal {L}_\textit{odd}$.

Formula $\varphi _\textit{odd}$ is the conjunction of the following three splittable $\textsf {THT}_2(\textsf {X},\textsf {G})$ formulas, where $\psi _\emptyset := \lnot a \wedge \lnot b \wedge \lnot u$ characterizes the empty positions of the “there” interpretation.

$$\begin{aligned} \lnot \lnot u \,\,\wedge \,\, \lnot \lnot \textsf {G}(\psi _\emptyset \vee (a\wedge b \wedge u)) \,\,\wedge \,\, \lnot \lnot \textsf {G}(\psi _\emptyset \rightarrow \textsf {X}\psi _\emptyset ) \end{aligned}$$

(1)

$$\begin{aligned} \textsf {G}(u \rightarrow a\wedge b) \,\,\wedge \,\, \textsf {G}(\textsf {X}u \rightarrow u) \,\,\wedge \,\, \textsf {G}(u \rightarrow \textsf {X}u \vee \textsf {X}\lnot u) \end{aligned}$$

(2)

$$\begin{aligned} a \,\,\wedge \,\, \textsf {G}(a \wedge b \rightarrow u) \,\,\wedge \,\, \textsf {G}(a \rightarrow \textsf {X}b) \,\,\wedge \,\, \textsf {G}(b \rightarrow \textsf {X}a \vee \textsf {X}\lnot u) \end{aligned}$$

(3)

Formula (1), which is a conjunction of constraints in a splittable $\textsf {THT}$ formula, captures the interpretations $(\textsf {H}, \textsf {T})$ such that $\textsf {T}\in \{a,b,u\}^{+}\,\emptyset ^{\omega }$. Formula (2) additionally ensures that whenever $\textsf {H}\ne \textsf {T}$, then $u\notin \textsf {H}(i)$ for all positions i. Finally, formula (3) requires that whenever $\textsf {H}\ne \textsf {T}$, the prefix of $\textsf {H}$ corresponding to the slice of $\textsf {T}$ (i.e., the maximal prefix of $\textsf {T}$ which does not contain empty positions) is in $(\{a\}\{b\})^{+}$. This last condition can be satisfied iff the length of the slice of $\textsf {T}$ is even. Hence, it easily follows that the $\textsf {TEL}$ language of $\varphi _\textit{odd}$ is exactly $\mathcal {L}_\textit{odd}$, and we are done.$\square$

We now establish the main results of Sect. 5.

Theorem 6

The following holds, where $k\ge 2$ and $\mathcal {O}\in \{\textsf {U},\textsf {R}\}$:

• 1. $(\textsf {THT}(\textsf {X},\textsf {U}))_\textsf {TEL} \, \bot \,\textsf {LTL}$ and $(\textsf {THT}_k(\textsf {X},\textsf {U}))_\textsf {TEL} \, \bot \,\textsf {LTL}$;

• 2. $(\textsf {THT}(\textsf {X},\textsf {R}))_\textsf {TEL} \, > \,\textsf {LTL}$ and $(\textsf {THT}_k(\textsf {X},\textsf {R}))_\textsf {TEL} \, \bot \,\textsf {LTL}$;

• 3. $(\textsf {THT}(\mathcal {O}))_\textsf {TEL} \, \bot \, \textsf {LTL}$ and $(\textsf {THT}_{k+1}(\mathcal {O}))_\textsf {TEL} \, \bot \, \textsf {LTL}$;

• 4. $(\textsf {THT}_k(\textsf {X},\textsf {R}))_\textsf {TEL} > (\textsf {THT}_k(\textsf {X},\textsf {R}))_\textsf {LTL}$ and $(\textsf {THT}_{k-1})_\textsf {TEL} > (\textsf {THT}_{k-1})_\textsf {LTL}$;

• 5. $(\text {splittable } \textsf {THT})_\textsf {TEL} \, > \,\textsf {LTL}$.

Proof

In [2], it is shown that every $\textsf {TEL}$ model of a $\textsf {THT}(\textsf {X},\textsf {U})$ has a finite set of non-empty positions. Since there are $\textsf {THT}$ formulas whose $\textsf {LTL}$ models have infinitely many non-empty positions, by Proposition 4, Properties 1 and 3 with $\mathcal {O} = \textsf {U}$ follow. One can trivially check that the $\textsf {LTL}$-expressible $\omega$-language $\mathcal {L}= \emptyset \{a\}^{\omega }$ is not expressible in the fragment $\textsf {THT}(\textsf {R})$ under the $\textsf {TEL}$ semantics. Hence, by Proposition 4, Property 3 for the case $\mathcal {O} = \textsf {R}$ follows as well. For Properties 2 and 4, let $n\ge 1$ and $\mathcal {L}_n$ be the $\textsf {LTL}$-expressible $\omega$-language consisting of the $\textsf {LTL}$ interpretation $\emptyset ^{n}\cdot \{a\}\cdot \emptyset ^{\omega }$. One can easily check that no $\textsf {THT}_h$ formula with $h<n$ can capture $\mathcal {L}_n$ under the $\textsf {TEL}$ semantics. Since $\textsf {THT}$ is expressively equivalent to $\textsf {THT}(\textsf {X},\textsf {R})$ under the $\textsf {LTL}$ semantics and for all $h\ge 1$ and $\varphi \in \textsf {THT}_h(\textsf {X},\textsf {R})$, the set of $\textsf {LTL}$ models of $\varphi$ corresponds to the set of $\textsf {TEL}$ models of the $\textsf {THT}_h(\textsf {X},\textsf {R})$ formula $\varphi \wedge \psi _\textit{Tot}(P)$, by Theorem 5 and Proposition 4, Properties 2 and 4 follows. Finally, for Property 5, we exploit Proposition 4 and the fact that the set of $\textsf {LTL}$ models of a $\textsf {THT}$ formula $\varphi$ corresponds to the set of $\textsf {TEL}$ models of the splittable $\textsf {THT}$ formula $\lnot \lnot \varphi \wedge \psi _\textit{Tot}(P)$.$\square$

We conclude this section by showing that $\textsf {TEL}$ languages capture in a weak sense the full class of $\omega$-regular languages. In fact, this weak equivalence, as formalized by the following Theorem 7, is similar to the well-known equivalence between $\omega$-regular languages and $\omega$-languages defined by formulas of Quantified propositional $\textsf {LTL}$ ($\textsf {QLTL}$)[23], where for capturing a given $\omega$-regular language over $2^{P}$ by a $\textsf {QLTL}$-formula, one needs to use quantification over additional propositions not in P. Intuitively, flat propositions in $\textsf {TEL}$ play the role of bounded propositions in $\textsf {QLTL}$.

Theorem 7

Let $\mathcal {L}$ be an $\omega$-language over $2^{P}$. Then, $\mathcal {L}$ is $\omega$-regular iff there exists a finite set Q disjoint from P such that $\mathcal {L}\oplus Q$ is a TEL language.

6 Conclusion

We have provided a systematic study of the expressiveness comparison between the $\textsf {LTL}$ semantics and the $\textsf {TEL}$ semantics for various natural $\textsf {THT}$ syntactical fragments. Some interesting questions remain open: for example, we don’t know whether the TEL semantics of the fragment $\textsf {THT}(\textsf {F},\textsf {G},\textsf {X})$ is able to capture full $\textsf {LTL}$. Additionally, it is well-known that the class of $\textsf {LTL}$-definable languages is algebraically robust, being, in particular, closed under all boolean operations. It is an intriguing open question whether the same holds for the class of $\textsf {TEL}$-definable languages.