Computational Complexity of Standpoint LTL

The $\mathsf{SLTL}$ formulae are built over a countably infinite set $\mathcal{P}$ of propositional variables and a countably infinite set $\mathcal{S}=\{\mathtt{s},\mathtt{s}^{\prime},\ldots\}$ of standpoint symbols including the universal standpoint symbol $*$. The $\mathsf{SLTL}$ formulae $\varphi$ are defined according to the grammar:

$$\varphi::=p\mid\mathtt{s}\preceq\mathtt{s}^{\prime}\mid\neg\varphi\mid\varphi\wedge\varphi\mid\Diamond_{\mathtt{s}}\varphi\mid\Box_{\mathtt{s}}\varphi\mid\mathsf{X}\varphi\mid\varphi\mathsf{U}\varphi,$$

where $p\in\mathcal{P}$ and $\mathtt{s},\mathtt{s}^{\prime}\in\mathcal{S}$; other Boolean connectives and $\mathsf{LTL}$ temporal operators (e.g. $\to$, $\leftrightarrow$, $\vee$, $\mathsf{G}$ for “always in the future”, and $\mathsf{F}$ for “sometime in the future”) are treated as standard abbreviations. In terms of expressivity, one modality among $\Diamond_{\mathtt{s}},\Box_{\mathtt{s}}$ is sufficient. An $\mathsf{SLTL}$ model, $\mathcal{M}$, is a structure of the form $\mathcal{M}=(\Pi,\lambda)$ where,

• –

  $\Pi\neq\emptyset$ is a set of $\mathsf{LTL}$ models (traces) of the form $\sigma:\mathbb{N}\longrightarrow 2^{\mathcal{P}}$,

• –

  $\lambda$ is a map of the form $\lambda:\mathcal{S}\longrightarrow(2^{\Pi}\setminus\{\emptyset\})$ such that $\lambda(*)=\Pi$.

For example, Figure 1 presents an $\mathsf{SLTL}$ model with six traces. The satisfaction relation, $\mathcal{M},\sigma,i\models\varphi$, for an $\mathsf{SLTL}$ model $\mathcal{M}=(\Pi,\lambda)$, $\sigma\in\Pi$, $i\in\mathbb{N}$, and an $\mathsf{SLTL}$ formula $\varphi$ is defined inductively as follows (we omit the standard clauses for Boolean connectives):

	$\displaystyle\mathcal{M},\sigma,i\models p$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;\Leftrightarrow\;}}$	$\displaystyle p\in\sigma(i),$
	$\displaystyle\mathcal{M},\sigma,i\models\mathtt{s}\preceq\mathtt{s}^{\prime}$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;\Leftrightarrow\;}}$	$\displaystyle\lambda(\mathtt{s})\subseteq\lambda(\mathtt{s}^{\prime}),$
	$\displaystyle\mathcal{M},\sigma,i\models\Diamond_{\mathtt{s}}\varphi$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;\Leftrightarrow\;}}$	$\displaystyle\mathcal{M},\sigma^{\prime},i\models\varphi,\text{ for some }\sigma^{\prime}\in\lambda(\mathtt{s}),$
	$\displaystyle\mathcal{M},\sigma,i\models\Box_{\mathtt{s}}\varphi$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;\Leftrightarrow\;}}$	$\displaystyle\mathcal{M},\sigma^{\prime},i\models\varphi,\text{ for all }\sigma^{\prime}\in\lambda(\mathtt{s}),$
	$\displaystyle\mathcal{M},\sigma,i\models\mathsf{X}\varphi$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;\Leftrightarrow\;}}$	$\displaystyle\mathcal{M},\sigma,i+1\models\varphi,$
	$\displaystyle\mathcal{M},\sigma,i\models\varphi\mathsf{U}\psi$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;\Leftrightarrow\;}}$	$\displaystyle\text{there is }i^{\prime}\geq i\text{ such that }\mathcal{M},\sigma,i^{\prime}\models\psi$
	$\displaystyle\text{and }\mathcal{M},\sigma,i^{\prime\prime}\models\varphi\text{ for all }i\leq i^{\prime\prime}<i^{\prime}.$

The satisfiability problem for $\mathsf{SLTL}$ takes as input an $\mathsf{SLTL}$ formula $\varphi$ and asks whether there is a model $\mathcal{M}=(\Pi,\lambda)$ and $\sigma\in\Pi$ such that $\mathcal{M},\sigma,0\models\varphi$. By way of example, we provide an $\mathsf{SLTL}$ formula below taken from the medical devices example [20, Section 2.1] (more elaborated examples can be found in [21, 22, 20]):

$$\Box_{*}(\mathsf{G}\neg\mathit{Malf}\to\mathit{Test})\land\Box_{\mathsf{IT}}(\mathit{Comp}\vee\mathit{Test}\to\mathit{Safe}).$$

The first conjunct states that all countries agree in their standpoints that if a medical device never malfunctions, then it is safe according to testing. The second one states that Italy deems a device safe if it is safe according to testing or it has been found safe by comparison.

Regarding our definition of $\mathsf{SLTL}$, it is worth observing that, as far as we can judge, the satisfiability problem is not formally defined in [20, Section 2.2]. Only the validity problem is defined. In particular, non validity of the $\mathsf{SLTL}$ formula $\varphi$ is defined as the existence of an $\mathsf{SLTL}$ model $\mathcal{M}=(\Pi,\lambda)$ and $\sigma\in\Pi$ such that $\mathcal{M},\sigma,0\models\neg\varphi$. So, our definition of satisfiability is dual to the notion of validity used by Gigante et al. [20].

Besides, it is worth noting that the above presentation of $\mathsf{SLTL}$ differs slightly with the definition of Gigante et al. [20, Section 2.2], but it has no impact on our results, as described next. $\mathsf{SLTL}$ formulae, as defined in [20], are in negation normal form and allow for using the “release” $\mathsf{LTL}$ operator. In our definition negation is unrestricted and we do not use the “release” operator, which makes no substantial difference. Gigante et al. [20] assumes also that the formulae $\mathtt{s}\preceq\mathtt{s}^{\prime}$ cannot be combined with other formulae, so the way we define $\mathsf{SLTL}$ formulae is slightly more expressive. However, our ExpSpace-hardness proof (reduction in Lemma 1) does not use formulae of the form $\mathtt{s}\preceq\mathtt{s}^{\prime}$ (actually only the modalities $\Box_{*}$, $\mathsf{X}$, and $\mathsf{U}$ are needed). The ExpSpace-membership (Corollary 4) for our, slightly richer language, clearly implies the same upper bound for the weaker language of Gigante et al. [20].

The change of standpoint performed with the modalities $\Diamond_{\mathtt{s}}$ and $\Box_{\mathtt{s}}$ is reminiscent to the change of observational power studied in [8] with the modalities $\Delta^{o}$. In both cases, a modality explicitly performs a change in the way the forthcoming formulae are evaluated.

In the sequel, we also consider propositional standpoint logic [22] (herein, written $\mathsf{PSL}$) understood as the fragment of $\mathsf{SLTL}$ without temporal connectives. The grammar of formulae is restricted to

$$\varphi::=p\mid\mathtt{s}\preceq\mathtt{s}^{\prime}\mid\neg\varphi\mid\varphi\wedge\varphi\mid\Diamond_{\mathtt{s}}\varphi\mid\Box_{\mathtt{s}}\varphi,$$

and the models are of the form $\mathcal{M}=(\Pi,V)$ where $\Pi$ is a finite non-empty set of precisifications, $V:\mathcal{S}\cup\mathcal{P}\longrightarrow 2^{\Pi}$ is a valuation such that for all $\mathtt{s}\in\mathcal{S}$, we have $V(\mathtt{s})\neq\emptyset$ and $V(*)=\Pi$. The satisfaction relation is defined as follows (where $\pi\in\Pi$ and we omit the obvious clauses for Boolean connectives):

	$\displaystyle\mathcal{M},\pi\models p$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;\Leftrightarrow\;}}$	$\displaystyle\pi\in V(p),$
	$\displaystyle\mathcal{M},\pi\models\mathtt{s}\preceq\mathtt{s}^{\prime}$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;\Leftrightarrow\;}}$	$\displaystyle V(\mathtt{s})\subseteq V(\mathtt{s}^{\prime}),$
	$\displaystyle\mathcal{M},\pi\models\Diamond_{\mathtt{s}}\varphi$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;\Leftrightarrow\;}}$	$\displaystyle\mathcal{M},\pi^{\prime}\models\varphi,\text{ for some }\pi^{\prime}\in V(\mathtt{s}),$
	$\displaystyle\mathcal{M},\pi\models\Box_{\mathtt{s}}\varphi$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;\Leftrightarrow\;}}$	$\displaystyle\mathcal{M},\pi^{\prime}\models\varphi,\text{ for all }\pi^{\prime}\in V(\mathtt{s}).$

The satisfiability problem, for an input formula $\varphi$, consists in checking whether there is some pair $\mathcal{M},\pi$ such that $\mathcal{M},\pi\models\varphi$. This problem is NP-complete. To show NP-membership,  Gómez Álvarez [21, Section 4.4.2] proved that if a satisfiable formula $\varphi$ contains $N_{1}$ many standpoint symbols and $N_{2}$ many diamond modal operators, then $\varphi$ is satisfied in a model $\mathcal{M}=(\Pi,V)$ such that ${\mid\!{\Pi}\!\mid}\leq N_{1}+N_{2}+1$. An alternative way to get the NP-membership is to translate $\varphi$ into a formula $\bigwedge_{\mathtt{s}}\Diamond\mathtt{s}\wedge\mathfrak{t}(\varphi)$ of the modal logic $\mathsf{S5}$ [12], where $\mathfrak{t}$ turns standpoint operators into modal operators in the following manner: $\mathfrak{t}(\mathtt{s}\preceq\mathtt{s}^{\prime})=\Box(\mathtt{s}\to\mathtt{s}^{\prime})$, $\mathfrak{t}(\Diamond_{\mathtt{s}}\varphi)=\Diamond(\mathtt{s}\wedge\mathfrak{t}(\varphi))$, and $\mathfrak{t}(\Box_{\mathtt{s}}\varphi)=\Box(\mathtt{s}\to\mathfrak{t}(\varphi))$. The correctness of such a reduction relies naturally on the Kripke-style semantics for $\mathsf{PSL}$. We will refine complexity analysis of $\mathsf{PSL}$ in Section 4.2, which will be essential to establish complexity of $\mathsf{SLTL}$ fragments.

Another logic that is useful herein is the multi-dimensional modal logic $\mathsf{PTLxS5}$ [19, Chapter 5] defined as the product of $\mathsf{LTL}$ and $\mathsf{S5}$. $\mathsf{PTLxS5}$ formulae are generated from the grammar

$$\varphi::=p\mid\neg\varphi\mid\varphi\wedge\varphi\mid\Diamond\varphi\mid\Box\varphi\mid\mathsf{X}\varphi\mid\varphi\mathsf{U}\varphi,$$

where $p\in\mathcal{P}$ is a propositional variable. As in $\mathsf{SLTL}$, we use standard abbreviations for other Boolean connectives and $\mathsf{LTL}$ operators ($\to$, $\vee$, $\mathsf{G}$, $\mathsf{F}$, etc.). The models for $\mathsf{PTLxS5}$ are of the form $\mathcal{M}=(\mathbb{N}\times W,R,L)$ where $(W,R)$ is an $\mathsf{S5}$-frame (i.e. $R$ is an equivalence relation on $W$) and $L:\mathbb{N}\times W\longrightarrow 2^{\mathcal{P}}$. The satisfaction relation for $\mathsf{PTLxS5}$ is defined as follows (again, we omit the standard clauses for Boolean connectives):

	$\displaystyle\mathcal{M},(n,w)\models p$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;\Leftrightarrow\;}}$	$\displaystyle p\in L(n,w),$
	$\displaystyle\mathcal{M},(n,w)\models\Diamond\varphi$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;\Leftrightarrow\;}}$	$\displaystyle\mathcal{M},(n,w^{\prime})\models\varphi,\text{ for some }w^{\prime}\in R(w),$
	$\displaystyle\mathcal{M},(n,w)\models\Box\varphi$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;\Leftrightarrow\;}}$	$\displaystyle\mathcal{M},(n,w^{\prime})\models\varphi,\text{ for all }w^{\prime}\in R(w),$
	$\displaystyle\mathcal{M},(n,w)\models\mathsf{X}\varphi$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;\Leftrightarrow\;}}$	$\displaystyle\mathcal{M},(n+1,w)\models\mathsf{X}\varphi,$
	$\displaystyle\mathcal{M},(n,w)\models\varphi\mathsf{U}\psi$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;\Leftrightarrow\;}}$	$\displaystyle\text{there is }n^{\prime}\geq n\text{ such that }\mathcal{M},(n^{\prime},w)\models\psi$
	$\displaystyle\text{and }\mathcal{M},(n^{\prime\prime},w)\models\varphi\text{ for all }n\leq n^{\prime\prime}<n^{\prime}.$

Therefore, the modalities $\Diamond$ and $\Box$ allow us to move within the $(W,R)$ dimension whereas the temporal connectives $\mathsf{X}$ and $\mathsf{U}$ allow us to move along the $(\mathbb{N},\leq)$ dimension. The satisfiability problem for $\mathsf{PTLxS5}$ takes as input a $\mathsf{PTLxS5}$ formula $\varphi$ and asks whether there is a model $\mathcal{M}=(\mathbb{N}\times W,R,L)$ and $(n,w)\in\mathbb{N}\times W$ such that $\mathcal{M},(n,w)\models\varphi$. It is known, that satisfaction of a formula can be always witnessed by a model $\mathcal{M}=(\mathbb{N}\times W,R,L)$ with $R=W\times W$ and by a pair $(0,w)$ (i.e. its first component is the origin position $0$). In the sequel we will use this assumption; in particular, we will assume that $R=W\times W$, and for simplicity of presentation we will drop the component $R$ from $\mathsf{PTLxS5}$ models.

It is worth noting that the above presentation of $\mathsf{PTLxS5}$ differs slightly from the definitions by Gabbay et al. [19, Section 2.1], but it has no impact on our results. Indeed, Gabbay et al. [19] use only the strict “until” operator, which we denote by $\mathsf{U}_{<}$ (and no next-time operator $\mathsf{X}$) and whose semantics is as follows:

	$\displaystyle\mathcal{M},(n,w)\models\varphi\mathsf{U}_{<}\psi$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;\Leftrightarrow\;}}$	$\displaystyle\text{there is }n^{\prime}>n\text{ with }\mathcal{M},(n^{\prime},w)\models\psi$
	$\displaystyle\text{and }\mathcal{M},(n^{\prime\prime},w)\models\varphi\text{ for all }n<n^{\prime\prime}<n^{\prime}.$

It is easy to see that $\varphi\mathsf{U}_{<}\psi$ can be encoded by $\mathsf{X}(\varphi\mathsf{U}\psi)$ and therefore the ExpSpace-hardness for $\mathsf{PTLxS5}$ proved by Gabbay et al. [19, Theorem 5.43] applies also to our version of $\mathsf{PTLxS5}$. As far as the ExpSpace-membership is concerned, the satisfiability problem for our version of $\mathsf{PTLxS5}$ is in ExpSpace using the approach of Gabbay et al. [19, Theorem 6.65] dedicated to $\mathsf{PTLxS5}$ with strict “until” and using a standard renaming technique [19, Proposition 2.10]. Note that a naive translation $\mathfrak{t}$ from our language to a formula with strict “until” exploiting $\mathfrak{t}(\varphi\mathsf{U}\psi)=\mathfrak{t}(\psi)\vee(\mathfrak{t}(\varphi)\wedge\mathfrak{t}(\varphi)\mathsf{U}_{<}\mathfrak{t}(\psi))$, would cause an exponential blow-up. However, we can get a logarithmic-space reduction using the renaming technique, where any subformula $\chi$ is associated with a fresh propositional variable $p_{\chi}$. For instance, to capture the meaning of $\varphi\mathsf{U}\psi$ we introduce an additional formula $\Box\mathsf{G}\big{(}p_{\varphi\mathsf{U}\psi}\leftrightarrow p_{\psi}\vee(p_{\varphi}\wedge p_{\varphi}\mathsf{U}_{<}p_{\psi})\big{)}.$ This additional formula (propagating an equivalence all over the model), if asserted in any world of the form $(0,w)$, allows us to state that $p_{\varphi\mathsf{U}\psi}$ is equivalent with $\psi\vee(\varphi\wedge\varphi\mathsf{U}_{<}\psi)$, in all elements in $\mathbb{N}\times W$. The propagation is over the model because of the modality $\Box\mathsf{G}$ and we can always assume that a world satisfying our formula is of the form $(0,w)$. As a conclusion, the version of $\mathsf{PTLxS5}$ involved in this paper admits also an ExpSpace-complete satisfiability problem (ExpSpace-hardness follows from the fact that $\varphi\mathsf{U}_{<}\psi$ can be encoded by $\mathsf{X}(\varphi\mathsf{U}\psi)$).

Let us conclude this section by evoking the relationships between $\mathsf{SLTL}$ and the well-known modal logic $\mathsf{S5}$ [12]. The logic $\mathsf{SLTL}$ contains a modality $\Box_{*}$ where $*$ can be understood as the universal standpoint interpreted by the total set of traces and therefore $\Box_{*}$ behaves naturally as an $\mathsf{S5}$ modality, whence the component $\mathsf{S5}$ in $\mathsf{PTLxS5}$. The presence of $\mathsf{S5}$ is not our finding as it has been already observed that quantification over precisifications leads to $\mathsf{S5}$ modalities, see e.g., the works of Bennett [9, Section 2.1] and Bennett [10, page 43], as well as the presence of $\mathsf{S5}$ modalities for modelling standpoints in [21, Section 3.5] and in [21, Chapter 4]. Furthermore, the relationship with multi-dimensional modal logics is already briefly evoked in [21, Section 7.3.3]. More importantly, an early introduction of some multi-dimensional modal logic is performed by Bennett [9, Section 2.1] where first-order logic and propositional modal logic $\mathsf{S5}$ are mixed. Hence, the fact that we use $\mathsf{PTLxS5}$ is not a total surprise, and the need for multi-dimensional modal logics was in the air for some time. Our contribution consists in establishing a formal result involving multi-dimensional modal logics and in designing simple logarithmic-space reductions between $\mathsf{SLTL}$ and $\mathsf{PTLxS5}$, proving ExpSpace-hardness of $\mathsf{SLTL}$, despite the complexity result claimed in [20, Theorem 28]. The design of a PSpace fragment completes our analysis and provides us with a fragment of $\mathsf{SLTL}$ which is a strict extension of both $\mathsf{LTL}$ and standpoint logic, but its computational complexity is not higher than the complexity of pure $\mathsf{LTL}$.

Let $\varphi$ be a $\mathsf{PTLxS5}$ formula and $\mathfrak{t}_{1}(\varphi)$ be its translation obtained from $\varphi$ by replacing every occurrence of $\Diamond$ by $\Diamond_{*}$ and every occurrence $\Box$ by $\Box_{*}$ (an alternative translation consists in using $\Diamond_{\mathtt{s}}$ and and $\Box_{\mathtt{s}}$ for some fixed $\mathtt{s}\in\mathcal{S}$). We show that this simple translation preserves satisfiability.

Note that this result contradicts the PSpace upper bound shown by Gigante et al. [20, Theorem 28], as PSpace and ExpSpace are known to be distinct complexity classes.

The translation from $\mathsf{SLTL}$ to $\mathsf{PTLxS5}$ is (slightly) more complex since $\mathsf{SLTL}$ models interpret standpoint symbols, which have no natural counterpart in $\mathsf{PTLxS5}$ models. As we will show, however, standpoints can be simulated in $\mathsf{PTLxS5}$ with fresh propositional variables. This, in particular, requires an additional formula (called $\chi_{n}$ below) simulating the requirements that each standpoint in an $\mathsf{SLTL}$ model has at least one associated trace and that if a trace is assigned to a standpoint, it is so throughout the entire timeline. As we show, such requirements can be easily expressed in $\mathsf{PTLxS5}$.

Given an $\mathsf{SLTL}$ formula $\varphi$, we construct a $\mathsf{PTLxS5}$ formula $\mathfrak{t}_{2}(\varphi)$, by applying the translation map $\mathfrak{t}_{2}$ such that $\mathfrak{t}_{2}$ is the identity map for propositional variables, it is homomorphic for Boolean and temporal connectives, and the following hold for all $\mathtt{s},\mathtt{s}^{\prime}\in\mathcal{S}$:

	$\displaystyle\mathfrak{t}_{2}(\Diamond_{*}\psi)$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}\Diamond\mathfrak{t}_{2}(\psi),$	$\displaystyle\mathfrak{t}_{2}(\Diamond_{\mathtt{s}}\psi)$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}\Diamond(\mathtt{s}\wedge\mathfrak{t}_{2}(\psi)),$
	$\displaystyle\mathfrak{t}_{2}(\Box_{*}\psi)$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}\Box\mathfrak{t}_{2}(\psi),$	$\displaystyle\mathfrak{t}_{2}(\Box_{\mathtt{s}}\psi)$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}\Box(\mathtt{s}\to\mathfrak{t}_{2}(\psi)),$
	$\displaystyle\mathfrak{t}_{2}(\mathtt{s}\preceq\mathtt{s}^{\prime})$	$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}\Box(\mathtt{s}\to\mathtt{s}^{\prime}).$

Assuming that the standpoint symbols in $\varphi$ are $\mathtt{s}_{1},\ldots,\mathtt{s}_{n}$, we let

$$\chi_{n}\stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}\bigwedge_{1\leq i\leq n}(\Diamond\mathtt{s}_{i})\wedge\Box\bigwedge_{1\leq i\leq n}(\mathsf{G}\mathtt{s_{i}}\vee\mathsf{G}\neg\mathtt{s}_{i}).$$

As we show next, checking satisfiability of $\varphi$ in $\mathsf{SLTL}$ reduces to checking satisfiability of $\chi_{n}\wedge\mathfrak{t}_{2}(\varphi)$ in $\mathsf{PTLxS5}$.

Logarithmic-space reductions between $\mathsf{SLTL}$ and $\mathsf{PTLxS5}$ emphasize how close are these formalisms, a property that remained unnoticed so far. This allows us to establish the ExpSpace-completeness of $\mathsf{SLTL}$-satisfiability in a transparent way. Therefore, the analysis of the properties of the tableau-style calculus for $\mathsf{SLTL}$ designed by Gigante et al. [20] needs, in the best case, lead to the ExpSpace upper bound.

To obtain a better understanding of the ExpSpace-hardness of full $\mathsf{SLTL}$ and of the mismatch between our result in Section 3.1 and the PSpace bound stated by Gigante et al. [20, Theorem 28], we present a specific $\mathsf{SLTL}$ formula $\varphi_{C}$ whose satisfiability is particularly hard to decide. This will also prove useful for constructing PSpace fragments of $\mathsf{SLTL}$, as they should disallow features expressing the computationally challenging behaviour of $\varphi_{C}$.

Our construction of $\varphi_{C}$ exploits the following $\mathsf{LTL}$ formula $C_{n}$, encoding a binary counter from 0 to $2^{n}-1$, where the propositional variables $p_{1},\dots,p_{n}$ correspond to consecutive bits of the counter with $p_{1}$ being the most significant bit:

$$(\neg p_{1}\wedge\cdots\wedge\neg p_{n})\wedge\mathsf{G}(p_{1}\wedge\cdots\wedge p_{n}\to\mathsf{X}(\neg p_{1}\wedge\cdots\wedge\neg p_{n}))\\ \wedge\bigwedge_{1\leq i\leq n}\mathsf{G}\Big{(}(\neg p_{i}\wedge\bigwedge_{i<i^{\prime}\leq n}p_{i^{\prime}})\to\big{(}\bigwedge_{i<i^{\prime}\leq n}(\mathsf{X}\neg p_{i^{\prime}})\wedge\mathsf{X}p_{i}\\ \wedge\bigwedge_{1\leq i^{\prime}<i}(p_{i^{\prime}}\leftrightarrow\mathsf{X}p_{i^{\prime}})\big{)}\Big{)}.$$

In every position $i$ of an $\mathsf{LTL}$ trace $\sigma$, the propositional variables $p_{1},\dots,p_{n}$ encode the bits $b_{1},\dots,b_{n}$ (with $b_{1}$ being the most significant bit) such that $b_{j}=1$ iff $p_{j}\in\sigma(i)$. We write $\sigma,i\models\mathtt{C}=m$ if the counter has value $m$ in the position $i$, that is $b_{1}\dots b_{n}$ represents the number $m$. It is easy to see that if $\sigma,i\models C_{n}$, then the counter has value $0$ in the position $i$ and in every next position this value increases by 1 until the counter reaches the value $2^{n}-1$. If this is the case, in the next position the value is $0$ and the process of counting (modulo $2^{n}$) repeats. Hence, $\sigma,i\models\mathtt{C}=0$ and for any $j\geq i$, we have $\sigma,j\models\mathtt{C}=m^{\prime}$ where $m^{\prime}\equiv j-i\;(\mathsf{mod}\;{2^{n}})$.

We use $C_{n}$ to define $\varphi_{C}\stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}\mathsf{G}\big{(}\Diamond_{\mathtt{s}}(C_{n}\wedge p\wedge\mathsf{X}\mathsf{G}\neg p)\big{)}$ (of polynomial-size in $n$). As we show next, if $\mathcal{M},\sigma,0\models\varphi_{C}$ for some $\mathsf{SLTL}$ model $\mathcal{M}=(\Pi,\lambda)$, then $\Pi$ must contain infinitely many traces and for every position $i>2^{n}$ there are exponentially many (at least $2^{n}$) traces in $\Pi$ which are pairwise different with respect to the valuation of $p_{1},\dots,p_{n}$ at the position $i$. The latter, in particular, seems to contradict the first paragraph of the proof of [20, Lemma 27] used to argue for PSpace satisfiability of $\mathsf{SLTL}$.

In this section we show that a PSpace upper bound for the satisfiability problem in $\mathsf{SLTL}$ can be obtained by limiting the interplay between standpoint and temporal operators. To this end, we focus on $\mathsf{SLTL}$ formulae which do not allow for $\mathsf{LTL}$ connectives occurring in the scope of standpoint modal operators; in the sequel we call this fragment $\mathsf{LTL[PSL]}$. By way of example, the formula $\Box_{*}(\mathsf{G}\neg\mathit{Malf}\to\mathit{Test})$ from Section 2.1 does not belong to $\mathsf{LTL[PSL]}$. However the following is already an $\mathsf{LTL[PSL]}$ formula: $\mathsf{G}(\Box_{*}\neg\mathit{Malf})\to\Box_{*}\mathit{Test}$, which states that if always in future all countries agree that a medical device does not malfunction, then all these countries agree that this device is safe according to testing. It is worth observing that the formula $\varphi_{C}$ from Section 4.1, illustrating computationally challenging behaviour, does not belong to $\mathsf{LTL[PSL]}$ (because of $\mathsf{X}\mathsf{G}$ in the scope of $\Diamond_{\mathtt{s}}$). In contrast, any formula of the form $\mathsf{G}\Box_{*}\varphi_{1}\wedge\mathsf{G}(\varphi_{2}\rightarrow\mathsf{X}\varphi_{3})$ where $\varphi_{1},\varphi_{2},\varphi_{3}$ are $\mathsf{PSL}$ formulae (see Section 2.2) are in $\mathsf{LTL[PSL]}$.

As we show in the remaining part of this section, we can check satisfiability of $\mathsf{LTL[PSL]}$ formulae in PSpace by adapting the Büchi automaton construction developed for $\mathsf{LTL}$ [5, 15] and by performing model-theoretical constructions based on a refinement of the finite model property for $\mathsf{PSL}$ (see Theorem 9).

Let us fix an $\mathsf{LTL[PSL]}$ formula $\varphi$ and let $\mathcal{P}(\varphi)$ be the set of propositional variables occurring in it. Let $I$ (for ‘inequality’) be the set of subformulae of $\varphi$ of the form $\mathtt{s}\preceq\mathtt{s}^{\prime}$. To check satisfiability of $\varphi$, our procedure considers all possible partitions $D=(I^{+},I^{-})$ of $I$ into sets $I^{+}$ and $I^{-}$; intuitively such a partition states that formulae in $I^{+}$ are true and those in $I^{-}$ are false. Since $\mathtt{s}\preceq\mathtt{s}^{\prime}$ is a global statement (either it is satisfied in all traces and all positions of a model, or it is not satisfied in any of them), its truth value can be non-deterministically guessed from the very beginning. Moreover, such a guess is feasible in PSpace since NPSpace = PSpace [30]. Given $D=(I^{+},I^{-})$, we encode the above intuition with the formula

$$\chi_{D}\stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}\mathsf{G}\left(\bigwedge_{(\mathtt{s}\preceq\mathtt{s}^{\prime})\in I^{+}}(\mathtt{s}\preceq\mathtt{s}^{\prime})\land\bigwedge_{(\mathtt{s}\preceq\mathtt{s}^{\prime})\in I^{-}}(\Diamond_{\mathtt{s}}\ p_{\mathtt{s},\mathtt{s}^{\prime}}\wedge\neg\Diamond_{\mathtt{s}^{\prime}}\ p_{\mathtt{s},\mathtt{s}^{\prime}})\right)$$

where each $p_{\mathtt{s},\mathtt{s}^{\prime}}$ is a fresh propositional variable. This can be done as $\mathcal{P}$ is countably infinite. Note that $\chi_{D}$ encodes that each $\mathtt{s}\preceq\mathtt{s^{\prime}}$ in $I^{+}$ holds true always in future and that each $\mathtt{s}\preceq\mathtt{s^{\prime}}$ in $I^{-}$ is always false. We also define $\varphi_{D}\stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}\varphi[I^{+}\mapsto\top,I^{-}\mapsto\bot]\wedge\chi_{D}$, where $\varphi[I^{+}\mapsto\top,I^{-}\mapsto\bot]$ is the formula obtained from $\varphi$ by replacing each $(\mathtt{s}\preceq\mathtt{s}^{\prime})\in I^{+}$ with $\top$ and each $(\mathtt{s}\preceq\mathtt{s}^{\prime})\in I^{-}$ with $\bot$. Note that $\chi_{D}$ is an $\mathsf{LTL[PSL]}$ formula.

The purpose of the construction of $\varphi_{D}$, leading to Lemma 7, is to nondeterministically choose which inequalities $\mathtt{s}\preceq\mathtt{s}^{\prime}$ hold, and in particular to enforce the non-satisfaction of some $\mathtt{s}\preceq\mathtt{s}^{\prime}$ by the existence of two traces, see the formula $\chi_{D}$. Notice that $\mathtt{s}\preceq\mathtt{s}^{\prime}$ occurs only positively in $\chi_{D}$. In forthcoming Theorem 9, we show how to construct $\mathsf{PSL}$ models based on $\varphi_{1}$, defined as a conjunction of inequalities of the form $\mathtt{s}\preceq\mathtt{s}^{\prime}$. This step is therefore instrumental to handle the inequalities $\mathtt{s}\preceq\mathtt{s}^{\prime}$.

We write $\mathsf{cl}(\varphi_{D})$ to denote the closure set of $\varphi_{D}$ defined as the smallest set containing all the subformulae $\psi$ of $\varphi_{D}$ as well as $\perp$ and $\top$, which is closed under taking negations (as usually, we do not allow for double negations by identifying $\neg\neg\psi$ with $\psi$) and such that $\psi\mathsf{U}\psi^{\prime}\in\mathsf{cl}(\varphi_{D})$ implies $\mathsf{X}(\psi\mathsf{U}\psi^{\prime})\in\mathsf{cl}(\varphi_{D})$. We can observe that ${\mid\!{\mathsf{cl}(\varphi_{D})}\!\mid}\leq 4\cdot{\mid\!{\varphi_{D}}\!\mid}$ and the number of formulae in the set $\mathsf{cl}(\varphi_{D})$, whose outermost connective is a modality of the form $\Diamond_{\mathtt{s}}$ or $\Box_{\mathtt{s}}$, is bounded by ${\mid\!{\varphi_{D}}\!\mid}$.

As in the standard automaton construction for $\mathsf{LTL}$ [5, 15, 16], we call a set $B\subseteq\mathsf{cl}(\varphi)$ maximally consistent if it satisfies the properties:

• –

  $\top\in B$ and $\perp\not\in B$; $\psi\in B$ iff $\neg\psi\notin B$, for all $\neg\psi\in\mathsf{cl}(\varphi_{D})$,

• –

  $\psi_{1}\land\psi_{2}\in B$ iff $\psi_{1}\in B$ and $\psi_{2}\in B$, for all $\psi_{1}\land\psi_{2}\in\mathsf{cl}(\varphi_{D})$,

• –

  $\psi_{1}\mathsf{U}\psi_{2}\in B$ iff $\psi_{2}\in B$ or $\{\psi_{1},\mathsf{X}(\psi_{1}\mathsf{U}\psi_{2})\}\subseteq B$, for all $\psi_{1}\mathsf{U}\psi_{2}\in\mathsf{cl}(\varphi_{D})$.

Moreover, we introduce an additional property specific to $\mathsf{SLTL}$; we say that $B$ is standpoint-consistent if the $\mathsf{PSL}$ formula $\bigwedge_{\psi\in B\cap\mathsf{PSL}}\psi$ (we treat here $\mathsf{PSL}$ as the set of all well-formed $\mathsf{PSL}$ formulae) is satisfiable in standpoint logic $\mathsf{PSL}$. It is worth noting that checking standpoint-consistency is decidable and, in particular, NP-complete [22, Corollary 3] as we have discussed in Section 2.1 (see also the forthcoming Theorem 9).