EXPSPACE-Completeness of the Logics K4xS5 and S4xS5 and the Logic of Subset Spaces, Part 2: EXPSPACE-Hardness

TL;DR

This paper establishes that the satisfiability problems for the product logics K4xS5, S4xS5, and the logic of subset spaces are all EXPSPACE-complete, refining previous lower bounds to match known upper bounds.

Contribution

The paper proves that these three logic satisfiability problems are EXPSPACE-hard, completing their complexity classification as EXPSPACE-complete.

Findings

All three problems are EXPSPACE-hard under logspace reduction.

These problems are in EXPSPACE, thus are EXPSPACE-complete.

The results improve previous lower bounds from NEXPTIME and PSPACE.

Abstract

It is known that the satisfiability problems of the product logics K4xS5 and S4xS5 are NEXPTIME-hard and that the satisfiability problem of the logic SSL of subset spaces is PSPACE-hard. We improve these lower bounds for the complexity of these problems by showing that all three problems are EXPSPACE-hard under logspace reduction. In another paper we show that these problems are in ESPACE. This shows that all three problems are EXPSPACE-complete.

Tables

Table 1. Table 1: Some (partially numerical) abbreviations for logical formulas, where F ¯ = ( F l − 1 , … , F 0 ) ¯ 𝐹 subscript 𝐹 𝑙 1 … subscript 𝐹 0 \underline{F}=(F_{l-1},\ldots,F_{0}) and G ¯ = ( G l − 1 , … , G 0 ) ¯ 𝐺 subscript 𝐺 𝑙 1 … subscript 𝐺 0 \underline{G}=(G_{l-1},\ldots,G_{0}) are vectors of formulas. As usual, an empty conjunction like ⋀ h = 0 − 1 F h superscript subscript ℎ 0 1 subscript 𝐹 ℎ \bigwedge_{h=0}^{-1}F_{h} can be replaced by any propositional formula that is true always.

For	the following	is an abbreviation
	expression	of the following formula
$l\ge 1,k\ge -1$	$(\underset{¯}{F}=\underset{¯}{G},>k)$	${\bigwedge }_{h=k+1}^{l-1}(F_h\leftrightarrow G_h)$
$l\ge 1$	$\left(\underset{¯}{F}=\underset{¯}{G}\right)$	$(\underset{¯}{F}=\underset{¯}{G},>-1)$
$l\ge 1$,	$\left(\underset{¯}{F}={\mathrm{bin}}_l\left(i\right)\right)$	${\bigwedge }_{k\in \mathrm{Ones}\left(i\right)}{F}_k\wedge$
		${\bigwedge }_{k\in \{0,\dots ,l-1\}\setminus \mathrm{Ones}\left(i\right)}\neg F_k$
$l\ge 1$,	$\mathrm{rightmost}\_\mathrm{zero}(\underset{¯}{F},k)$	$\neg F_k\wedge {\bigwedge }_{h=0}^{k-1}{F}_h$
$l\ge 1$,	$\mathrm{rightmost}\_\mathrm{one}(\underset{¯}{F},k)$	$F_k\wedge {\bigwedge }_{h=0}^{k-1}\neg F_h$

Table 2. Table 2: Some (partially numerical) abbreviations for logical formulas, where F ¯ = ( F l − 1 , … , F 0 ) ¯ 𝐹 subscript 𝐹 𝑙 1 … subscript 𝐹 0 \underline{F}=(F_{l-1},\ldots,F_{0}) and G ¯ = ( G l − 1 , … , G 0 ) ¯ 𝐺 subscript 𝐺 𝑙 1 … subscript 𝐺 0 \underline{G}=(G_{l-1},\ldots,G_{0}) are vectors of formulas. An empty conjunction like ⋀ h = 0 − 1 F h superscript subscript ℎ 0 1 subscript 𝐹 ℎ \bigwedge_{h=0}^{-1}F_{h} can be replaced by any propositional formula that is true always. An empty disjunction like ⋁ h = 0 − 1 F h superscript subscript ℎ 0 1 subscript 𝐹 ℎ \bigvee_{h=0}^{-1}F_{h} can be replaced by any propositional formula that is false always.

For	the following	is an abbreviation
	expression	of the following formula
$l\ge 1$	$\mathrm{unique}\left(\underset{¯}{F}\right)$	${\bigvee }_{k=0}^{l-1}{F}_k\wedge {\bigwedge }_{k=0}^{l-1}{\bigwedge }_{m=k+1}^{l-1}\neg \left(F_k\wedge F_m\right)$
$l\ge 1$	$\left(\underset{¯}{F}\ne \underset{¯}{G}\right)$	$\neg \left(\underset{¯}{F}=\underset{¯}{G}\right)$
$l\ge 1$		${\bigvee }_{k=0}^{l-1}((\underset{¯}{F}=\underset{¯}{G},>k)\wedge \neg F_k\wedge G_k)$
$l\ge 1$	$\left(\underset{¯}{F}\le \underset{¯}{G}\right)$
$l\ge 1$	$\left(\underset{¯}{F}=\underset{¯}{G}+1\right)$	${\bigvee }_{k=0}^{l-1}((\underset{¯}{F}=\underset{¯}{G},>k)$
		$\wedge \mathrm{rightmost}\_\mathrm{one}(\underset{¯}{F},k)$
		$\wedge \mathrm{rightmost}\_\mathrm{zero}(\underset{¯}{G},k))$
$l\ge 1$	$\left(\underset{¯}{F}\ne \underset{¯}{G}+1\right)$	$\neg \left(\underset{¯}{F}=\underset{¯}{G}+1\right)$
$l\ge 1$,		${\bigvee }_{k\in \mathrm{Ones}\left(i\right)}\left(\neg F_k\wedge {\bigwedge }_{h\in \{k+1,\dots ,l-1\}\setminus \mathrm{Ones}\left(i\right)}\neg F_h\right)$
$l\ge 1$,	$\left(\underset{¯}{F}\le {\mathrm{bin}}_l\left(i\right)\right)$
$l\ge 1$,	$\left(\underset{¯}{F}>{\mathrm{bin}}_l\left(i\right)\right)$	$\neg \left(\underset{¯}{F}\le {\mathrm{bin}}_l\left(i\right)\right)$

Table 3. Table 3: Some abbreviations for logical formulas, where F ¯ = ( F l − 1 , … , F 0 ) ¯ 𝐹 subscript 𝐹 𝑙 1 … subscript 𝐹 0 \underline{F}=(F_{l-1},\ldots,F_{0}) and G ¯ = ( G l − 1 , … , G 0 ) ¯ 𝐺 subscript 𝐺 𝑙 1 … subscript 𝐺 0 \underline{G}=(G_{l-1},\ldots,G_{0}) are vectors of formulas. As usual, an empty conjunction like ⋀ h = 0 − 1 F h superscript subscript ℎ 0 1 subscript 𝐹 ℎ \bigwedge_{h=0}^{-1}F_{h} can be replaced by any propositional formula that is true always.

For	the following	is an abbreviation
	expression	of the following formula
$l\ge 1,k\ge -1$	$\mathrm{persistent}(\underset{¯}{F},>k)$	${\bigwedge }_{h=k+1}^{l-1}K\left(\square F_h\vee \square \neg F_h\right)$
$l\ge 1$	$\mathrm{persistent}\left(\underset{¯}{F}\right)$	$\mathrm{persistent}(\underset{¯}{F},>-1)$

Equations

$${\alpha }_i:=L(A_i\wedge \square LB).$$

$$\neg {\alpha }_i\equiv K(\neg A_i\vee ◊K\neg B).$$

$$\sum _{k\in \mathrm{Ones}(i)}{2}^k=i,$$

$$b_k(i):=\{\begin{array}{ll}1& \text{ if }k\in \mathrm{Ones}(i),\\ 0& \text{ if }k\notin \mathrm{Ones}(i).\end{array}$$

$${\mathrm{bin}}_n(i):=b_{n-1}(i),\dots ,b_0(i).$$

$$p_i^{\prime }\models (\underline{X}=\underline{\alpha },>k)\wedge rightmost\_one(\underline{X},k).$$

$$p_{i+1}\models (\underline{X}=\underline{\alpha }).$$

$$p_{i}\models L\bigl{(}(\underline{X}=\underline{\alpha},>k)\wedge\mathrm{rightmost\_one}(\underline{X},k)\wedge\Diamond(\underline{X}=\underline{\alpha})\bigr{)}.$$

$$p_0\models (\underline{\alpha }={\mathrm{bin}}_n(0)).$$

$${\mathrm{counter}}_{\mathrm{SSL},n}$$

$$W:=P\cup U\cup S$$

$$P$$

$$U$$

$$S$$

$$C_i:=\{p_{i,j}:i\le j<2^n\}\cup \{u_{i,k}:k\in \{0,\dots ,n-1\}\}\cup \{s_{i,k}:k\in \mathrm{Ones}(i)\},$$

$$C_{2^n}:=\{u_{2^n,k}:k\in \{0,\dots ,n-1\}\}.$$

$$\stackrel{◊}{\to }$$

$$\sigma (A_k)$$

$$\sigma (B)$$

$$\sigma (X_k)$$

$$p\models (\underline{\alpha }={\mathrm{bin}}_n(i)).$$

$$p\models {\alpha }_k⟺k\in \mathrm{Ones}(i).$$

$$(\forall p^{\prime }\in P)p^{\prime }\models (\neg A_k\vee ◊K\neg B).$$

$$(\forall u^{\prime }\in U)u^{\prime }\models (\neg A_k\vee ◊K\neg B).$$

$$p\models {\alpha }_k⟺k\in \mathrm{Ones}(i).$$

$$p_{0,0}\models B.$$

$$p_{0,0}\models (\underline{\alpha }={\mathrm{bin}}_n(0)).$$

$$p\models L\bigl{(}B\wedge(\underline{X}=\underline{\alpha},>k)\wedge\mathrm{rightmost\_one}(\underline{X},k)\wedge\Diamond(\underline{X}=\underline{\alpha})\bigr{)}.$$

$$p_{i,i+1}\models B.$$

$$p_{i,i+1}\models (\underline{X}=\underline{\alpha },>k)\wedge rightmost\_one(\underline{X},k)$$

$$p_{i+1,i+1}\models (\underline{X}=\underline{\alpha }).$$

$$p_{i,i+1}\models X_j\iff j\in \mathrm{Ones}(i+1)$$

Full text

Keywords: bimodal product logics, subset space logic, satisfiability problem, complexity theory, $\mathrm{EXPSPACE}$-completeness

1 Introduction

In this article we are concerned with the complexity of the bimodal product logics $\mathrm{K4\times S5}$ and $\mathrm{S4\times S5}$ and with the subset space logic $\mathrm{SSL}$, a bimodal logic as well. To the best of our knowledge, the complexity of $\mathrm{K4\times S5}$, of $\mathrm{S4\times S5}$, and of $\mathrm{SSL}$ were open problems. The main results of this article can be summarized in the following theorem.

Theorem 1.1**.**

The logics $\mathrm{K4\times S5}$, $\mathrm{S4\times S5}$, and $\mathrm{SSL}$ are $\mathrm{EXPSPACE}$-hard under logspace reduction.

Actually, we are considering the satisfiability problems of these three logics, and we are going to show that the satisfiability problems of these logics are $\mathrm{EXPSPACE}$-hard. Of course, this assertion is equivalent to the theorem above because $\mathrm{EXPSPACE}$ is closed under complements. This paper is a continuation of the paper [8], in which we show that these problems are in $\mathrm{ESPACE}$. Both results together imply the following theorem.

Theorem 1.2**.**

The logics $\mathrm{K4\times S5}$, $\mathrm{S4\times S5}$, and $\mathrm{SSL}$ are $\mathrm{EXPSPACE}$-complete under logspace reduction.

Let us recap the history of the questions and results concerning the complexity of these problems. The following text is almost identical with a corresponding text in  [8]. In [15, Question 5.3(i)] Marx posed the question what the complexity of the bimodal logic $\mathrm{S4\times S5}$ is. This question is restated and extended to the logic $\mathrm{K4\times S5}$ in [13, Problem 6.67, Page 334]. There it is also stated that “M. Marx conjectures that these logics are also EXPSPACE-complete”. That it is desirable to know the complexity of $\mathrm{SSL}$ and similar logics is mentioned by Parikh, Moss, and Steinsvold in [17, Page 30] and by Heinemann in [6, Page 153] and in [7, Page 513].

For the complexity of the satisfiability problems of the logics $\mathrm{K4\times S5}$ and $\mathrm{S4\times S5}$ the best upper bound known is $\mathrm{N2EXPTIME}$ [13, Theorem 5.28], that is, they can be solved by a nondeterministic Turing machine working in doubly exponential time. The best lower bound known for the satisfiability problems of these two logics is $\mathrm{NEXPTIME}$-hardness [13, Theorem 5.42]; compare also [13, Table 6.3, Page 340]. It is known as well that for any $\mathrm{SSL}$-satisfiable formula there exists a cross axiom model of at most doubly exponential size [5, Section 2.3]. This shows that the complexity of the satisfiability problem of $\mathrm{SSL}$ is in $\mathrm{N2EXPTIME}$ as well. The best lower bound known for $\mathrm{SSL}$ is $\mathrm{PSPACE}$-hardness  [12, 11].

In this paper we improve the lower bounds $\mathrm{NEXPTIME}$-hardness resp. $\mathrm{PSPACE}$-hardness for the satisfiability problems of these three logics to $\mathrm{EXPSPACE}$-hardness. In [8] we show a matching upper bound by showing that these problems are in $\mathrm{ESPACE}$. This shows that they are $\mathrm{EXPSPACE}$-complete. Thus, Marx’s conjecture for $\mathrm{K4\times S5}$ and $\mathrm{S4\times S5}$ stated above is true.

The main part of the paper is the $\mathrm{EXPSPACE}$-hardness proof of the satisfiability problem of the logic $\mathrm{SSL}$ in Section 4. In order to show this, we shall use Alternating Turing Machines [2]. In this respect, we follow the example of Lange and Lutz [14] who used Alternating Turing Machines in order to establish a sharp lower bound for the complexity of a certain dynamic logic. As any language in $\mathrm{EXPSPACE}$ is recognized by an Alternating Turing Machine (ATM) working in exponential time, it is sufficient to show that any language recognized by an Alternating Turing Machine working in exponential time can be reduced in logarithmic space to the satisfiability problem of $\mathrm{SSL}$. We will present such a reduction in Section 4. For this purpose we will construct an $\mathrm{SSL}$ formula that describes the computation of an exponential time bounded Alternating Turing Machine. In Section 3 we shall introduce Alternating Turing Machines. In that section we will also introduce certain formulas that we shall call ‘shared variables’ that we use in order to overcome the problem that ordinary propositional variables are persistent (see Subsection 3.1) in $\mathrm{SSL}$. Their usage is illustrated by an implementation of a binary counter in $\mathrm{SSL}$. The $\mathrm{EXPSPACE}$-hardness of the satisfiability problems of $\mathrm{K4\times S5}$ and of $\mathrm{S4\times S5}$ is then shown by reductions. In Section 5 we show that the satisfiability problem of $\mathrm{SSL}$ can be reduced in logarithmic space to the satisfiability problem of $\mathrm{S4\times S5}$. And in Section 6 we show that the satisfiability problem of $\mathrm{S4\times S5}$ can be reduced in logarithmic space to the satisfiability problem of $\mathrm{K4\times S5}$. These reductions are much easier than the reduction of a language recognized by an Alternating Turing Machine working in exponential time to the satisfiability problem of $\mathrm{SSL}$ presented in Section 4.

As there may be some interest in a direct proof of the $\mathrm{EXPSPACE}$-hardness of the satisfiability problem of the logic $\mathrm{S4\times S5}$, in an appendix we present such a proof by presenting a direct logspace reduction of any language recognized by an Alternating Turing Machine working in exponential time to the satisfiability problem of $\mathrm{S4\times S5}$. Although the overall structure of this proof is rather similar to the structure of the reduction of ATMs to the satisfiability problem of $\mathrm{SSL}$, there are some important differences. For illustration purposes, we also present an implementation of a binary counter in $\mathrm{S4\times S5}$ in the appendix.

2 Notations and Preliminaries

This paper is a continuation of [8]. We are going to use the same terminology as in that paper. In order not to repeat the definition of a lot of basic notions we would like to ask the reader to consult the first sections of [8] for the needed basic notions from complexity (see the end of the introduction of [8]), for the syntax of bimodal formulas (Subsection 2.1 in [8]), for $\mathrm{K4\times S5}$- and $\mathrm{S4\times S5}$-product models and -commutator models as well as for cross axiom models (Subsection 2.2 in [8]), for the notions of $X$-satisfiability of bimodal formulas, for $X\in\{\mathrm{K4\times S5},\mathrm{S4\times S5},\mathrm{SSL}\}$ (Subsection 2.3 in [8]), and for some basic notions and observations concerning transitive relations and equivalence relations, in particular for the definition of the relation $\stackrel{{\scriptstyle\Diamond}}{{\to}}^{\stackrel{{\scriptstyle L}}{{\to}}}$ induced by a relation $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ on the equivalence classes with respect to an equivalence relation $\stackrel{{\scriptstyle L}}{{\to}}$ (Subsection 3.1 in [8]).

As in [8] the $\stackrel{{\scriptstyle L}}{{\to}}$-equivalence class of a point in an $X\times\mathrm{S5}$-commutator model, for $X\in\{\mathrm{K4},\mathrm{S4}\}$, or a cross axiom model will be called the cloud of that point. Finally, for reducing one language to another one we use the logarithmic space bounded reduction as in [16].

3 Preparations for the Reduction of Alternating Turing Machines to $\mathrm{SSL}$

A string $w$ is an element of the language $L(M)$ recognized by an Alternating Turing Machine $M$ iff there exists a so-called accepting tree of $M$ on input $w$. In such a tree each node represents a configuration of $M$. Our idea is to construct a formula depending on $w$ such that the models of this formula have the tree structure of an accepting tree of $M$ on input $w$, where now the nodes of the tree are clouds such that the formulas satisfied in some cloud describe a configuration of $M$. In this way the induced relation $\stackrel{{\scriptstyle\Diamond}}{{\to}}^{\stackrel{{\scriptstyle L}}{{\to}}}$ between the clouds serves as a simple temporal operator.

In the following subsection we describe how information is stored and transmitted in a model of such a formula. In particular we introduce certain formulas that we call shared variables that can transmit information in the $\stackrel{{\scriptstyle L}}{{\to}}$-direction and by which we can overcome the problem in the logic $\mathrm{SSL}$ that all propositional variables are persistent. As a first application of this, in Subsection 3.2 we demonstrate how one can implement a binary counter in the logic $\mathrm{SSL}$. In Subsection 3.3 we recall the definition of Alternating Turing Machines.

3.1 Shared Variables

We have to make sure that various kinds of information are stored in a suitable way in any model of the fomula. We also need to copy and transmit various bits of information, both in the $\stackrel{{\scriptstyle\Diamond}}{{\to}}$-direction (we always depict this as the vertical direction) as well as in the $\stackrel{{\scriptstyle L}}{{\to}}$-direction (we always depict this as the horizontal direction). This will be done by two kinds of formulas.

• •

On the one hand, we need formulas that have the same truth value in the vertical ($\stackrel{{\scriptstyle\Diamond}}{{\to}}$) direction but can change their truth values in the horizontal ($\stackrel{{\scriptstyle L}}{{\to}}$) direction. In the case of the logic $\mathrm{SSL}$, for this purpose we can simply use propositional variables as they are persistent anyway.

• •

On the other hand, we need formulas that have the same truth value in the horizontal ($\stackrel{{\scriptstyle L}}{{\to}}$) direction but can change their truth values in the vertical ($\stackrel{{\scriptstyle\Diamond}}{{\to}}$) direction. Such formulas will be called shared variables and will be defined now.

Definition 3.1** (Shared Variables).**

For $i\in\mathbb{N}$ let $A_{i}$ be special propositional variables, and let $B$ be another special propositional variable $B$, different from all $A_{i}$. The shared variables $\alpha_{i}$ are defined as follows:

[TABLE]

Note that

[TABLE]

See Figure 1 for a model of a single shared variable $\alpha_{i}$ (in the figure we have omitted the index $i$) in $\mathrm{SSL}$ changing its value from $1$ to [math] and back from [math] to $1$. In this model the information is stored at the white points which we call information points. The gray points are auxiliary points that ensure that we obtain a model for the shared variables. Note that the information points differ from the auxiliary points in the value of the propositional variable $B$, which is true at all information points, independent of the value of $\alpha$ stored there, and false at all auxiliary points. Thus, the value of the propositional variable $B$ allows us to distinguish between the information points and the auxiliary points.

Although the shared variables $\alpha_{i}$ are formulas we are going to use them as if they were variables. The propositional variables $A_{i}$ and the propositional variable $B$ that are used in their definition will not be used in any other way. As a first example of the application of shared variables, in the following section we demonstrate how, using shared variables, one can implement $n$-bit binary counters in $\mathrm{SSL}$. Binary counters are going to play a key role in the simulation of Alternating Turing Machines in $\mathrm{SSL}$.

3.2 Binary Counters in $\mathrm{SSL}$

Fix some natural number $n\geq 1$. We wish to implement in $\mathrm{SSL}$ a binary $n$-bit counter that counts from [math] to $2^{n}-1$. That means, we wish to construct an $\mathrm{SSL}$-satisfiable formula with the property that any model of it contains a sequence of pairwise distinct points $p_{0},\ldots,p_{2^{n}-1}$ such that, for each $i\in\{0,\ldots,2^{n}-1\}$, at the point $p_{i}$ the number $i$ is stored in binary form in a certain way. To describe the implementation of the counter we first introduce some notation.

• •

For a natural number $i$, we define the finite set $\mathrm{Ones}(i)\subseteq\mathbb{N}$ by

[TABLE]

that is, $\mathrm{Ones}(i)$ is the set of the positions of ones in the binary representation of $i$ (where the positions are counted from the right starting with [math]).

• •

We will also need the bits $b_{k}(i)\in\{0,1\}$ of the binary representation of $i$, for $i,k\in\mathbb{N}$. They are defined by

[TABLE]

• •

For natural numbers $i,n$ with $n>0$ and $i\leq 2^{n}-1$ the binary representation of length $n$ of $i$ is the string

[TABLE]

Table 1 lists expressions that we use as abbreviations of formulas.

The idea of the construction is as follows.

• •

We store the counter values in a vector $\underline{\alpha}:=\alpha_{n-1},\ldots,\alpha_{0}$ of shared variables. To this end we embed the sequence $p_{0},\ldots,p_{2^{n}-1}$ of points in a sequence of clouds $\mathit{C}_{0},\ldots,\mathit{C}_{2^{n-1}}$ such that the cloud $\mathit{C}_{i}$ contains the point $p_{i}$ and such that the vector $\underline{\alpha}$ of shared variables satisfied at $p_{i}$ (and hence at all points in $\mathit{C}_{i}$) encodes the number $i$.

• •

Let $i\leq 2^{n}-1$ be the number encoded by $\underline{\alpha}$. If $\underline{\alpha}$ contains no [math] then $i$ has reached its highest posible value, the number $2^{n}-1$. Otherwise let $k$ be the position of the rightmost [math]. We determine the position $k$ with the aid of the formula $\mathrm{rightmost\_zero}(\alpha,k)$. In order to increment the counter we have to keep all $\alpha_{j}$ at positions $j>k$ unchanged and to switch all $\alpha_{j}$ at positions $j\leq k$. We do this in two steps:

First me make an $\stackrel{{\scriptstyle L}}{{\to}}$-step from the point $p_{i}$ to a point $p^{\prime}_{i}$ where we store the number $i+1$ in a vector $\underline{X}:=X_{n-1},\ldots,X_{0}$ of usual propositional variables by demanding that

[TABLE] 2. 2.

Then we make a $\stackrel{{\scriptstyle\Diamond}}{{\to}}$-step from the point $p^{\prime}_{i}$ to a point $p_{i+1}$ in the cloud $\mathit{C}_{i+1}$ and demand that

[TABLE]

Note that in $\mathrm{SSL}$ the value of $\underline{X}$ is copied from $p^{\prime}_{i}$ to its $\stackrel{{\scriptstyle\Diamond}}{{\to}}$-successor $p_{i+1}$ since in $\mathrm{SSL}$ propositional variables are persistent.

Altogether we demand that for the number $k$

[TABLE]

• •

Additionally we need a formula to ensure that the starting value is [math], that is we demand

[TABLE]

We now define the counter formula, for $n>0$. Remember that $\underline{\alpha}$ is a vector $(\alpha_{n-1},\ldots,\alpha_{0})$ of formulas $\alpha_{i}$ where $\alpha_{i}$ is defined by $\alpha_{i}:=L(A_{i}\wedge\Box LB)$; compare Definition 3.1.

[TABLE]

Proposition 3.2**.**

For all $n\in\mathbb{N}\setminus\{0\}$, the formula $\mathrm{counter}_{\mathrm{SSL},n}$ is $\mathrm{SSL}$-satisfiable. 2. 2.

For all $n\in\mathbb{N}\setminus\{0\}$, for every cross axiom model of $\mathrm{counter}_{\mathrm{SSL},n}$ and for every point $p_{0}$ in this model with $p_{0}\models\mathrm{counter}_{\mathrm{SSL},n}$ there exist a sequence of $2^{n}-1$ points $p_{1},p_{2},\ldots,p_{2^{n}-1}$ and a sequence of $2^{n}-1$ points $p_{0}^{\prime},p_{1}^{\prime},\ldots,p^{\prime}_{2^{n}-2}$ such that

• •

for $0\leq i\leq 2^{n}-1$,  $p_{i}\models(\underline{\alpha}=\mathrm{bin}_{n}(i))$,

• •

for $0\leq i\leq 2^{n}-2$,  $p_{i}\stackrel{{\scriptstyle L}}{{\to}}p^{\prime}_{i}$ and $p^{\prime}_{i}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{i+1}$ and $p^{\prime}_{i}\models(\underline{X}=\mathrm{bin}_{n}(i+1))$.

Proof.

For the following let us fix some $n>0$.

We construct a cross axiom model $M=(W,\stackrel{{\scriptstyle L}}{{\to}},\stackrel{{\scriptstyle\Diamond}}{{\to}},\sigma)$ with a point $p_{0,0}$ satisfying $M,p_{0,0}\models\mathrm{counter}_{\mathrm{SSL},n}$ as follows; see Figure 2.

We define

[TABLE]

where

[TABLE]

As the relation $\stackrel{{\scriptstyle L}}{{\to}}$ is supposed to be an equivalence relation we can define it by defining the $\stackrel{{\scriptstyle L}}{{\to}}$-equivalence classes. These are the sets

[TABLE]

for all $i\in\{0,\ldots,2^{n}-1\}$, and

[TABLE]

We define the relation $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ by:

[TABLE]

It is straightforward to check that $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ is reflexive and transitive. The cross property is satisfied as well. Thus, $(W,\stackrel{{\scriptstyle L}}{{\to}},\stackrel{{\scriptstyle\Diamond}}{{\to}})$ is a cross axiom frame. We define the valuation $\sigma$ by

[TABLE]

for $k\in\{0,\ldots,n-1\}$.

It is obvious that all of the propositional variables $A_{0},\ldots,A_{n-1},B$ and $X_{0},\ldots,X_{n-1}$ are persistent. Thus, $(W,\stackrel{{\scriptstyle L}}{{\to}},\stackrel{{\scriptstyle\Diamond}}{{\to}},\sigma)$ is a cross axiom model. We claim $p_{0,0}\models\mathrm{counter}_{\mathrm{SSL},n}$. Before we show this we show the following claim, for all $i\in\{0,\ldots,2^{n}-1\}$ and for all $p\in\mathit{C}_{i}$,

[TABLE]

In order to show this it is sufficient to show for all $i\in\{0,\ldots,2^{n}-1\}$, for all $p\in\mathit{C}_{i}$, and for all $k\in\{0,\ldots,n-1\}$

[TABLE]

Let us fix some $k\in\{0,\ldots,n-1\}$. Note that, for all $p^{\prime}\in P$, we have $p^{\prime}\models\neg A_{k}$, hence

[TABLE]

Furthermore, $u_{2^{n},h}\models K\neg B$ for all $h\in\{0,\ldots,n-1\}$. Since for all $i\in\{0,\ldots,2^{n}\}$ and $h\in\{0,\ldots,n-1\}$ we have $u_{i,h}\stackrel{{\scriptstyle\Diamond}}{{\to}}u_{2^{n},h}$ we obtain $u_{i,h}\models\Diamond K\neg B$ for all $i\in\{0,\ldots,2^{n}\}$ and $h\in\{0,\ldots,n-1\}$. Hence,

[TABLE]

This shows that, for any $i\in\{0,\ldots,2^{n}-1\}$, the shared variable $\alpha_{k}=L(A_{k}\wedge\Box LB)$ is true in the cloud $\mathit{C}_{i}$ if, and only if, there exists some $s^{\prime}\in\mathit{C}_{i}\cap V$ with $s^{\prime}\models(A_{k}\wedge\Box LB)$. As $p^{\prime}\models B$ for all $p^{\prime}\in P$ and any $s^{\prime}\in S$ is $\stackrel{{\scriptstyle L}}{{\to}}$-equivalent to some $p^{\prime}\in P$, we have $s^{\prime}\models LB$, for all $s^{\prime}\in S$. Actually, for $s^{\prime}\in S$ we even have $s^{\prime}\models\Box LB$ as $s^{\prime}$ does not have any $\stackrel{{\scriptstyle\Diamond}}{{\to}}$-successors besides itself. Thus, the shared variable $\alpha_{k}$ is true in the cloud $\mathit{C}_{i}$ if, and only if, there exists some $s^{\prime}\in\mathit{C}_{i}\cap S$ with $s^{\prime}\models A_{k}$. As the only elements $s^{\prime}\in\mathit{C}_{i}\cap S$ are the elements $s_{i,h}$ with $h\in\mathrm{Ones}(i)$ and as $s_{i,h}\models A_{k}\iff h=k$, we obtain for $i\in\{0,\ldots,2^{n}-1\}$ and for $p\in\mathit{C}_{i}$,

[TABLE]

We have shown the claim (3.1).

We claim that $p_{0,0}\models\mathrm{counter}_{\mathrm{SSL},n}$. Indeed, it is obvious that

[TABLE]

Due to $p_{0,0}\in\mathit{C}_{0}$ and (3.1) we obtain

[TABLE]

Let us assume that for some $p\in W$ and some $k\in\{0,\ldots,n-1\}$ we have $p\models(B\wedge\mathrm{rightmost\_zero}(\underline{\alpha},k))$. It is sufficient to show that

[TABLE]

From $p\models B$ we conclude $p\in P$, hence, there exist $i,j\in\{0,\ldots,2^{n}-1\}$ with $i\leq j$ and with $p=p_{i,j}$. Thus, $p\in\mathit{C}_{i}$. Then we have $p\models(\underline{\alpha}=\mathrm{bin}_{n}(i))$. Now, $p\models\mathrm{rightmost\_zero}(\underline{\alpha},k)$ implies $\{0,\ldots,n-1\}\setminus\mathrm{Ones}(i)\neq\emptyset$ and $k=\min(\{0,\ldots,n-1\}\setminus\mathrm{Ones}(i))$. Note that this implies $i<2^{n}-1$. We have $p_{i,j}\stackrel{{\scriptstyle L}}{{\to}}p_{i,i+1}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{i+1,i+1}$, and since $p_{i,i+1}\in P$ we have

[TABLE]

It is sufficient to show

[TABLE]

and

[TABLE]

By definition of $\sigma$ we have for all $j\in\{0,\ldots,n-1\}$

[TABLE]

and hence on the one hand $p_{i,i+1}\models(\underline{X}=\mathrm{bin}_{n}(i+1))$. Due to (3.1), we have on the other hand $p_{i,i+1}\models(\underline{\alpha}=\mathrm{bin}_{n}(i))$. This proves the first claim. For the second claim we observe that by definition of $\sigma$ also $p_{i+1,i+1}\models(\underline{X}=\mathrm{bin}_{n}(i+1))$. Since $p_{i+1,i+1}\in\mathit{C_{i+1}}$ we also have by (3.1) that $p_{i+1,i+1}\models(\underline{\alpha}=\mathrm{bin}_{n}(i+1))$ and hence $p_{i+1,i+1}\models(\underline{X}=\underline{\alpha})$.

Thus, we have constructed a cross axiom model for $\mathrm{counter}_{\mathrm{SSL},n}$. 2. 2.

Suppose there is a cross axiom model $M$ of the formula $\mathrm{counter}_{\mathrm{SSL},n}$ and some point $p_{0}\in M$ with $M,p_{0}\models\mathrm{counter}_{\mathrm{SSL},n}$. We show by induction that the claimed sequences of points $p_{1},\ldots p_{2^{n}-1}$ and $p^{\prime}_{0},\ldots p^{\prime}_{2^{n}-2}$ with the claimed properties and additionally with $p_{i}\models B$, for $0\leq i\leq 2^{n}-1$, and with $p^{\prime}_{i}\models B$, for $0\leq i\leq 2^{n}-2$, exist. In addition, we show that there exist points $t_{i}$ with $p_{0}\stackrel{{\scriptstyle L}}{{\to}}t_{i}$ and $t_{i}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{i}$, for $1\leq i\leq 2^{n}-1$. Note that the sequences $p_{0},\ldots p_{2^{n}-1}$ and $p^{\prime}_{0},\ldots p^{\prime}_{2^{n}-2}$ are supposed to form a “staircase” as in Figure 3.

By definition, $p_{0}\models B\wedge(\underline{\alpha}=\mathrm{bin}_{n}(0))$. By induction hypothesis, let us assume that for some $m$ with $0\leq m<2^{n}-1$ there exist $p_{1},\ldots,p_{m}$ and $p^{\prime}_{0},\ldots,p_{m-1}^{\prime}$ with

[TABLE]

with

[TABLE]

for $0\leq i\leq m$, and with

[TABLE]

for $0\leq i<m$, and that there are $t_{i}$ with $p_{0}\stackrel{{\scriptstyle L}}{{\to}}t_{i}$ and $t_{i}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{i}$, for $1\leq i\leq m$. Since $m<2^{n}-1$, the set $\{0,\ldots,n-1\}\setminus\mathrm{Ones}(m)$ is nonempty. With $k:=\min(\{0,\ldots,n-1\}\setminus\mathrm{Ones}(m))$ we have

[TABLE]

Due to $p_{0}\models\mathrm{counter}_{\mathrm{SSL},n}$ as well as $p_{0}\stackrel{{\scriptstyle L}}{{\to}}t_{m}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{m}$ this implies

[TABLE]

Thus, there must exist points $p^{\prime}_{m}$ and $p_{m+1}$ satisfying $p^{\prime}_{m}\models B$ as well as $p_{m}\stackrel{{\scriptstyle L}}{{\to}}p^{\prime}_{m}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{m+1}$,

[TABLE]

and

[TABLE]

We have to show

[TABLE]

and

[TABLE]

Due to the fact that $p^{\prime}_{m}$ is an element of the same cloud as $p_{m}$, and $\underline{\alpha}$ has the same value in all points in a cloud we obtain

[TABLE]

Together with

[TABLE]

this implies

[TABLE]

(the values of the leading bits $\alpha_{n-1},\ldots,\alpha_{k+1}$ of $\underline{\alpha}$ are copied to the leading bits $X_{n-1},\ldots,X_{k+1}$ and the other bits are defined explicitly by $p^{\prime}_{m}\models\mathrm{rightmost\_one}(\underline{X},k)$ so that the binary value of $\underline{X}$ is $m+1$). From $p^{\prime}_{m}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{m+1}$ and the fact that in $\mathrm{SSL}$ propositional variables are persistent we obtain $p_{m+1}\models(B\wedge(\underline{X}=\mathrm{bin}_{n}(m+1)))$. Using $p_{m+1}\models(\underline{X}=\underline{\alpha})$ we obtain $p_{m+1}\models(\underline{\alpha}=\mathrm{bin}_{n}(m+1))$. Finally, the cross property applied to $t_{m}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{m}$ and $p_{m}\stackrel{{\scriptstyle L}}{{\to}}p^{\prime}_{m}$ implies that there exists a point $t_{m+1}$ with $t_{m}\stackrel{{\scriptstyle L}}{{\to}}t_{m+1}$ and $t_{m+1}\stackrel{{\scriptstyle\Diamond}}{{\to}}p^{\prime}_{m}$. Using additionally $p_{0}\stackrel{{\scriptstyle L}}{{\to}}t_{m}$ and $p^{\prime}_{m}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{m+1}$ we obtain $p_{0}\stackrel{{\scriptstyle L}}{{\to}}t_{m+1}$ and $t_{m+1}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{m+1}$. This ends the proof of the second assertion. ∎

3.3 Alternating Turing Machines

The concept of an Alternating Turing Machine (ATM) was set forth by Chandra and Stockmeyer [3] and independently by Kozen [10] in 1976, with a joint journal publication in 1981 [2]. We are going to use a variant of ATMs with a single tape as in [14]. This is justified by the fact that one-tape ATMs can efficiently simulate multi-tape ATMs; see [3, Proposition 3.4]. For an even more efficient simulation of multi-tape ATMs by one-tape ATMs see [18].

An ATM is a nondeterministic Turing machine where some configurations are “or” configurations that accept if at least one of their successors does, while other configurations are “and” configurations that accept if all of their successors accept. The mode of each configuration (“and” vs. “or”) is determined by the state of the configuration. There are two special states called $q_{accept}$ and $q_{reject}$. All other states are either universal states or existential states.

For a relation $\delta\subseteq X\times Y$ and any $x\in X$ we write $\delta(x):=\{y\in Y\mid(x,y)\in\delta\}$.

Definition 3.3**.**

An alternating Turing Machine $M$ is a quintuple

[TABLE]

where

• •

$Q$, the set of states of $M$, is the disjoint union of the following four sets:

• –

$Q_{\exists}$, a finite set, its elements are called existential states,

• –

$Q_{\forall}$, a finite set, its elements are called universal states,

• –

$\{q_{\mathrm{accept}}\}$, a one-element set, its element is called accepting state,

• –

$\{q_{\mathrm{reject}}\}$, a one-element set, its element is called rejecting state,

• •

$\Sigma$ is a nonempty finite set, called the input alphabet,

• •

$\Gamma\supseteq\Sigma$ is a finite set containing a blank symbol $\#\not\in\Sigma$, we call $\Gamma$ the tape alphabet,

• •

$q_{0}\in Q$ is the initial state,

• •

$\delta\subseteq(Q\times\Gamma)\times(Q\times\Gamma\times\{\mathit{left},\mathit{right}\})$ is the transition relation,

and where $\delta$ satisfies the condition

[TABLE]

A configuration of an alternating Turing machine $M$ is an element $(q,z,\gamma)$ of

[TABLE]

where $q\in Q$ is the current state of the finite control, $z\in\mathbb{Z}$ is the current position of the tape head (that is, the number of the cell on which the tape head is positioned), and the function $\gamma:\mathbb{Z}\to\Gamma$ represents the current tape content and satisfies the condition $\gamma(z)=\#$ for all but finitely many $z\in\mathbb{Z}$. A configuration represents an instantaneous description of $M$ at some point in a computation. The initial configuration of $M$ on input $w=w_{1}\ldots w_{n}\in\Sigma^{*}$ with $w_{i}\in\Gamma$ for $i=1\ldots,|w|$ is

[TABLE]

where $\gamma_{w}:\mathbb{Z}\to\Gamma$ is defined by

[TABLE]

That means that at the start of the computation the tape head is positioned on cell no. [math], and the input string $w$ is contained in the cells with the numbers $1$ to $|w|$ while all other cells contain the blank $\#$.

For two configurations $c$ and $c^{\prime}$ we write $c\vdash c^{\prime}$ and say $c^{\prime}$ is a successor of $c$, if, according to the transition relation $\delta$, the configuration $c^{\prime}$ can be reached from the configuration $c$ in one step (this is defined in the usual way). The reflexive-transitive closure of $\vdash$ is denoted $\vdash^{*}$. A computation or computation path of $M$ on input $w$ is a sequence $c_{0}\vdash\ldots\vdash c_{m}$, where $c_{0}=\sigma_{M}(w)$. In the following we will only consider ATMs $M$ such that there exists a function $t:\mathbb{N}\to\mathbb{N}$ such that for any $n\in\mathbb{N}$ and any possible input string $w\in\Sigma^{n}$, any computation path of $M$ on input $w$ has length at most $t(n)$, that is, if $c_{0},\ldots,c_{m}$ is a computation path of $M$ on input $w$ then $m\leq t(n)$. In this case we say that $M$ works in time $t$. For such machines $M$ we can define the language $L(M)\subseteq\Sigma^{*}$ recognized by $M$ as follows: for $w\in\Sigma^{*}$

[TABLE]

An accepting tree of $M$ on input $w$ is a finite rooted and labeled tree each of whose nodes is labeled with a configuration of $M$ such that the following five properties hold true:

1. I.

The root of the tree is labeled with the initial configuration $\sigma_{M}(w)$ of $M$ on input $w$. 2. II.

If $c$ is the label of an internal node of the tree then the labels of its successors are configurations $c^{\prime}$ satisfying $c\vdash c^{\prime}$ (note that this implies that the state $q$ of $c$ is an element of $Q_{\exists}\cup Q_{\forall}$). 3. III

If $c$ is the label of an internal node of the tree then the labels of its successors are pairwise different configurations. 4. IV.

If $c$ is the label of an internal node of the tree and the state $q$ of $c$ is an element of $Q_{\forall}$ then for every configuration $c^{\prime}$ with $c\vdash c^{\prime}$ there exists a successor node labeled with $c^{\prime}$. 5. V.

If $c$ is the label of a leaf of the tree then the state of $c$ is equal to $q_{\mathrm{accept}}$.

Note that these conditions imply that, if $c$ is the label of a node of the tree and the state $q$ of $c$ is an element of $Q_{\exists}$, then this node is an internal node, hence, it has a successor. Let the height of a rooted tree be the length of the longest path in the tree. It is clear that if there is an accepting tree of $M$ on input $w$ then its height is at most $t(|w|)$.

The time complexity class $\mathrm{AEXPTIME}$ is the class of all languages $L$ such that there exist an alternating Turing machine $M$ with $L=L(M)$ and a polynomial $p$ such that $M$ works in time $2^{p(n)}$. We will make use of the fundamental fact $\mathrm{AEXPTIME}=\mathrm{EXPSPACE}$ [3, Corollary 3.6].

For technical purposes we will also need the following notion. A partial tree of $M$ on input $w$ is a finite rooted and labeled tree each of whose nodes is labeled with a configuration of $M$ that satisfies the same four properties I, II, III, and IV as an accepting tree of $M$ on input $w$ and instead of the property V the following weaker property:

1. $\mathrm{V}^{\prime}$.

If $c$ is the label of a leaf of the tree then the state of $c$ is different from $q_{\mathrm{reject}}$.

It is clear that any accepting tree of $M$ on input $w$ is a partial tree of $M$ on input $w$. Usually we will write a partial tree of $M$ on input $w$ as a triple $T=(V,E,c)$ where $V$ is the set of nodes of the tree $T$, where $E\subseteq V\times V$ is the set of edges of the tree $T$ (note that the root $\mathit{root}$ of the tree is uniquely determined by $V$ and $E$: it is the only node that does not have an incoming edge), and where $c:V\to Q\times\mathbb{Z}\times\Gamma^{\mathbb{Z}}$ is the labeling of the tree. Let $E^{*}$ be the reflexive-transitive closure of $E$. We will often need the following data associated with any computation node $v\in V$:

• •

The time $\mathit{time}(v)$ of $v$. This is the number of edges of the unique path in $T$ from $\mathit{root}$ to $v$. Note that $\mathit{time}(\mathit{root})=0$.

• •

The configuration $c(v)$ of $v$. This is the configuration with which the node $v$ is labeled.

• •

The state $\mathit{state}(v)$ of the configuration $c(v)$.

• •

The position $\mathit{pos}(v)$ of the tape head in the configuration $c(v)$.

• •

The symbol $\mathit{read}(v)$ in the cell $\mathit{pos}(v)$ in the configuration $c(v)$.

• •

The predecessor $\mathit{pred}(v)$ of $v$ in the tree $T$, for $v\neq\mathit{root}$.

• •

The symbol $\mathit{written}(v)$ that has been written in the computation step that lead to this node $v$, for $v\neq\mathit{root}$. Note that this is the symbol now contained in the cell $\mathit{pos}(\mathit{pred}(v))$ on which the tape head was positioned in the previous configuration.

4 Reduction of Alternating Turing Machines Working in Exponential Time to $\mathrm{SSL}$

In this section we prove the following theorem.

Theorem 4.1**.**

The satisfiability problem of $\mathrm{SSL}$ is $\mathrm{EXPSPACE}$-hard under logarithmic space reduction.

As explained before, we are going to show this by showing that any language $L$ recognized by an Alternating Turing Machine working in exponential time can be reduced in logarithmic space to the satisfiability problem of $\mathrm{SSL}$.

In the following subsection we will first describe the idea of the reduction and then define the reduction function $f_{\mathrm{SSL}}$ in detail. In Subsection 4.2 we will show that it can be computed in logarithmic space. In the final two subsections we are going to show that it is corrrect. First we show that in case $w\in L$ the formula $f_{\mathrm{SSL}}(w)$ is $\mathrm{SSL}$-satisfiable by explicitly constructing a cross axiom model for $f_{\mathrm{SSL}}(w)$. In the last section we show that if $f_{\mathrm{SSL}}(w)$ is $\mathrm{SSL}$-satisfiable then $w$ is an element of $L$.

4.1 Construction of the Formula

Let $L\in\mathrm{EXPSPACE}$ be an arbitrary language over some alphabet $\Sigma$, that is, $L\subseteq\Sigma^{*}$. We are going to show that there is a logspace computable function $f_{\mathrm{SSL}}$ mapping strings to strings such that, for any $w\in\Sigma^{*}$,

• •

$f_{\mathrm{SSL}}(w)$ is a bimodal formula and

• •

$f_{\mathrm{SSL}}(w)$ is $\mathrm{SSL}$-satisfiable if, and only if, $w\in L$.

Once we have shown this, we have shown the result. In order to define this desired reduction function $f_{\mathrm{SSL}}$, we are going to make use of an Alternating Turing Machine for $L$. Since $\mathrm{EXPSPACE}=\mathrm{AEXPTIME}$, there exist an Alternating Turing Machine $M=(Q,\Sigma,\Gamma,q_{0},\delta)$ and a univariate polynomial $p$ such that $M$ accepts $L$, that is, $L(M)=L$, and such that the time used by $M$ on arbitrary input of length $n$ is bounded by $2^{p(n)}-1$. We can assume without loss of generality $Q=\{0,\ldots,|Q|-1\}$, $\Gamma=\{0,\ldots,|\Gamma|-1\}$, that the coefficients of the polynomial $p$ are natural numbers and that, for all $n\in\mathbb{N}$, we have $p(n)\geq n$ and $p(n)\geq 1$. In the following, whenever we have fixed some $n\in\mathbb{N}$, we set

[TABLE]

Let us consider an input word $w\in\Sigma^{n}$ of length $n$, for some $n\in\mathbb{N}$, and let us sketch the main idea of the construction of the formula $f_{\mathrm{SSL}}(w)$. The formula $f_{\mathrm{SSL}}(w)$ will describe the possible computations of $M$ on input $w$ in the following sense: any cross axiom model of $f_{\mathrm{SSL}}(w)$ will essentially contain an accepting tree of $M$ on input $w$, and if $w\in L(M)$ then there exists an accepting tree of $M$ on input $w$ and one can turn this into a cross axiom model of $f_{\mathrm{SSL}}(w)$. In such a model, any node in an accepting tree of $M$ on input $w$ will be modeled by a cloud (that is, by an $\stackrel{{\scriptstyle L}}{{\to}}$-equivalence class) in which certain shared variables (we use the notion “shared variables” in the same sense as in Subsection 3.1) will have values that describe the data of the computation node that are important in this computation step. Which data are these? First of all, we need the time of the computation node. We assume that the computation starts with the initial configuration of $M$ on input $w$ at time [math]. Since the ATM $M$ needs at most $2^{N}-1$ time steps, we can store the time of each computation node in a binary counter counting from [math] to $2^{N}-1$. Since during each time step at most one additional cell either to the right or to the left of the previous cell can be visited, we can describe any configuration reachable during a computation of $M$ on input $w$ by the following data:

• •

the current content of the tape, which is a string in $\Gamma^{2\cdot(2^{N}-1)+1}=\Gamma^{2^{N+1}-1}$,

• •

the current tape head position, which is a number in $\{0,\ldots,2^{N+1}-2\}$.

We assume that in the initial configuration on input $w$ the tape content is $\#^{2^{N}}w\#^{2^{N}-1-n}$ (remember that we use $\#$ for the blank symbol) and that the tape head scans the blank $\#$ to the left of the first symbol of $w$, that is, the position of the tape head is $2^{N}-1$. If a cloud in a cross axiom model of $f_{\mathrm{SSL}}(w)$ describes a computation node of $M$ on input $w$ then in this cloud the following shared variables will have the following values:

• •

a vector $\underline{\alpha}^{\mathrm{time}}=(\alpha^{\mathrm{time}}_{N-1},\ldots,\alpha^{\mathrm{time}}_{0})$ giving in binary the current time of the computation,

• •

a vector $\underline{\alpha}^{\mathrm{pos}}=(\alpha^{\mathrm{pos}}_{N},\ldots,\alpha^{\mathrm{pos}}_{0})$ giving in binary the current position of the tape head,

• •

a vector $\underline{\alpha}^{\mathrm{state}}=(\alpha^{\mathrm{state}}_{0},\ldots,\alpha^{\mathrm{state}}_{|Q|-1})$ giving in unary the current state of the computation (here “unary” means: exactly one of the shared variables $\alpha^{\mathrm{state}}_{i}$ will be true, namely the one with $i$ being the current state),

• •

a vector $\underline{\alpha}^{\mathrm{written}}=(\alpha^{\mathrm{written}}_{0},\ldots,\alpha^{\mathrm{written}}_{|\Gamma|-1})$ giving in unary the symbol that has just been written into the cell that has just been left, unless the cloud corresponds to the first node in the computation tree — in that case the value of this vector is irrelevant (here “unary” means: exactly one of the variables $\alpha^{\mathrm{written}}_{i}$ will be true, namely the one with $i$ being the symbol that has just been written),

• •

a vector $\underline{\alpha}^{\mathrm{read}}=(\alpha^{\mathrm{read}}_{0},\ldots,\alpha^{\mathrm{read}}_{|\Gamma|-1})$ giving in unary the symbol in the current cell (here “unary” means: exactly one of the shared variables $\alpha^{\mathrm{read}}_{i}$ will be true, namely the one with $i$ being the symbol in the current cell).

The formula $f_{\mathrm{SSL}}(w)$ has to ensure that for any possible computation step in an accepting tree starting from such a computation node there exists a cloud describing the corresponding successor node in the accepting tree. In this new cloud, the value of the counter for the time $\underline{\alpha}^{\mathrm{time}}$ has to be incremented. This can be done by the technique described in Subsection 3.2 for implementing a binary counter. In parallel, we have to make sure that in this new cloud also the vectors $\underline{\alpha}^{\mathrm{pos}}$, $\underline{\alpha}^{\mathrm{state}}$, $\underline{\alpha}^{\mathrm{written}}$, and $\underline{\alpha}^{\mathrm{read}}$ are set to the right values. For the vectors $\underline{\alpha}^{\mathrm{pos}}$, $\underline{\alpha}^{\mathrm{state}}$, and $\underline{\alpha}^{\mathrm{written}}$ these values can be computed using the corresponding element of the transition relation $\delta$ of the ATM. For example, $\underline{\alpha}^{\mathrm{pos}}$ has to be decremented by one if the tape head moves to the left, and it has to be incremented by one if the tape head moves to the right. Also the new state (to be stored in $\underline{\alpha}^{\mathrm{state}}$) and the symbol written into the cell that has just been left (to be stored in $\underline{\alpha}^{\mathrm{written}}$) are determined by the data of the previous computation node and by the corresponding element of the transition relation $\delta$.

But the vector $\underline{\alpha}^{\mathrm{read}}$ is supposed to describe the symbol in the current cell. This symbol is not determined by the current computation step but has either been written the last time when this cell has been visited during this computation or, when this cell has never been visited before, the symbol in this cell is still the one that was contained in this cell before the computation started. How can one ensure that $\underline{\alpha}^{\mathrm{read}}$ is set to the right value? If the current cell has never been visited before, we have to make sure that the value is set to the correct value describing the inital content of this cell. Otherwise, we make use of the cross property. The point in the new cloud whose existence is enforced by the formula must have a cross point in any cloud corresponding to any previous computation node. The idea is that one of these cross points picks up the right value in the right cloud. We are going to make sure that the cloud is identified that corresponds to the configuration after the previous visit of the same cell during the computation. Then in the cloud corresponding to this configuration the value of $\underline{\alpha}^{\mathrm{written}}$ will tell us the symbol that has been written into the current cell during the previous visit. In order to identify the correct cloud of the step after the previous visit of the current cell and to copy the value of the symbol, the formula $f_{\mathrm{SSL}}(w)$ will ensure that any cloud describing a computation node will contain a point in which the following (persistent!) propositional variables have the following values:

• •

a vector $\underline{X}^{\mathrm{time}}=(X^{\mathrm{time}}_{N-1},\ldots,X^{\mathrm{time}}_{0})$ giving in binary the current time of the computation,

• •

a vector $\underline{X}^{\mathrm{pos}}=(X^{\mathrm{pos}}_{N},\ldots,X^{\mathrm{pos}}_{0})$ giving in binary the current position of the tape head, that is the position of the current cell,

• •

a vector $\underline{X}^{\mathrm{read}}=(X^{\mathrm{read}}_{0},\ldots,X^{\mathrm{read}}_{|\Gamma|-1})$ giving in unary the symbol in the current cell, (here “unary” means: exactly one of the variables $X^{\mathrm{read}}_{i}$ will be true, namely the one with $i$ being the symbol in the current cell).

• •

a vector $\underline{X}^{\text{time-apv}}=(X^{\text{time-apv}}_{N-1},\ldots,X^{\text{time-apv}}_{0})$ giving in binary the time one step after the previous visit of the cell, if it has been visited before (“time-apv” stands for “time after previous visit”); otherwise this vector will have the binary value [math].

Now we come to the formal definition of the formula $f_{\mathrm{SSL}}(w)$. The formula $f_{\mathrm{SSL}}(w)$ will have the following structure:

[TABLE]

The formula $f_{\mathrm{SSL}}(w)$ will contain the following propositional variables:

[TABLE]

For $\mathit{string}\in\{\mathrm{time},\mathrm{pos},\mathrm{state},\mathrm{written},\mathrm{read}\}$ and natural numbers $k$ we define

[TABLE]

These formulas $\alpha^{\mathit{string}}_{k}$ are the shared variables we talked about above. We are now going to define the subformulas of $f_{\mathrm{SSL}}(w)$. We will use the abbreviations introduced above, in Table 1, and in Table 2.

The models of the formula $f_{\mathrm{SSL}}(w)$ will contain certain “information” points that will realize an accepting tree of $M$ on input $w$ if, and only if, $w\in L$. Besides these information points there will also be other, “auxiliary”, points (and an $\stackrel{{\scriptstyle L}}{{\to}}$-equivalence class not containing any information points) whose sole purpose is to make the mechanism of shared variables work. In several formulas we need to distinguish between the information points and the other, auxiliary, points. It turns out that this can be done simply by the truth value of the propositional variable $B$.

The following formula makes sure that in each of the vectors of shared variables that describe in a unary way the current state respectively the written symbol respectively the current symbol, exactly one shared variable is true:

[TABLE]

The vector $\underline{X}^{\mathrm{read}}$ will satisfy the same uniqueness condition automatically.

The following formula ensures that the variables in the cloud corresponding to the first node in a computation tree get the correct values. The computation starts at time [math] with the tape head at position $2^{N}-1$ and in the state $q_{0}$ and with the blank symbol $\#$ in the current cell.

[TABLE]

The following formula ensures that the vector $\underline{X}^{\text{time-apv}}$ stores the time after the previous visit of the same cell, if it has been visited before. If it has never been visited before, this vector gets the binary value [math].

[TABLE]

We explain this formula. The time $\underline{X}^{\text{time-apv}}$ after the previous visit of the current cell $\underline{X}^{\mathrm{pos}}$ is certainly at most as large as the current time $\underline{X}^{\mathrm{time}}$. When during the computation at an earlier time a cell has been visited that is different from the current one then one plus the time of that visit is certainly not the time after the previous visit of the current cell. When during the computation at an earlier time the current cell has been visited then the time of that visit is a strict lower bound for the time after the previous visit of the current cell. Together these conditions ensure that $\underline{X}^{\text{time-apv}}$ gets the correct value.

The following formula ensures that the vector $\underline{X}^{\mathrm{read}}$ stores (in unary form) the symbol in the current cell.

[TABLE]

We explain this formula. If the current cell has never before been visited (this is the case iff the vector $\underline{X}^{\text{time-apv}}$ has the binary value [math]) then the vector $\underline{X}^{\mathrm{read}}$ is forced to store in unary format the initial symbol in the current cell. This is either a symbol $w_{i}$ of the input string or the blank $\#$. If the current cell has been visited before (this is the case iff the vector $\underline{X}^{\text{time-apv}}$ has a binary value strictly greater than [math]) then in the cloud corresponding to the time stored in $\underline{X}^{\text{time-apv}}$ the vector $\underline{\alpha}^{\mathrm{written}}$ describes the symbol that has been written into the current cell during the previous visit. Therefore, this value is copied into the vector $\underline{X}^{\mathrm{read}}$.

Next, we wish to define the formula $\mathit{computation}$ that describes the computation steps. We have to distinguish between the two cases whether the tape head is going to move to the left or to the right. If in a computation step the symbol $\theta\in\Gamma$ is written into the current cell, if the tape head moves to the right, and if the new state after this step is the state $r\in Q$, then the following formula guarantees the existence of a point and its cloud with suitable values in the shared variables and in the persistent propositional variables.

[TABLE]

We explain this formula. The procedure is quite similar to the one of the formula $\mathrm{counter}_{SSL,n}$ in Subsection 3.2 for a binary counter. The first three lines of the formula make sure that there is a point in the same cloud as the current point such that in this new point the binary value of the persistent variable vector $\underline{X}^{\mathrm{time}}$ is larger by one than the binary value of the shared variable vector $\underline{\alpha}^{\mathrm{time}}$ and that in this new point the binary value of the persistent variable vector $\underline{X}^{\mathrm{pos}}$ is larger by one than the binary value of the shared variable vector $\underline{\alpha}^{\mathrm{pos}}$. The last two lines ensure the existence of a $\stackrel{{\scriptstyle\Diamond}}{{\to}}$-successor of this new point in which the shared variable vectors $\underline{\alpha}^{\mathrm{time}}$, $\underline{\alpha}^{\mathrm{pos}}$, $\underline{\alpha}^{\mathrm{state}}$, $\underline{\alpha}^{\mathrm{written}}$, and $\underline{\alpha}^{\mathrm{read}}$ get the correct new values.

If in a computation step the symbol $\theta\in\Gamma$ is written into the current cell, if the tape head moves to the left, and if the new state after this step is the state $r\in Q$, then the following formula guarantees the existence of a point and its cloud with suitable values in the shared variables and in the persistent propositional variables.

[TABLE]

This formula is very similar to the previous one with the exception that here the binary counter for the position of the tape head is decremented.

The computation is modeled by the following subformula. Remember that $Q$ is the disjoint union of the sets $\{q_{\mathrm{accept}}\}$, $\{q_{\mathrm{reject}}\}$, $Q_{\forall}$, $Q_{\exists}$.

[TABLE]

Finally, the subformula $\mathit{no\_reject}$ is defined as follows.

[TABLE]

We have completed the description of the formula $f_{\mathrm{SSL}}(w)$ for $w\in\Sigma^{*}$. It is clear that $f_{\mathrm{SSL}}(w)$ is a bimodal formula, for any $w\in\Sigma^{*}$. We still have to show two claims:

The function $f_{\mathrm{SSL}}$ can be computed in logarithmic space. 2. 2.

For any $w\in\Sigma^{*}$,

[TABLE]

The first claim will be shown in the following section. The two directions of the second claim will be shown separately in Subsections 4.3 and 4.4.

4.2 LOGSPACE Computability of the Reduction

For the first claim, we observe that there are three kinds of subformulas of $f_{\mathrm{SSL}}(w)$:

subformulas that do not depend on the input string $w$ at all, 2. 2.

subformulas that depend only on the length $n$ of the input string $w$ but not on its symbols $w_{1},\ldots,w_{n}$, 3. 3.

subformulas that depend on the particular symbols $w_{1},\ldots,w_{n}$ of the input string $w$.

The subformula $K\Box\mathit{uniqueness}$ is of the first type. Therefore, it can be written using only a constant amount of workspace. And there is only one subformula of the third type, the subformula $K\Box\mathit{get\_the\_right\_symbol}$. All other subformulas are of the second type. All of them contain vectors of propositional variables of length at most $N+1$ or conjunctions or disjunctions of length at most $N+1$, where $N=p(n)$. And all of these vectors and lists of conjunctions or disjunctions have a very regular structure. This applies also to the only subformula of the third type. This regular structure makes it possible to write down these formulas using a fixed (that means: independent of the input string $w$) number of counters that can count up to $N$. But such counters can be implemented in binary using not more than $O(\log N)=O(\log n)$ space. Hence, given a string $w$, the whole formula $f_{\mathrm{SSL}}(w)$ can be computed using not more than logarithmic space.

4.3 Construction of a Model

We come to the second claim. First, we show the direction from left to right. Let us assume $w\in L$. We will construct a cross axiom model $(W,\stackrel{{\scriptstyle L}}{{\to}},\stackrel{{\scriptstyle\Diamond}}{{\to}},\sigma)$ with a point $p_{\mathit{root},\mathit{root}}\in W$ such that $p_{\mathit{root},\mathit{root}}\models f_{\mathrm{SSL}}(w)$. There exists an accepting tree $T=(V,E,c)$ of $M$ on input $w$, where $V$ is the set of nodes of $T$, where $E\subseteq V\times V$ is the set of edges, and where the function $c:V\to Q\times\{0,\ldots,2^{N+1}-2\}\times\Gamma^{2^{N+1}-1}$ labels each node with a configuration (remember the discussion about the description of configurations at the beginning of Subsection 4.1). Let $\mathit{root}\in V$ be the root of $T$. The set $W$ is defined to be the (disjoint) union of the following three sets $P$, $U$, and $S$. We define

[TABLE]

For the definition of $U$ we use the following set as an index set:

[TABLE]

We define

[TABLE]

where $\top$ is a special element not contained in $V$. We extend the binary relation $E^{*}$ on $V$ to a binary relation $\widetilde{E}$ on $V\cup\{\top\}$ by

[TABLE]

We define the set $S$ by

[TABLE]

As the relation $\stackrel{{\scriptstyle L}}{{\to}}$ is supposed to be an equivalence relation we can define it by defining the $\stackrel{{\scriptstyle L}}{{\to}}$-equivalence classes. These are the sets

[TABLE]

for all $v\in V$, and the set

[TABLE]

We define the relation $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ by:

[TABLE]

It is straightforward to check that $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ is reflexive and transitive. The cross property is satisfied as well. Thus, $(W,\stackrel{{\scriptstyle L}}{{\to}},\stackrel{{\scriptstyle\Diamond}}{{\to}})$ is an cross axiom frame. Finally, we define the valuation $\sigma$ as follows.

[TABLE]

and

[TABLE]

for $k\in\{0,\ldots,N-1\}$,

[TABLE]

for $k\in\{0,\ldots,N\}$,

[TABLE]

for $q\in Q$,

[TABLE]

for $\gamma\in\Gamma$. It is obvious that all propositional variables are persistent. Thus, we have defined a cross axiom model $(W,\stackrel{{\scriptstyle L}}{{\to}},\stackrel{{\scriptstyle\Diamond}}{{\to}},\sigma)$. We claim that $p_{\mathit{root},\mathit{root}}\models f_{\mathrm{SSL}}(w)$. For an illustration of an important detail of the structure see Figure 4.

We start with some preliminary observations. First, for any cloud, any shared variable has the same truth values in all points in the cloud. Secondly,

[TABLE]

for all $y\in W$. So, the points in $P$ are the “information” points. On the other hand, as the cloud $\mathit{Cloud}_{\top}$ does not contain any elements from $P$, for all points $y\in\mathit{Cloud}_{\top}$ we have $y\models K\neg B$, hence,

[TABLE]

for all $\mathit{string}\in\{\mathrm{times},\mathrm{pos},\mathrm{state},\mathrm{written},\mathrm{read}\}$ and all $k$. That means, the truth value of any shared variable in the cloud $\mathit{Cloud}_{\top}$ is false. We claim that in the other clouds all shared variables have the values indicated by their names, namely,

[TABLE]

for $v\in V$ and $y\in\mathit{Cloud}_{v}$,

[TABLE]

for $\gamma\in\Gamma$, $v\in V\setminus\{\mathit{root}\}$ and $y\in\mathit{Cloud}_{v}$, and

[TABLE]

for $\gamma\in\Gamma$ and $y\in\mathit{Cloud}_{\mathit{root}}$. This can be checked similarly as the corresponding claim (3.1) in the proof of Proposition 3.2. We prove the assertions about $\alpha^{\mathrm{written}}_{\gamma}$ and leave the proofs of the other assertions to the reader. Let us fix some $\gamma\in\Gamma$. Note that, for all $p^{\prime}\in P$, we have $p^{\prime}\models\neg A^{\mathrm{written}}_{\gamma}$, hence

[TABLE]

Furthermore, $u_{\top,i}\models K\neg B$ for all $i\in I$. Since for all $v\in V\cup\{\top\}$ and $i\in I$ we have $u_{v,i}\stackrel{{\scriptstyle\Diamond}}{{\to}}u_{\top,i}$ we obtain $u_{v,i}\models\Diamond K\neg B$ for all $v\in V\cup\{\top\}$ and $i\in I$. Hence,

[TABLE]

This shows that, for any $v\in V$, the shared variable $\alpha^{\mathrm{written}}_{\gamma}=L(A^{\mathrm{written}}_{\gamma}\wedge\Box LB)$ is true in the cloud $\mathit{Cloud}_{v}$ if, and only if, there exists some $s^{\prime}\in\mathit{Cloud}_{v}\cap S$ with $s^{\prime}\models A^{\mathrm{written}}_{\gamma}\wedge\Box LB$. As $p^{\prime}\models B$ for all $p^{\prime}\in P$ and any $s^{\prime}\in S$ is $\stackrel{{\scriptstyle L}}{{\to}}$-equivalent to some $p^{\prime}\in P$, we have $s^{\prime}\models LB$, for all $s^{\prime}\in S$. Actually, for $s^{\prime}\in S$ we even have $s^{\prime}\models\Box LB$ as $s^{\prime}$ does not have any $\stackrel{{\scriptstyle\Diamond}}{{\to}}$-successor besides itself. Thus, for any $v\in V$, the shared variable $\alpha^{\mathrm{written}}_{\gamma}=L(A^{\mathrm{written}}_{\gamma}\wedge\Box LB)$ is true in the cloud $\mathit{Cloud}_{v}$ if, and only if, there exists some $s^{\prime}\in\mathit{Cloud}_{v}\cap S$ with $s^{\prime}\models A^{\mathrm{written}}_{\gamma}$. The elements $s^{\prime}\in\mathit{Cloud}_{v}\cap S$ have the form $s^{\prime}=s_{v,i}$ for some $i\in I$. On the one hand, we observe that, for $v\in V$ and $i\in I$, $s_{v,i}\models A^{\mathrm{written}}_{\gamma}\iff i=(\mathrm{written},\gamma)$. On the other hand, for $v\in V$ we have

[TABLE]

Thus, we have shown the desired claims:

[TABLE]

for $\gamma\in\Gamma$, $v\in V\setminus\{\mathit{root}\}$ and $y\in\mathit{Cloud}_{v}$, and

[TABLE]

for $\gamma\in\Gamma$ and $y\in\mathit{Cloud}_{\mathit{root}}$.

It is clear from the definition of the valuation $\sigma$ that in the points in $P$ the variable vectors $\underline{X}^{\mathrm{time}}$, $\underline{X}^{\mathrm{pos}}$, $\underline{X}^{\mathrm{read}}$, and $\underline{X}^{\text{time-apv}}$ have the values indicated by their names:

[TABLE]

for $v,x\in V$ satisfying $vE^{*}x$.

Now we are prepared to show $p_{\mathit{root},\mathit{root}}\models f_{\mathrm{SSL}}(w)$. Our observations about the values of the shared variable vectors $\underline{\alpha}^{\mathrm{state}}$, $\underline{\alpha}^{\mathrm{read}}$, and $\underline{\alpha}^{\mathrm{written}}$ show

[TABLE]

(remember that $B$ is false in all points of the cloud $\mathit{Cloud}_{\top}$). Similarly, our observations about the values of the shared variable vectors $\underline{\alpha}^{\mathrm{time}}$, $\underline{\alpha}^{\mathrm{pos}}$, $\underline{\alpha}^{\mathrm{state}}$, and $\underline{\alpha}^{\mathrm{read}}$ imply

[TABLE]

As the state of any node in the accepting tree $T$ of $M$ on input $w$ is different from $q_{\mathrm{reject}}$, our observations about the value of the vector $\underline{\alpha}^{\mathrm{state}}$ (in any cloud $\mathit{Cloud}_{v}$ for $v\in V$ the shared variable $\alpha^{\mathrm{state}}_{q}$ is true if, and only if, $q=\mathit{state}(v)$, and in the cloud $\mathit{Cloud}_{\top}$ all shared variables are false) shows

[TABLE]

Next, we show

[TABLE]

As the variable $B$ is true only in the elements of $P$, it is sufficient to show for all $v,x\in V$ with $vE^{*}x$

[TABLE]

We distinguish between the two cases whether the cell $\mathit{pos}(x)$ under the tape head in the configuration $c(x)$ has been visited on the path from $\mathit{root}$ to $x$ before $x$ is reached or not.

First let us assume that the cell $\mathit{pos}(x)$ has not been visited before. Then $p_{v,x}\models(\underline{X}^{\text{time-apv}}=\mathrm{bin}_{N}(0))$, hence $p_{v,x}\models(\underline{X}^{\text{time-apv}}\leq\underline{X}^{\mathrm{time}})$ and $p_{v,x}\models(\underline{X}^{\text{time-apv}}\neq\underline{\alpha}^{\mathrm{time}}+1)$, that is, the formulas in the first two lines are true in $p_{v,x}$. And if we have $p_{v,x}\models(\underline{\alpha}^{\mathrm{time}}<\underline{X}^{\mathrm{time}})$ then, due to $vE^{*}x$, the point $v$ is a point on the path from $\mathit{root}$ to $\mathit{pred}(x)$. Our assumption (that the cell $\mathit{pos}(x)$ has not been visited before $x$ is reached) implies $p_{v,x}\models\neg(\underline{\alpha}^{\mathrm{pos}}=\underline{X}^{\mathrm{pos}})$. Hence the formula in the third line is true in $p_{v,x}$ as well.

Now, let us assume that the cell $\mathit{pos}(x)$ has been visited on the path from $\mathit{root}$ to $x$ before $x$ is reached. Let $x^{\prime}$ be the last node on the path from $\mathit{root}$ to $\mathit{pred}(x)$ with $\mathit{pos}(x^{\prime})=\mathit{pos}(x)$. Let $i:=\mathit{time}(x^{\prime})$ and $j:=1+i$. Then $i<\mathit{time}(x)$ and $j\leq\mathit{time}(x)$. As $p_{v,x}\models(\underline{X}^{\text{time-apv}}=\mathrm{bin}_{N}(j))$, the formula in the first line above is true, that is, $p_{v,x}\models(\underline{X}^{\text{time-apv}}\leq\underline{X}^{\mathrm{time}})$. For the formula in the second line, let us assume $p_{v,x}\models(\underline{\alpha}^{\mathrm{time}}<\underline{X}^{\mathrm{time}})\wedge(\underline{\alpha}^{\mathrm{pos}}\neq\underline{X}^{\mathrm{pos}})$. Then $v$ is a node on the path from $\mathit{root}$ to $\mathit{pred}(x)$ with $\mathit{pos}(v)\neq\mathit{pos}(x)$. Hence, $v\neq x^{\prime}$, hence, $\mathit{time}(v)\neq\mathit{time}(x^{\prime})$, hence, $j\neq\mathit{time}(v)+1$, hence, $p_{v,x}\models(\underline{X}^{\text{time-apv}}\neq\underline{\alpha}^{\mathrm{time}}+1)$. For the formula in the third line, let us assume $p_{v,x}\models(\underline{\alpha}^{\mathrm{time}}<\underline{X}^{\mathrm{time}})\wedge(\underline{\alpha}^{\mathrm{pos}}=\underline{X}^{\mathrm{pos}})$. Then $v$ is a node on the path from $\mathit{root}$ to $\mathit{pred}(x)$ with $\mathit{pos}(v)=\mathit{pos}(x)$, that is, with the property that in this node the same cell is visited as in the node $x$. As $x^{\prime}$ is the last node on the path from $\mathit{root}$ to $\mathit{pred}(x)$ with this property, we have $\mathit{time}(v)\leq\mathit{time}(x^{\prime})$, hence, $j=1+i=1+\mathit{time}(x^{\prime})>\mathit{time}(v)$, hence $p_{v,x}\models(\underline{\alpha}^{\mathrm{time}}<\underline{X}^{\text{time-apv}})$.

Next, we show

[TABLE]

It is sufficient to show for all $y\in W$, $y\models\mathit{get\_the\_right\_symbol}$. There are two cases to be considered. In each of them, due to the presence of the variable $B$, we need to consider only points $y\in P$. Let us consider elements $v,x\in V$ with $vE^{*}x$. It is sufficient to show $p_{v,x}\models\mathit{get\_the\_right\_symbol}$. We distinguish between the two cases considered in this formula. First, let us assume $p_{v,x}\models(\underline{X}^{\text{time-apv}}=\mathrm{bin}_{N}(0))$. We have to show that in this case

[TABLE]

According to our observations about the value of $\underline{X}^{\text{time-apv}}$, the cell $\mathit{pos}(x)$ under the tape head in the configuration $c(x)$ has not been visited on the path from $\mathit{root}$ to $\mathit{pred}(x)$. Thus, the symbol $\mathit{read}(x)$ is still the initial symbol in the cell $\mathit{pos}(x)$. Let us call this symbol $\gamma$. Then $p_{v,x}\models X^{\mathrm{read}}_{\gamma}$, and

[TABLE]

On the other hand, $p_{v,x}\models(\underline{X}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(\mathit{pos}(x)))$. We have shown the assertion.

Now, let us assume

[TABLE]

We have to show that in this case

[TABLE]

The assumption $p_{v,x}\models(\underline{X}^{\text{time-apv}}>\mathrm{bin}_{N}(0))$ implies that the cell $\mathit{pos}(x)$ has already been visited on the path from $\mathit{root}$ to $\mathit{pred}(x)$ and that $p_{v,x}\models(\underline{X}^{\text{time-apv}}=\mathrm{bin}_{N+1}(1+i))$ where $i=\mathit{time}(x^{\prime})$ and $x^{\prime}$ is the last node on the path from $\mathit{root}$ to $\mathit{pred}(x)$ with $\mathit{pos}(x^{\prime})=\mathit{pos}(x)$. The assumption $p_{v,x}\models(\underline{\alpha}^{\mathrm{time}}=\underline{X}^{\text{time-apv}})$ implies $x^{\prime}=\mathit{pred}(v)$. But then in the point $v$ the vector $\underline{\alpha}^{\mathrm{written}}$ encodes in unary the symbol that was written into the cell $\mathit{pos}(x)$ in the computation step from $x^{\prime}$ to $v$. If we call this symbol $\gamma$, this means $p_{v,x}\models\alpha^{\mathrm{written}}_{\gamma}$. This is still the symbol in the cell $\mathit{pos}(x)$ when $x$ is reached, hence, $p_{v,x}\models X^{\mathrm{read}}_{\gamma}$. So, we have indeed shown

[TABLE]

Finally, we show

[TABLE]

It is sufficient to show

[TABLE]

for all $y\in W$. We will separately treat the conjunctions over the set $(q,\eta)\in Q_{\exists}\times\Gamma$ and over the set $Q_{\forall}\times\Gamma$. Let us fix a pair $(q,\eta)\in Q_{\exists}\times\Gamma$ and let us assume that $y\in W$ is a point with $y\models(\alpha^{\mathrm{state}}_{q}\wedge\alpha^{\mathrm{read}}_{\eta})$. We have to show that there is an element $(r,\theta,\mathit{left})\in\delta(q,\eta)$ such that $y\models\mathit{compstep}_{\mathrm{left}}(r,\theta)$ or that there is an element $(r,\theta,\mathit{right})\in\delta(q,\eta)$ such that $y\models\mathit{compstep}_{\mathrm{right}}(r,\theta)$. As in the cloud $\mathit{Cloud}_{\top}$ the truth value of any shared variable is false, the assumption $y\models(\alpha^{\mathrm{state}}_{q}\wedge\alpha^{\mathrm{read}}_{\eta})$ implies that there exists some $v\in V$ with $y\in\mathit{Cloud}_{v}$. Furthermore, $q=\mathit{state}(v)$ and $\eta=\mathit{read}(v)$. As $T$ is an accepting tree and the state $q$ of $c(v)$ is an element of $Q_{\exists}$, the node $v$ is an inner node of $T$, hence, it has a successor $v^{\prime}$. Let us assume that $((q,\eta),(r,\theta,\mathit{left}))\in\delta$ is the element of the transition relation $\delta$ that leads from $v$ to $v^{\prime}$ (the case that this element is of the form $((q,\eta),(r,\theta,\mathit{right}))$ is treated analogously). We claim that then

[TABLE]

Let us check this. Let us assume that, for some $k\in\{0,\ldots,N-1\}$ and for some $l\in\{0,\ldots,N\}$,

[TABLE]

The number $i:=\mathit{time}(v)$ is an element of $\{0,\ldots,2^{N}-2\}$ because $v$ is an inner point of the tree $T$ and the length of any computation path is at most $2^{N}-1$, and the number $j:=\mathit{pos}(v)$ is an element of $\{1,\ldots,2^{N+1}-3\}$ because the computation starts in cell $2^{N}-1$ and because during each computation step the tape head can move at most one step to the left or to the right. We obtain $k=\min(\{0,\ldots,N-1\}\setminus\mathrm{Ones}(i))$ and $l=\min\mathrm{Ones}(j)$. We claim that the two points $p_{v,v^{\prime}}$ and $p_{v^{\prime},v^{\prime}}$ have the properties formulated in the formula $\mathit{compstep}_{\mathrm{left}}(r,\theta)$. Indeed, we observe $y\stackrel{{\scriptstyle L}}{{\to}}p_{v,v^{\prime}}$ and $p_{v,v^{\prime}}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{v^{\prime},v^{\prime}}$ as well as $p_{v,v^{\prime}}\models B$. The facts

[TABLE]

imply

[TABLE]

We obtain

[TABLE]

and with

[TABLE]

we obtain as well

[TABLE]

Finally, our observations about the values of the shared variable vectors $\underline{\alpha}^{\mathrm{state}}$, $\underline{\alpha}^{\mathrm{written}}$, $\underline{\alpha}^{\mathrm{read}}$ and about the vector $\underline{X}^{\mathrm{read}}$ imply that also

[TABLE]

(remember that $((q,\eta),(r,\theta,\mathit{left}))\in\delta$ is the element of the transition relation $\delta$ that leads from the node $v$ to the node $v^{\prime}$). This ends the treatment of the conjunctions over the set $(q,\eta)\in Q_{\exists}\times\Gamma$ in the formula $\mathit{computation}$. Let us now consider a pair $(q,\eta)\in Q_{\forall}\times\Gamma$. Let us assume that $y\in W$ is a point such that $y\models(\alpha^{\mathrm{state}}_{q}\wedge\alpha^{\mathrm{read}}_{\eta})$. We have to show that for all elements $(r,\theta,\mathit{left})\in\delta(q,\eta)$ we have $y\models\mathit{compstep}_{\mathrm{left}}(r,\theta)$ and for all elements $(r,\theta,\mathit{right})\in\delta(q,\eta)$ we have $y\models\mathit{compstep}_{\mathrm{right}}(r,\theta)$. Let us consider an arbitrary element $(r,\theta,\mathit{left})\in\delta(q,\eta)$ (the case of an element $(r,\theta,\mathit{right})\in\delta(q,\eta)$ is treated analogously). As in the cloud $\mathit{Cloud}_{\top}$ the truth value of any shared variable is false, the assumption $y\models(\alpha^{\mathrm{state}}_{q}\wedge\alpha^{\mathrm{read}}_{\eta})$ implies that there exists some $v\in V$ with $y\in\mathit{Cloud}_{v}$. Furthermore, $q=\mathit{state}(v)$ and $\eta=\mathit{read}(v)$. As $q\in Q_{\forall}$ and $T$ is an accepting tree, in $T$ there is a successor $v^{\prime}$ of $v$ such that the element $((q,\eta),(r,\theta,\mathit{left}))$ leads from $v$ to $v^{\prime}$. Above, we have already seen that this implies

[TABLE]

Thus, we have shown $y\models\mathit{computation}$ for all $y\in W$. This ends the proof of the claim $p_{\mathit{root},\mathit{root}}\models f_{\mathrm{SSL}}(w)$.

4.4 Existence of an Accepting Tree

We come to the other direction. Let $w\in\Sigma^{*}$. We wish to show that if $f_{\mathrm{SSL}}(w)$ is $\mathrm{SSL}$-satisfiable then $w\in L$. We will show that any cross axiom model of $f_{\mathrm{SSL}}(w)$ essentially contains an accepting tree of the Alternating Turing Machine $M$ on input $w$. Of course, this implies $w\in L$.

Let us sketch the main idea. We will consider a cross axiom model of $f_{\mathrm{SSL}}(w)$. And we will consider partial trees of $M$ on input $w$ as considered in Subsection 3.3, for any $w\in\Sigma^{*}$. First, we will show that a certain very simple partial tree of $M$ on input $w$ “can be mapped to” the model (later we will give a precise meaning to “can be mapped to”). Then we will show that any partial tree of $M$ on input $w$ that can be mapped to the model and that is not an accepting tree of $M$ on input $w$ can be properly extended to a strictly larger partial tree of $M$ on input $w$ that can be mapped to the model as well. If there would not exist an accepting tree of $M$ on input $w$ then we would obtain an infinite strictly increasing sequence of partial trees of $M$ on input $w$. But we show that this cannot happen by giving a finite upper bound on the size of partial trees of $M$ on input $w$.

Let $w\in\Sigma^{*}$ be a string such that the formula $f_{\mathrm{SSL}}(w)$ is $\mathrm{SSL}$-satisfiable. We set $n:=|w|$. Let $(W,\stackrel{{\scriptstyle\Diamond}}{{\to}},\stackrel{{\scriptstyle L}}{{\to}},\sigma)$ be a cross axiom model and $r_{0}\in W$ a point such that $r_{0}\models f_{\mathrm{SSL}}(w)$. The quintuple

[TABLE]

will be important in the following. Points in $W$ that cannot be reached from $r_{0}$ by finitely many $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ and $\stackrel{{\scriptstyle L}}{{\to}}$-steps (in any order) can be deleted from $W$ with no harm: the resulting smaller quintuple will still be a model of $f_{\mathrm{SSL}}(w)$. Hence, we will assume without loss of generality that every point $x\in W$ can be reached from $r_{0}$ by finitely many $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ and $\stackrel{{\scriptstyle L}}{{\to}}$-steps (in any order). Note that now the cross property implies that for any $x\in W$ there exists some $x^{\prime}\in W$ with $r_{0}\stackrel{{\scriptstyle L}}{{\to}}x^{\prime}$ and $x^{\prime}\stackrel{{\scriptstyle\Diamond}}{{\to}}x$. Hence, if $\varphi$ is a formula with $r_{0}\models K\Box\varphi$ then, for all $x\in W$, we have $x\models\varphi$. For every $x\in W$, let $\mathit{Cloud}_{x}$ be the $\stackrel{{\scriptstyle L}}{{\to}}$-equivalence class of $x$. Remember that for every $\stackrel{{\scriptstyle L}}{{\to}}$-equivalence class and every shared variable $\alpha^{\mathit{string}}_{i}$ for $\mathit{string}\in\{\mathrm{time},\mathrm{pos},\mathrm{state},\mathrm{written},\mathrm{read}\}$ and a natural number $i$, the truth value of this shared variable is the same in all elements of the $\stackrel{{\scriptstyle L}}{{\to}}$-equivalence class.

Partial trees of $M$ on input $w$ as introduced in Subsection 3.3 will play an important role in the following. We will write a partial tree of $M$ on input $w$ similarly as in Subsection 3.3 as a triple $T=(V,E,c)$, but with the difference that we will describe configurations as at the beginning of this section: the labeling function $c$ will be a function of the form $c:V\to Q\times\{0,\ldots,2^{N+1}-2\}\times\Gamma^{2^{N+1}-1}$. If $T=(V,E,c)$ is a partial tree of $M$ on input $w$ with root $\mathit{root}$ then a function $\pi:V\to W$ is called a morphism from $T$ to $\mathit{Model}$ if it satisfies the following four conditions:

$\pi(\mathit{root})=r_{0}$, 2. 2.

$(\forall v,v^{\prime}\in V)\,(\text{ if }vEv^{\prime}\text{ then }\mathit{Cloud}_{\pi(v)}\stackrel{{\scriptstyle\Diamond}}{{\to}}^{\stackrel{{\scriptstyle L}}{{\to}}}\mathit{Cloud}_{\pi(v^{\prime})})$, 3. 3.

$(\forall v\in V\setminus\{\mathit{root}\})\,\pi(v)\models\alpha^{\mathrm{written}}_{\mathit{written}(v)}$, 4. 4.

(\forall v\in V)\,\pi(v)\models\begin{array}[t]{l}\bigl{(}B\wedge(\underline{\alpha}^{\mathrm{time}}=\mathrm{bin}_{N}(\mathit{time}(v)))\\ \wedge(\underline{\alpha}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(\mathit{pos}(v)))\wedge\alpha^{\mathrm{state}}_{\mathit{state}(v)}\wedge\alpha^{\mathrm{read}}_{\mathit{read}(v)}\bigr{)}.\end{array}

We say that $T$ can be mapped to $\mathit{Model}$ if there exists a morphism from $T$ to $\mathit{Model}$. Below we shall prove the following lemma.

Lemma 4.2**.**

If a partial tree $T=(V,E,c)$ of $M$ on input $w$ can be mapped to $\mathit{Model}$ and is not an accepting tree of $M$ on input $w$ then there exists a partial tree $T=(\widetilde{V},\widetilde{E},\widetilde{c})$ of $M$ on input $w$ that can be mapped to $\mathit{Model}$ and that satisfies $V\subsetneq\widetilde{V}$.

Before we prove this lemma, we deduce the desired assertion from it. Let

[TABLE]

Then, due to Condition III in the definition of a “partial tree of $M$ on input $w$”, any node in any partial tree of $M$ on input $w$ has at most $D$ successors. As any computation of $M$ on $w$ stops after at most $2^{N}-1$ steps, any partial tree of $M$ on input $w$ has at most

[TABLE]

nodes. We claim that the rooted and labeled tree

[TABLE]

is a partial tree of $M$ on input $w$ and can be mapped to $\mathit{Model}$. Indeed, Condition I in the definition of a “partial tree of $M$ on input $w$” is satisfied because the node $\mathit{root}$ is labeled with the initial configuration of $M$ on input $w$. Conditions II, III, and IV are satisfied because $T_{0}$ does not have any inner nodes. Condition $V^{\prime}$ is satisfied because $q_{0}\neq q_{\mathrm{reject}}$, and this follows from $r_{0}\models\alpha^{\mathrm{state}}_{q_{0}}$ (this is a part of $r_{0}\models\mathit{start}$) and $r_{0}\models\neg\alpha^{\mathrm{state}}_{q_{\mathrm{reject}}}$ (this follows from $r_{0}\models K\Box\mathit{no\_reject}$). Thus, $T_{0}$ is indeed a partial tree of $M$ on input $w$. Now we show that $T_{0}$ can be mapped $\mathit{Model}$. Of course, we define $\pi:\{\mathit{root}\}\to W$ by $\pi(\mathit{root}):=r_{0}$. We claim that $\pi$ is a morphism from $T$ to $\mathit{Model}$. We check the four conditions one by one.

The condition $\pi(\mathit{root})=r_{0}$ is true by definition. 2. 2.

The second condition is satisfied trivially because the tree $T_{0}$ does not have any edges. 3. 3.

The third condition in the definition of a “morphism from $T$ to $\mathit{Model}$” is satisfied trivially because $T_{0}$ has only one node, its root. 4. 4.

On the one hand, we have $\mathit{time}(\mathit{root})=0$, $\mathit{pos}(\mathit{root})=2^{N}-1$,

$\mathit{state}(\mathit{root})=q_{0}$, and $\mathit{read}(\mathit{root})=\#$.

On the other hand, the condition $r_{0}\models\mathit{start}$ implies

[TABLE]

Thus, we have shown that $T_{0}$ is a partial tree of $M$ on input $w$ and that $T_{0}$ can be mapped to $\mathit{Model}$.

If there would not exist an accepting tree of $M$ on input $w$ then, starting with $T_{0}$ and using Lemma 4.2 we could construct an infinite sequence of partial trees $T_{0},T_{1},T_{2},\ldots$ of $M$ on input $w$ that can be mapped to $\mathit{Model}$ such that the number of nodes in these trees is strictly increasing. But we have seen that any partial tree of $M$ on input $w$ can have at most $\widetilde{D}$ nodes. Thus, there exists an accepting tree of $M$ on input $w$. We have shown $w\in L$.

In order to complete the proof of Theorem 4.1 it remains to prove Lemma 4.2.

Proof of Lemma 4.2.

Let $T=(V,E,c)$ be a partial tree of $M$ on input $w$ that is not an accepting tree of $M$ on input $w$ and that can be mapped to $\mathit{Model}$. Let $\pi:V\to W$ be a morphism from $T$ to $\mathit{Model}$. Then $T$ has a leaf $\widehat{v}$ such that the state $q:=\mathit{state}(\widehat{v})$ is either an element of $Q_{\exists}$ or of $Q_{\forall}$. First we treat the case that it is an element of $Q_{\exists}$, then the case that it is an element of $Q_{\forall}$.

So, let us assume that $q\in Q_{\exists}$. We define $\eta:=\mathit{read}(\widehat{v})$. Then, because $\pi$ is a morphism from $T$ to $\mathit{Model}$, we have

[TABLE]

hence, due to $\pi(\widehat{v})\models\mathit{computation}$,

[TABLE]

Let us assume that there is an element $(r,\theta,\mathit{left})\in\delta(q,\eta)$ such that $\pi(\widehat{v})\models\mathit{compstep}_{\mathrm{left}}(r,\theta)$ (the other case, the case when there is an element $(r,\theta,\mathit{right})\in\delta(q,\eta)$ such that $\pi(\widehat{v})\models\mathit{compstep}_{\mathrm{right}}(r,\theta)$, is treated analogously). We claim that we can define the new tree $\widetilde{T}=(\widetilde{V},\widetilde{E},\widetilde{c})$ as follows:

• •

$\widetilde{V}:=V\cup\{\widetilde{v}\}$ where $\widetilde{v}$ is a new element (not in $V$),

• •

$\widetilde{E}:=E\cup\{(\widehat{v},\widetilde{v})\}$,

• •

\widetilde{c}(x):=\begin{cases}c(x)&\text{for all }x\in V,\\ c^{\prime}&\text{for }x=\widetilde{v},\text{ where c^{\prime}$is the configuration that is reached from$c(\widehat{v})}\\ &\text{in the computation step given by }((q,\eta),(r,\theta,\mathit{left}))\in\delta.\end{cases}

Before we show that $\widetilde{T}$ is a partial tree of $M$ on input $w$, we define a function $\widetilde{\pi}:\widetilde{V}\to W$ that we will show to be a morphism from $\widetilde{T}$ to $\mathit{Model}$.

As $\widehat{v}$ is an element of a partial tree of $M$ on input $w$ with $\mathit{state}(\widehat{v})\in Q_{\exists}$, at least one more computation step can be done. As any computation of $M$ on input $w$ stops after at most $2^{N}-1$ steps, we observe that the number $i:=\mathit{time}(\widehat{v})$ satisfies $0\leq i<2^{N}-1$. Then $\{0,\ldots,N-1\}\setminus\mathrm{Ones}(i)\neq\emptyset$. We set $k:=\min(\{0,\ldots,N-1\}\setminus\mathrm{Ones}(i))$. The assumption that $\pi$ is a morphism from $T$ to $\mathit{Model}$ implies $\pi(\widehat{v})\models(\underline{\alpha}^{\mathrm{time}}=\mathrm{bin}_{N}(i))$. We conclude $\pi(\widehat{v})\models\mathrm{rightmost\_zero}(\underline{\alpha}^{\mathrm{time}},k)$. As during each computation step, the tape head can move at most one step to the left or to the right and as the computation started in position $2^{N}-1$ the number $j:=\mathit{pos}(\widehat{v})$ satisfies $0<j\leq 2^{N+1}-3$. Then $\mathrm{Ones}(j)\neq\emptyset$. We set $l:=\min\mathrm{Ones}(j)$. The assumption that $\pi$ is a morphism from $T$ to $\mathit{Model}$ implies $\pi(\widehat{v})\models(\underline{\alpha}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(j))$. We conclude $\pi(\widehat{v})\models\mathrm{rightmost\_one}(\underline{\alpha}^{\mathrm{pos}},l)$. Furthermore, as $\pi$ is a morphism from $T$ to $\mathit{Model}$ we have $\pi(\widehat{v})\models B$. Summarizing this, we have

[TABLE]

Due to $\pi(\widehat{v})\models\mathit{compstep}_{\mathrm{left}}(r,\theta)$ there exist an element $x\in\mathit{Cloud}_{\pi(\widehat{v})}$ and an element $y\in W$ such that $x\stackrel{{\scriptstyle\Diamond}}{{\to}}y$ as well as

[TABLE]

and

[TABLE]

We claim that we can define the desired function $\widetilde{\pi}:\widetilde{V}\to W$ by

[TABLE]

We have to show that $\widetilde{T}$ is a partial tree of $M$ on input $w$ and that $\widetilde{\pi}$ is a morphism from $\widetilde{T}$ to $\mathit{Model}$. Condition I in the definition of a “partial tree of $M$ on input $w$” is satisfied because $\widetilde{T}$ has the same root as $T$, and the label of the root does not change. A node in $\widetilde{T}$ is an internal node of $\widetilde{T}$ if, and only if, it is either an internal node of $T$ or equal to $\widehat{v}$. For internal nodes of $T$ Conditions II, III, and IV are satisfied by assumption (and due to the fact that the labels of nodes in $V$ do not change). The new internal node $\widehat{v}$ satisfies Condition II by our definition of $\widetilde{c}(\widetilde{v})$. Condition III is satisfied for $\widehat{v}$ because $\widehat{v}$ has exactly one successor. And Condition IV does not apply to $\widehat{v}$ because $\widehat{v}\in Q_{\exists}$. A node in $\widetilde{T}$ is a leaf if, and only if, it is either equal to $\widetilde{v}$ or a leaf in $T$ different from $\widehat{v}$. For the leaves in $T$ different from $\widehat{v}$ Condition $\mathrm{V}^{\prime}$ is satisfied by assumption (and due to the fact that the labels of nodes in $V$ do not change). For the new leaf $\widetilde{v}$ in $\widetilde{T}$ Condition $\mathrm{V}^{\prime}$ says $\mathit{state}(\widetilde{v})\neq q_{\mathrm{reject}}$. This is true because on the one hand $\mathit{state}(\widetilde{v})=r$ and on the other hand $y\models\alpha^{\mathrm{state}}_{r}$ and $y\models\neg\alpha^{\mathrm{state}}_{q_{\mathrm{reject}}}$ (this follows from $r\models K\Box\mathit{no\_reject}$). We have shown that $\widetilde{T}$ is a partial tree of $M$ on input $w$.

Now we show that $\widetilde{\pi}$ is a morphism from $\widetilde{T}$ to $\mathit{Model}$. The first condition in the definition of a “morphism from $\widetilde{T}$ to $\mathit{Model}$” is satisfied because $\widetilde{\pi}(\mathit{root})=\pi(\mathit{root})=r_{0}$. Let us look at the second condition and let us assume that $v,v^{\prime}\in\widetilde{V}$ satisfy $v\widetilde{E}v^{\prime}$. We distinguish between two different cases for $v$ and $v^{\prime}$.

Case: $v^{\prime}\in V$. Then our assumption $v\widetilde{E}v^{\prime}$ implies $v\in V$ and $vEv^{\prime}$. In this case the facts $\widetilde{\pi}(v)=\pi(v)$ and $\widetilde{\pi}(v^{\prime})=\pi(v^{\prime})$ as well as the assumption that $\pi:V\to W$ is a morphism from $T$ to $\mathit{Model}$ imply the desired assertion:

[TABLE] 2. 2.

Case: $v^{\prime}=\widetilde{v}$. Then our assumption $v\widetilde{E}v^{\prime}$ implies $v=\widehat{v}$. On the one hand, we have $x\in\mathit{Cloud}_{\pi(\widehat{v})}=\mathit{Cloud}_{\widetilde{\pi}(\widehat{v})}$, on the other hand $y=\widetilde{\pi}(\widetilde{v})$, hence, $y\in\mathit{Cloud}_{\widetilde{\pi}(\widetilde{v})}$. With $x\stackrel{{\scriptstyle\Diamond}}{{\to}}y$ we obtain the desired assertion $\mathit{Cloud}_{\widetilde{\pi}(\widehat{v})}\stackrel{{\scriptstyle\Diamond}}{{\to}}^{\stackrel{{\scriptstyle L}}{{\to}}}\mathit{Cloud}_{\widetilde{\pi}(\widetilde{v})}$.

The third condition in the definition of a “morphism from $\widetilde{T}$ to $\mathit{Model}$” is satisfied for $v\in V\setminus\{\mathit{root}\}$ by assumption (and by $\widetilde{\pi}(v)=\pi(v)$ and $\widetilde{c}(v)=c(v)$). It is satisfied for $\widetilde{v}$ because $\mathit{written}(\widetilde{v})=\theta$, because $\widetilde{\pi}(\widetilde{v})=y$, and because $y\models\alpha^{\mathrm{written}}_{\theta}$. We come to the fourth condition. It is satisfied for $v\in V\setminus\{\mathit{root}\}$ by assumption (and due to $\widetilde{\pi}(v)=\pi(v)$ and $\widetilde{c}(v)=c(v)$). We still need to show that it is satisfied for $\widetilde{v}$. Remember $\widetilde{\pi}(\widetilde{v})=y$. We need to show

[TABLE]

This assertion consists really of five assertions. We treat them one by one.

• •

The condition $y\models B$ is satisfied because $x\models B$ and $x\stackrel{{\scriptstyle\Diamond}}{{\to}}y$ and because $B$ is persistent.

• •

In the trees $T$ and $\widetilde{T}$ we have $\mathit{time}(\widehat{v})=i$, and in the tree $\widetilde{T}$ we have $\mathit{time}(\widetilde{v})=i+1$. We wish to show $y\models(\underline{\alpha}^{\mathrm{time}}=\mathrm{bin}_{N}(i+1))$. We have already seen $\pi(\widehat{v})\models(\underline{\alpha}^{\mathrm{time}}=\mathrm{bin}_{N}(i))$ and $\pi(\widehat{v})\models\mathrm{rightmost\_zero}(\underline{\alpha}^{\mathrm{time}},k)$. As $x\in\mathit{Cloud}_{\pi(\widehat{v})}$, we obtain

[TABLE]

The conditions $x\stackrel{{\scriptstyle\Diamond}}{{\to}}y$ as well as

[TABLE]

imply $y\models(\underline{\alpha}^{\mathrm{time}}=\mathrm{bin}_{N}(i+1))$.

• •

In the trees $T$ and $\widetilde{T}$ we have $\mathit{pos}(\widehat{v})=j$, and in the tree $\widetilde{T}$ we have $\mathit{pos}(\widetilde{v})=j-1$. We wish to show $y\models(\underline{\alpha}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(j-1))$. We have already seen $\pi(\widehat{v})\models(\underline{\alpha}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(j))$ and $\pi(\widehat{v})\models\mathrm{rightmost\_one}(\underline{\alpha}^{\mathrm{pos}},l)$. As $x\in\mathit{Cloud}_{\pi(\widehat{v})}$, we obtain

[TABLE]

The conditions $x\stackrel{{\scriptstyle\Diamond}}{{\to}}y$ as well as

[TABLE]

imply $y\models(\underline{\alpha}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(j-1))$.

• •

We have $\mathit{state}(\widetilde{v})=r$. And we have $y\models\alpha^{\mathit{state}}_{r}$.

• •

Let $\gamma:=\mathit{read}(\widetilde{v})$ in $\widetilde{T}$. We wish to show $y\models\alpha^{\mathrm{read}}_{\gamma}$. As we know $y\models(\underline{\alpha}^{\mathrm{read}}=\underline{X}^{\mathrm{read}})$ it is sufficient to show $y\models X^{\mathrm{read}}_{\gamma}$. We have already seen $y\models(\underline{\alpha}^{\mathrm{time}}=\mathrm{bin}_{N}(i+1))$ and $y\models(\underline{\alpha}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(j-1))$. As we know $y\models(\underline{\alpha}^{\mathrm{time}}=\underline{X}^{\mathrm{time}})\wedge(\underline{\alpha}^{\mathrm{pos}}=\underline{X}^{\mathrm{pos}})$ we conclude $y\models((\underline{X}^{\mathrm{time}}=\mathrm{bin}_{N}(i+1))\wedge(\underline{X}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(j-1)))$. We have seen $y\models B$ as well. Furthermore, we have $y\models\mathit{time\_after\_previous\_visit}$. The first line in the formula $\mathit{time\_after\_previous\_visit}$ implies $y\models(\underline{X}^{\text{time-apv}}\leq\underline{X}^{\mathrm{time}})$, hence, $y\models(\underline{X}^{\text{time-apv}}\leq\mathrm{bin}_{N}(i+1))$. Let $v_{m}\in V$ for $m=0,\ldots,i+1$ be the uniquely determined node on the path from $\mathit{root}$ to $\widetilde{v}$ with $\mathit{time}(v_{m})=m$ (hence $v_{0}=\mathit{root}$, $v_{i}=\widehat{v}$, and $v_{i+1}=\widetilde{v}$). Then

[TABLE]

By the second condition in the definition of a “morphism from $\widetilde{T}$ to $\mathit{Model}$”

[TABLE]

By repeated application of the cross property and by starting with $z_{i+1}:=y$ we conclude that for $m=i+1,i,\ldots,1,0$ there exists some $z_{m}\in\mathit{Cloud}_{\widetilde{\pi}(v_{m})}$ with $z_{m}\stackrel{{\scriptstyle\Diamond}}{{\to}}y$. Let us consider $m\in\{0,1,\ldots,i+1\}$. As $y\models B$ we also have $z_{m}\models B$ (remember that variables are persistent in $\mathrm{SSL}$). Due to $\widetilde{\pi}(v_{m})\models((\underline{\alpha}^{\mathrm{time}}=\mathrm{bin}_{N}(m))\wedge(\underline{\alpha}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(\mathit{pos}(v_{m}))))$ we obtain $z_{m}\models((\underline{\alpha}^{\mathrm{time}}=\mathrm{bin}_{N}(m))\wedge(\underline{\alpha}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(\mathit{pos}(v_{m}))))$ as well. Due to $y\models((\underline{X}^{\mathrm{time}}=\mathrm{bin}_{N}(i+1))\wedge(\underline{X}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(j-1)))$ and the persistence of variables we obtain $z_{m}\models((\underline{X}^{\mathrm{time}}=\mathrm{bin}_{N}(i+1))\wedge(\underline{X}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(j-1)))$ as well. Furthermore, we have $z_{m}\models\mathit{time\_after\_previous\_visit}$. We distinguish between the two cases whether the cell $j-1$ has been visited on the path from $\mathit{root}$ to $\widehat{v}$ or not.

Let us first consider the case when the cell $j-1$ has not been visited on the path from $\mathit{root}$ to $\widehat{v}$. Then, on the one hand, the symbol $\gamma=\mathit{read}(\widetilde{v})$ is still the initial symbol in the cell $j-1$. On the other hand, for all $m\in\{0,\ldots,i\}$ we have $\mathit{pos}(v_{m})\neq j-1$ and

[TABLE]

Together with $z_{m}\models((\underline{X}^{\mathrm{time}}=\mathrm{bin}_{N}(i+1))\wedge(\underline{X}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(j-1)))$ and $z_{m}\models((\underline{\alpha}^{\mathrm{time}}=\mathrm{bin}_{N}(m))\wedge(\underline{\alpha}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(\mathit{pos}(v_{m}))))$ we conclude that $z_{m}\models(\underline{X}^{\text{time-apv}}\neq\mathrm{bin}_{N}(m+1))$ for $m\in\{0,\ldots,i\}$. The persistence of $\underline{X}^{\text{time-apv}}$ implies that $y\models(\underline{X}^{\text{time-apv}}\neq\mathrm{bin}_{N}(m+1))$ for $m\in\{0,\ldots,i\}$. Together with $y\models(\underline{X}^{\text{time-apv}}\leq\underline{X}^{\mathrm{time}})$ we conclude that the binary value of $\underline{X}^{\text{time-apv}}$ in $y$ must be [math]. Now the fact $y\models\mathit{get\_the\_right\_symbol}$ implies $y\models X^{\mathrm{read}}_{\gamma}$.

Let us consider the second case, the case when the cell $j-1$ has been visited on the path from $\mathit{root}$ to $\widehat{v}$. Let $v_{m^{\prime}}$ be the last node on this path with $\mathit{pos}(v_{m^{\prime}})=j-1$. Then $0\leq m^{\prime}\leq i$. On the one hand, then the symbol $\gamma=\mathit{read}(\widetilde{v})$ is the symbol that was written into the cell $j-1$ in the computation step from node $v_{m^{\prime}}$ to node $v_{m^{\prime}+1}$, and by the third condition in the definition of a “morphism from $\widetilde{T}$ to $\mathit{Model}$” we have $\widetilde{\pi}(v_{m^{\prime}+1})\models\alpha^{\mathrm{written}}_{\gamma}$, hence, $z_{m^{\prime}+1}\models\alpha^{\mathrm{written}}_{\gamma}$. On the other hand, from $y\models\mathit{time\_after\_previous\_visit}$ we get $y\models(\underline{X}^{\text{time-apv}}\leq\underline{X}^{\mathrm{time}})$, hence, $y\models(\underline{X}^{\text{time-apv}}\leq\mathrm{bin}_{N}(i+1))$. From $z_{m^{\prime}}\models\mathit{time\_after\_previous\_visit}$ we get

[TABLE]

Together with $z_{m^{\prime}}\models(\underline{\alpha}^{\mathrm{time}}=\mathrm{bin}_{N}(m^{\prime}))$ we obtain $z_{m^{\prime}}\models(\mathrm{bin}_{N}(m^{\prime})<\underline{X}^{\text{time-apv}})$. And similarly as in the first case, from

[TABLE]

for $m=m^{\prime}+1,\ldots,i$ we obtain

[TABLE]

All this implies $y\models(\underline{X}^{\text{time-apv}}=\mathrm{bin}_{N}(1+m^{\prime}))$ and $z_{m^{\prime}+1}\models(\underline{X}^{\text{time-apv}}=\mathrm{bin}_{N}(1+m^{\prime}))$. Then $z_{m^{\prime}+1}\models\mathit{get\_the\_right\_symbol}$ implies $z_{m^{\prime}+1}\models(\underline{X}^{\mathrm{read}}=\underline{\alpha}^{\mathrm{written}})$. With $z_{m^{\prime}+1}\models\alpha^{\mathrm{written}}_{\gamma}$ we conclude $z_{m^{\prime}+1}\models X^{\mathrm{read}}_{\gamma}$, hence, $y\models X^{\mathrm{read}}_{\gamma}$. That was to be shown.

Thus, $\widetilde{T}$ is not only a partial tree of $M$ on input $w$ but can also be mapped to $\mathit{Model}$. This ends the treatment of the case $q\in Q_{\exists}$.

Now we consider the other case, the case $q\in Q_{\forall}$. We define $\eta:=\mathit{read}(\widehat{v})$. Let

[TABLE]

be the elements of $\delta(q,\eta)$ where $d\geq 1$ and $\mathit{dir}_{m}\in\{\mathit{left},\mathit{right}\}$, for $m=1,\ldots,d$. We claim that we can define the new tree $\widetilde{T}=(\widetilde{V},\widetilde{E},\widetilde{c})$ as follows:

• •

$\widetilde{V}:=V\cup\{\widetilde{v}_{1},\ldots,\widetilde{v}_{d}\}$ where $\widetilde{v}_{1},\ldots,\widetilde{v}_{d}$ are new (not in $V$) pairwise different elements,

• •

$\widetilde{E}:=E\cup\{(\widehat{v},\widetilde{v}_{1}),\ldots,(\widehat{v},\widetilde{v}_{d})\}$,

• •

\widetilde{c}(x):=\begin{cases}c(x)&\text{for all }x\in V,\\ c^{\prime}_{m}&\text{for }x=\widetilde{v}_{m},\text{where c^{\prime}_{m} is the configuration that is reached from }\\ &\text{c(\widehat{v}) in the computation step given by }((q,\eta),(r_{m},\theta_{m},\mathit{dir}_{m}))\in\delta.\end{cases}

Before we show that $\widetilde{T}$ is a partial tree of $M$ on input $w$, we define a function $\widetilde{\pi}:\widetilde{V}\to W$ that we will show to be a morphism from $\widetilde{T}$ to $\mathit{Model}$. Since $\pi$ is a morphism from $T$ to $\mathit{Model}$), we have

[TABLE]

hence, due to $\pi(\widehat{v})\models\mathit{computation}$,

[TABLE]

As in the case $q\in Q_{\exists}$ one shows that the numbers $i:=\mathit{time}(\widehat{v})$ and $j:=\mathit{pos}(\widehat{v})$ satisfy $0\leq i<2^{N}-1$ and $0<j\leq 2^{N+1}-3$, and one defines

[TABLE]

As in the case $q\in Q_{\exists}$ one obtains

[TABLE]

Let us now consider some $m\in\{1\ldots,d\}$. If $\mathit{dir}_{m}=\mathit{left}$ then, due to $\pi(\widehat{v})\models\mathit{compstep}_{\mathrm{left}}(r,\theta)$, there exist an element $x_{m}\in\mathit{Cloud}_{\pi(\widehat{v})}$ and an element $y_{m}\in W$ such that $x_{m}\stackrel{{\scriptstyle\Diamond}}{{\to}}y_{m}$ as well as

[TABLE]

and

[TABLE]

Similarly, if $\mathit{dir}_{m}=\mathit{right}$ then, due to $\pi(\widehat{v})\models\mathit{compstep}_{\mathrm{right}}(r,\theta)$, there exist an element $x_{m}\in\mathit{Cloud}_{\pi(\widehat{v})}$ and an element $y_{m}\in W$ such that $x_{m}\stackrel{{\scriptstyle\Diamond}}{{\to}}y_{m}$ as well as

[TABLE]

and

[TABLE]

We claim that we can define the desired function $\widetilde{\pi}:\widetilde{V}\to W$ by

[TABLE]

Similarly as in the case $q\in Q_{\exists}$ one shows that $\widetilde{T}$ is a partial tree of $M$ on input $w$. Note that also Condition IV is satisfied for $\widehat{v}$. Finally, similarly as in the case $q\in Q_{\exists}$ one shows that $\widetilde{\pi}$ is a morphism from $\widetilde{T}$ to $\mathit{Model}$. This ends the treatment of the case $q\in Q_{\forall}$. We have proved Lemma 4.2. ∎

5 Reduction of $\mathrm{SSL}$ to $\mathrm{S4\times S5}$

In this section we prove the $\mathrm{EXPSPACE}$-hardness of $\mathrm{S4\times S5}$ by showing the following result. Remember that according to Theorem 4.1 the satisfiability problem of $\mathrm{SSL}$ is $\mathrm{EXPSPACE}$-hard.

Theorem 5.1**.**

The satisfiability problem of the bimodal logic $\mathrm{SSL}$ can be reduced in logarithmic space to the satisfiability problem of the bimodal logic $\mathrm{S4\times S5}$.

To prove this theorem we proceed in three steps:

We start with the definition of the reduction function. 2. 2.

We prove its correctness. 3. 3.

We show that the reduction function can be computed using not more than logarithmic space.

5.1 The Reduction Function

We show that the satisfiability problem of $\mathrm{SSL}$ can be reduced to the satisfiability problem of $\mathrm{S4\times S5}$. To this end we define a translation $\widehat{T}$ of bimodal formulas in the language $\mathcal{L}$ to bimodal formulas in $\mathcal{L}$ such that for all $\varphi\in\mathcal{L}$

[TABLE]

For the reduction we face two main problems.

The first problem is that in cross axiom models literals are persistent. To handle this we make sure that the translation $\widehat{T}(\varphi)$ contains a subformula postulating the persistence of literals. 2. 2.

The second problem is that in general cross axiom models do not satisfy right commutativity. To handle this we add to each cloud in a cross-axiom model a special “new point” serving as successor point for all points in a predecessor cloud that fail to have in the original model a successor point in this cloud. In order to distinguish the new points from the original ones we use a special propositional variable main which is false exactly at the new points.

We define the desired function $\widehat{T}:\mathcal{L}\to\mathcal{L}$ in four steps:

Definition 5.2** (Translation $\widehat{T}$).**

For every $\varphi\in\mathcal{L}$ let $\mathrm{main}\in AT$ by the alphabetically first propositional variable that is not a subformula of $\varphi$. 2. 2.

Recursively, we define a function $T:\mathcal{L}\to\mathcal{L}$ as follows:

[TABLE]

for all $A\in AT$ and for all $\psi,\psi_{1},\psi_{2}\in\mathcal{L}$. (Note that $K\neg(\mathrm{main}\wedge\neg T(\psi))$ is equivalent to $K(\mathrm{main}\to T(\psi))$ and that $\Box\neg(\mathrm{main}\wedge\neg T(\psi))$ is equivalent to $\Box(\mathrm{main}\to T(\psi))$.) 3. 3.

For $\varphi\in\mathcal{L}$ we define

[TABLE] 4. 4.

For $\varphi\in\mathcal{L}$ we define a function $\widehat{T}:\mathcal{L}\to\mathcal{L}$ by

[TABLE]

We claim that the function $\widehat{T}$ is indeed a reduction function from the satisfiability problem of $\mathrm{SSL}$ to the satisfiability problem of $\mathrm{S4\times S5}$.

Proposition 5.3**.**

The function $\widehat{T}:\mathcal{L}\to\mathcal{L}$ satisfies, for all $\varphi\in\mathcal{L}$,

[TABLE]

The next section is dedicated to the proof of Proposition 5.3. We treat both directions of the claimed equivalence separately.

5.2 Correctness

Lemma 5.4**.**

Let $\varphi\in\mathcal{L}$. Then

[TABLE]

Proof.

Let $\varphi\in\mathcal{L}$ be $\mathrm{SSL}$–satisfiable. Then there are a cross axiom model $M=(W,\stackrel{{\scriptstyle\Diamond}}{{\to}},\stackrel{{\scriptstyle L}}{{\to}},\sigma)$ and a point $w\in W$ such that $M,w\models\varphi$. Let $C_{i}$, for $i\in I$, where $I$ is a suitable index set, be the $\stackrel{{\scriptstyle L}}{{\to}}$-equivalence classes in $W$. We construct an $\mathrm{S4\times S5}$-commutator model $M^{\prime}=(W^{\prime},\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}},\stackrel{{\scriptstyle L^{\prime}}}{{\to}},\sigma^{\prime})$ for $\widehat{T}(\varphi)$ as follows. Let $newpoint_{i}$ for $i\in I$ be pairwise different “new” points that are not elements of $W$. We define

[TABLE]

We define the equivalence relation $\stackrel{{\scriptstyle L^{\prime}}}{{\to}}$ on $W^{\prime}$ by demanding that the following sets $C^{\prime}_{i}$ for $i\in I$ are the $\stackrel{{\scriptstyle L^{\prime}}}{{\to}}$-equivalence classes of $W^{\prime}$:

[TABLE]

for $i\in I$. Let $\stackrel{{\scriptstyle\Diamond}}{{\to}}^{\stackrel{{\scriptstyle L}}{{\to}}}$ be the relation on the set of clouds in $M$ induced by $\stackrel{{\scriptstyle\Diamond}}{{\to}}$; compare [8, Definition 4.1]. We define

[TABLE]

Finally we define

[TABLE]

We wish to show the following:

$M^{\prime}$ is an $\mathrm{S4\times S5}$-commutator model, 2. 2.

$M^{\prime},w\models\widehat{T}(\varphi)$.

We prove the first claim.

Clearly, $\stackrel{{\scriptstyle L^{\prime}}}{{\to}}$ is an equivalence relation.

The relations $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ and $\stackrel{{\scriptstyle\Diamond}}{{\to}}^{\stackrel{{\scriptstyle L}}{{\to}}}$ are preorders (by assumption respectively by [8, Corollary 4.4]), hence, both of them are reflexive and transitive. It is clear that this implies that the relation $\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}$ is reflexive as well. For transitivity of $\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}$, assume that $p\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}q$ and $q\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}r$. If $r\in W$ then the definition of $\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}$ implies that also $q\in W$ and $p\in W$ and $p\stackrel{{\scriptstyle\Diamond}}{{\to}}q$ as well as $q\stackrel{{\scriptstyle\Diamond}}{{\to}}r$, hence, $p\stackrel{{\scriptstyle\Diamond}}{{\to}}r$ by transitivity of $\stackrel{{\scriptstyle\Diamond}}{{\to}}$. This implies $p\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}r$. If $r\not\in W$ then we let $i,j,k\in I$ be the indices with $p\in C^{\prime}_{i}$, $q\in C^{\prime}_{j}$, and $r\in C^{\prime}_{k}$. Note that in this case $r=newpoint_{k}$. We observe that $p\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}q$ and $q\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}r$ imply $C_{i}\stackrel{{\scriptstyle\Diamond}}{{\to}}^{\stackrel{{\scriptstyle L}}{{\to}}}C_{j}$ and $C_{j}\stackrel{{\scriptstyle\Diamond}}{{\to}}^{\stackrel{{\scriptstyle L}}{{\to}}}C_{k}$. Transitivity of $\stackrel{{\scriptstyle\Diamond}}{{\to}}^{\stackrel{{\scriptstyle L}}{{\to}}}$ implies $C_{i}\stackrel{{\scriptstyle\Diamond}}{{\to}}^{\stackrel{{\scriptstyle L}}{{\to}}}C_{k}$, hence, $p\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}newpoint_{k}=r$. Thus, $\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}$ is transitive as well. We have shown that $\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}$ is a preorder.

Next, we wish to show left commutativity. Let us consider some $p,q,r\in W^{\prime}$ with $p\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}q$ and $q\stackrel{{\scriptstyle L^{\prime}}}{{\to}}r$. Let $i,j$ be the indices with $p\in C^{\prime}_{i}$ and $q,r\in C^{\prime}_{j}$. It is sufficient to show that there exists some $s\in C^{\prime}_{i}$ with $s\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}r$. The condition $p\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}q$ implies $C_{i}\stackrel{{\scriptstyle\Diamond}}{{\to}}^{\stackrel{{\scriptstyle L}}{{\to}}}C_{j}$. If $r\in W$ then the left commutativity of $M$ gives us an $s\in C_{i}$ with $s\stackrel{{\scriptstyle\Diamond}}{{\to}}r$, hence, with $s\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}r$. If $r\not\in W$ then $r=newpoint_{j}$, and $s:=p$ does the job.

In order to prove right commutativity let us consider some $p,q,r\in W^{\prime}$ with $p\stackrel{{\scriptstyle L^{\prime}}}{{\to}}q$ and $q\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}r$. Let $i,j$ be the indices with $p,q\in C^{\prime}_{i}$ and $r\in C^{\prime}_{j}$. It is sufficient to show that there exists some $s\in C^{\prime}_{j}$ with $p\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}s$. The condition $q\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}r$ implies $C_{i}\stackrel{{\scriptstyle\Diamond}}{{\to}}^{\stackrel{{\scriptstyle L}}{{\to}}}C_{j}$. Hence, we obtain $p\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}newpoint_{j}$. This proves the first claim, that $M^{\prime}$ is an $\mathrm{S4\times S5}$-commutator model.

We come to the second claim, $M^{\prime},w\models\widehat{T}(\varphi)$.

From the definition of $\sigma^{\prime}(\mathrm{main})$ we obtain

[TABLE]

Exactly at the points in $\{newpoint_{i}\mid i\in I\}$ the propositional variable $\mathrm{main}$ is false. From the fact that all $\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}$-successors of points in this set are elements of this set as well, we conclude

[TABLE]

Next, we observe that for all $v\in W$ and for all propositional variables $A\in\mathrm{sf}(\varphi)$ we have by definition of $\sigma^{\prime}$

[TABLE]

Since all literals are persistent in $M$ and $\mathrm{main}$ is true exactly at the points in $W\subseteq W^{\prime}$ we obtain

[TABLE]

Finally, we have to show $M^{\prime},w\models T(\varphi)$. By induction on the structure of $\psi$ we show the stronger assertion:

[TABLE]

for all $v\in W$ and for all $\psi\in\mathrm{sf}(\varphi)$. We distinguish the following cases:

• •

Case $\psi\in AT$. We already mentioned that for all $v\in W$ and for all $A\in AT\cap\mathrm{sf}(\varphi)$ we have $M,v\models A\iff M^{\prime},v\models A$.

• •

Case $\psi=\neg\chi$. Then the following four assertions are equivalent, the second and the third by induction hypothesis: (1) $M,v\models\psi$, (2) $M,v\not\models\chi$, (3) $M^{\prime},v\not\models T(\chi)$, (4) $M^{\prime},v\models T(\psi)$.

• •

Case $\psi=(\chi_{1}\wedge\chi_{2})$. This case is treated in the same way.

• •

Case $\psi=K\chi$. We wish to show

[TABLE]

First, let us assume $M,v\models K\chi$. Let us consider an arbitrary $v^{\prime}\in W^{\prime}$ such that $v\stackrel{{\scriptstyle L^{\prime}}}{{\to}}v^{\prime}$. It is sufficient to show that

[TABLE]

If $v^{\prime}\in W$ then we obtain $v\stackrel{{\scriptstyle L}}{{\to}}v^{\prime}$ and $M,v^{\prime}\models\chi$. By induction hypothesis we obtain $M^{\prime},v^{\prime}\models T(\chi)$, hence $M^{\prime},v^{\prime}\models(\mathrm{main}\to T(\chi))$. If $v^{\prime}\not\in W$ then $M^{\prime},v^{\prime}\not\models\mathrm{main}$, hence in this case $M^{\prime},v^{\prime}\models(\mathrm{main}\to T(\chi))$ as well.

Now, for the other direction, let us assume $M^{\prime},v\models K(\mathrm{main}\to T(\chi))$. Consider some $u\in W$ with $v\stackrel{{\scriptstyle L}}{{\to}}u$ (remember that this implies $v\stackrel{{\scriptstyle L^{\prime}}}{{\to}}u$). It is sufficient to show that

[TABLE]

But for $u\in W$ we have $M^{\prime},u\models\mathrm{main}$. The condition $M^{\prime},v\models K(\mathrm{main}\to T(\chi))$ implies $M^{\prime},u\models(\mathrm{main}\to T(\chi))$. We obtain $M^{\prime},u\models T(\chi)$. Finally, by induction hypothesis we obtain $M,u\models\chi$.

• •

Case $\psi=\Box\chi$. This case can be treated in the same way as the previous case. In fact, it is sufficient to copy the argument for the case $\psi=K\chi$ and to replace $K$ by $\Box$, $\stackrel{{\scriptstyle L}}{{\to}}$ by $\stackrel{{\scriptstyle\Diamond}}{{\to}}$, and $\stackrel{{\scriptstyle L^{\prime}}}{{\to}}$ by $\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}$. ∎

Now we turn to the other direction of Proposition 5.3.

Lemma 5.5**.**

Let $\varphi\in\mathcal{L}$. Then

[TABLE]

Proof.

Let $\widehat{T}(\varphi)$ be $\mathrm{S4\times S5}$–satisfiable. This implies that there exist an $\mathrm{S4\times S5}$–commutator model $M^{\prime}=(W^{\prime},\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}},\stackrel{{\scriptstyle L^{\prime}}}{{\to}},\sigma^{\prime})$ and a point $w\in W^{\prime}$ such that $M^{\prime},w\models\widehat{T}(\varphi)$, that is

[TABLE]

We construct a cross axiom model $M:=(W,\stackrel{{\scriptstyle\Diamond}}{{\to}},\stackrel{{\scriptstyle L}}{{\to}},\sigma)$ for $\varphi$ as follows. We construct $M$ as a rooted model, where all points are reachable from the point $w$:

[TABLE]

We define the relations $\stackrel{{\scriptstyle L}}{{\to}}$ and $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ on $W$ simply by

[TABLE]

Finally,

[TABLE]

for all $A\in AT$.

First, we observe that $M^{\prime},w\models\mathrm{main}$ and the reflexivity of $\stackrel{{\scriptstyle L^{\prime}}}{{\to}}$ and $\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}$ imply $w\in W$. We wish to show the following:

$M$ is a cross axiom model, 2. 2.

$M,w\models\varphi$.

We prove the first claim.

It is obvious that the relation $\stackrel{{\scriptstyle L}}{{\to}}$ inherits reflexivity, symmetry and transitivity from $\stackrel{{\scriptstyle L^{\prime}}}{{\to}}$ and that the relation $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ inherits reflexivity and transitivity from $\stackrel{{\scriptstyle L^{\prime}}}{{\to}}$. Thus, the relation $\stackrel{{\scriptstyle L}}{{\to}}$ is an equivalence relation, and the relation $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ is a preorder.

Next we wish to show that $M$ has the left commutativity property. So let us consider points $p,q,r\in W$ with $p\stackrel{{\scriptstyle\Diamond}}{{\to}}q$ and $q\stackrel{{\scriptstyle L}}{{\to}}r$. By definition of the relations $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ and $\stackrel{{\scriptstyle L}}{{\to}}$ we obtain that also $p\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}q$ and $q\stackrel{{\scriptstyle L^{\prime}}}{{\to}}r$. Since $M^{\prime}$ has the left commutativity property there is some point $p^{\prime}\in W^{\prime}$ with $p\stackrel{{\scriptstyle L^{\prime}}}{{\to}}p^{\prime}$ and $p^{\prime}\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}r$. The definition of $W$ and $p\in W$ imply that there exists some $w^{\prime}\in W^{\prime}$ with $w\stackrel{{\scriptstyle L^{\prime}}}{{\to}}w^{\prime}$ and $w^{\prime}\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}p$. The left commutativity of $M^{\prime}$ and $w^{\prime}\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}p$ as well as $p\stackrel{{\scriptstyle L^{\prime}}}{{\to}}p^{\prime}$ imply that there exists some $w^{\prime\prime}\in W^{\prime}$ with $w^{\prime}\stackrel{{\scriptstyle L^{\prime}}}{{\to}}w^{\prime\prime}$ and $w^{\prime\prime}\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}p^{\prime}$. So, we have $w\stackrel{{\scriptstyle L^{\prime}}}{{\to}}w^{\prime\prime}$ and $w^{\prime\prime}\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}p^{\prime}$. In addition to that, $M^{\prime},w\models K\Box(\neg\mathrm{main}\to\Box\neg\mathrm{main})$ implies $M^{\prime},w^{\prime\prime}\models\Box(\neg\mathrm{main}\to\Box\neg\mathrm{main})$, hence, $M^{\prime},p^{\prime}\models\neg\mathrm{main}\to\Box\neg\mathrm{main}$. This, together with $p^{\prime}\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}r$ and $M^{\prime},r\models\mathrm{main}$, implies $M^{\prime},p^{\prime}\models\mathrm{main}$. Hence $p^{\prime}\in W$ and $p\stackrel{{\scriptstyle L}}{{\to}}p^{\prime}$ as well as $p^{\prime}\stackrel{{\scriptstyle\Diamond}}{{\to}}r$. This shows that $M$ has the left commutativity property.

Finally, we claim that propositional variables are persistent in $M$. For all $A\in AT\setminus(\{\mathrm{main}\}\cup\mathrm{sf}(\varphi))$ we have $\sigma(A)=\emptyset$. Hence, all $A\in AT\setminus(\{\mathrm{main}\}\cup\mathrm{sf}(\varphi))$ are persistent in $M$. Furthermore, we have $\sigma(\mathrm{main})=W$. Hence, $\mathrm{main}$ is persistent in $M$ as well. Let us consider $u,v\in W$ with $u\stackrel{{\scriptstyle\Diamond}}{{\to}}v$. Due to the definition of $W$ there exists some $w^{\prime}\in W^{\prime}$ with $w\stackrel{{\scriptstyle L^{\prime}}}{{\to}}w^{\prime}$ and $w^{\prime}\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}u$. Then, $M^{\prime},w\models persistent_{main}$ implies, for all $A\in AT\cap\mathrm{sf}(\varphi)$, $M^{\prime},w^{\prime}\models\Box(\mathrm{main}\to A)\vee\Box(\mathrm{main}\to\neg A)$. Note that $M^{\prime},u\models\mathrm{main}$ and $M^{\prime},v\models\mathrm{main}$. So, $M^{\prime},u\models A$ if, and only if, $M^{\prime},v\models A$. Due to $\sigma(A)=\sigma^{\prime}(A)\cap W$ the same holds true with $M^{\prime}$ replaced by $M$. This shows that all $A\in AT\cap\mathrm{sf}(\varphi)$ are persistent in $M$. We have shown that $M$ is a cross axiom model.

We come to the second claim, $M,w\models\varphi$. Due to $M^{\prime},w\models T(\varphi)$ it is sufficient to prove for all $v\in W$ and for all $\psi\in\mathrm{sf}(\varphi)$:

[TABLE]

We show this by induction on the structure of $\psi$. We distinguish the following cases:

• •

Case $\psi=A\in AT$. In this case the claim is true due to the definition of $\sigma$.

• •

Case $\psi=\neg\chi$ or $\psi=(\chi_{1}\wedge\chi_{2})$. In both cases the claim follows directly from the induction hypothesis.

• •

Case $\psi=K\chi$. Let us first assume $M^{\prime},v\models T(K\chi)$, that is $M^{\prime},v\models K(\mathrm{main}\to T(\chi))$. We wish to show $M,v\models K\chi$. Consider an arbitrary $v^{\prime}\in W$ with $v\stackrel{{\scriptstyle L}}{{\to}}v^{\prime}$. It is sufficient to show $M,v^{\prime}\models\chi$. Note that the definition of $\stackrel{{\scriptstyle L}}{{\to}}$ implies $v\stackrel{{\scriptstyle L^{\prime}}}{{\to}}v^{\prime}$. Hence, we have $M^{\prime},v^{\prime}\models(\mathrm{main}\to T(\chi))$. Furthermore, due to $v^{\prime}\in W$ we have $M^{\prime},v^{\prime}\models\mathrm{main}$. We obtain $M^{\prime},v^{\prime}\models T(\chi)$. By induction hypothesis we obtain $M,v^{\prime}\models\chi$.

For the other direction let us assume that $M,v\models K\chi$. We wish to show $M^{\prime},v\models K(\mathrm{main}\to T(\chi))$. Consider an arbitrary $v^{\prime}\in W^{\prime}$ with $v\stackrel{{\scriptstyle L^{\prime}}}{{\to}}v^{\prime}$. It is sufficient to show $M^{\prime},v^{\prime}\models(\mathrm{main}\to T(\chi))$. If $v^{\prime}\in W$ then $v\stackrel{{\scriptstyle L^{\prime}}}{{\to}}v^{\prime}$ implies $v\stackrel{{\scriptstyle L}}{{\to}}v^{\prime}$, and $M,v\models K\chi$ implies $M,v^{\prime}\models\chi$. By induction hypothesis we obtain $M^{\prime},v^{\prime}\models T(\chi)$, hence, $M^{\prime},v^{\prime}\models(\mathrm{main}\to T(\chi))$. If $v^{\prime}\not\in W$ then we claim that $M^{\prime},v^{\prime}\not\models\mathrm{main}$, hence, $M^{\prime},v^{\prime}\models(\mathrm{main}\to T(\chi))$. Indeed, the assumption $v\in W$ implies that there exists some $w^{\prime}\in W^{\prime}$ with $w\stackrel{{\scriptstyle L^{\prime}}}{{\to}}w^{\prime}$ and $w^{\prime}\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}v$. Together with $v\stackrel{{\scriptstyle L^{\prime}}}{{\to}}v^{\prime}$ and left commutativity of $M^{\prime}$ and transitivity of $\stackrel{{\scriptstyle L^{\prime}}}{{\to}}$ we can conclude that there exists some $w^{\prime\prime}\in W^{\prime}$ with $w\stackrel{{\scriptstyle L^{\prime}}}{{\to}}w^{\prime\prime}$ and $w^{\prime\prime}\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}v^{\prime}$. Hence, $v^{\prime}$ is reachable from $w$. By definition of $W$ the assumption $v^{\prime}\not\in W$ indeed implies $M^{\prime},v^{\prime}\not\models\mathrm{main}$.

• •

Case $\psi=\Box\chi$. This case can be treated similarly as the previous case. The details are left to the reader. ∎

5.3 LOGSPACE Computability of the Reduction Function

In this subsection we show that the satisfiability problem of the logic $\mathrm{SSL}$ can be reduced in logarithmic space to the satisfiability problem of $\mathrm{S4\times S5}$. We start with the following assertion.

Lemma 5.6**.**

The language $\mathcal{L}$ of bimodal formulas is an element of $\mathrm{ALOGTIME}$.

Here, $\mathrm{ALOGTIME}$ is the set of all languages that can be decided in logarithmic time by an alternating Turing machine with “random access” to the input; compare Buss [1, Page 124], Ibarra, Jiang, and Rivakumar [9], Clote [4, Def. 2.3]. Note that Buss [1, Pages 124, 125] has shown that a certain language of Boolean formulas is in $\mathrm{ALOGTIME}$. As our syntax of formulas is slightly different from the one used by Buss we cannot directly use his result. But Lemma 5.6 can be proved by arguments similar to the arguments used by Buss. Therefore, we omit the proof of Lemma 5.6. Actually, we need only the following corollary.

Corollary 5.7**.**

The language $\mathcal{L}$ of bimodal formulas can be decided in logarithmic space.

Proof.

It is well-known that $\mathrm{ALOGTIME}$ is a subset of $\mathrm{LOGSPACE}$; see [4, Page 601]. ∎

Let $\Sigma:=\{(,),\neg,\Box,K,\wedge,x,0,1\}$ be the alphabet over which bimodal formulas are defined. In order to prove the assertion we have to show that there is a logspace computable function $\widetilde{T}:\Sigma^{*}\to\Sigma^{*}$ such that, for all $\varphi\in\Sigma^{*}$,

[TABLE]

We define such a function $\widetilde{T}$ by formulating an algorithm for computing it that works in logarithmic space.

So, let $\varphi\in\Sigma^{*}$ be the input string. According to Corollary 5.7 we can first check in logarithmic space whether $\varphi$ is a bimodal formula or not, that is, whether $\varphi$ is an element of $\mathcal{L}$ or not. If not then the algorithm outputs $\widetilde{T}(\varphi):=\wedge$ (which is certainly not a bimodal formula). If, on the other hand, $\varphi$ is a bimodal formula then we wish to compute and print $\widehat{T}(\varphi)$ as defined in Subsection 5.1.

First, we compute the smallest natural number $i$ such that $x{\rm bin}(i)$ is not a subformula of $\varphi$. We do this by starting with $j=0$, increasing $j$ step by step, and checking in each step whether $x{\rm bin}(j)$ is a subformula of $\varphi$. Note that a string $x{\rm bin}(j)$ for some $j\in\mathbb{N}$ is a subformula of $\varphi$ if, and only if, there exists an occurrence of the string $x{\rm bin}(j)$ as a substring of $\varphi$ that is not followed by a [math] or a $1$. This algorithm works in logarithmic space because $\varphi$ can contain only less than $|\varphi|$ many subformulas of the form $x{\rm bin}(j)$. Thus, we need to check whether $x{\rm bin}(j)$ is a subformula of $\varphi$ only for $j<|\varphi|$. For all these $j$ the binary representation ${\rm bin}(j)$ can be stored in logarithmic space. Finally, we can also store the string $\mathrm{main}:=x{\rm bin}(i)$ in logarithmic space.

Now we wish to compute and output $\widehat{T}(\varphi)$. It is straightforward to print $\mathrm{main}\wedge K\Box(\neg\mathrm{main}\to\Box\neg\mathrm{main})$. Next we wish to print $persistent_{main}$. In order to do this we must identify all $j\in\mathbb{N}$ such that $x{\rm bin}(j)$ is a subformula of $\varphi$, and for each such $j$ we must print

[TABLE]

This can be done as follows. We read the string $\varphi$ from left to right. Whenever we read an $x$ we use two binary counters in order to mark the beginning and the end of the subformula $x{\rm bin}(j)$ that begins with this occurrence of $x$. Then we check, again using binary counters, whether the same subformula $x{\rm bin}(j)$ has appeared already further to the left in $\varphi$. If it has then we just move on. If it has not appeared before, then we print out $K(\Box(\mathrm{main}\to x{\rm bin}(j))\vee\Box(\mathrm{main}\to\neg x{\rm bin}(j)))$, and then we move on. It is clear that all this can be done in logarithmic space.

Finally, we wish to output $T(\varphi)$. In order to compute $T(\varphi)$ one has to replace every occurrence of “$K$” by “$K\neg(\mathrm{main}\wedge\neg$”, and every occurrence of “$\Box$” by “$\Box\neg(\mathrm{main}\wedge\neg$”, and one has to add an additional closing bracket after each subformula $K\psi$ and each subformula $\Box\psi$ of $\varphi$. Besides that, all other symbols from $\varphi$ can simply be copied. The only nontrivial part here is the addition of a closing bracket after each occurrence of a subformula of the form $K\psi$ or $\Box\psi$ of $\varphi$. In order to do this, for each position in the string $\varphi$ one has to count how many subformulas of the form $K\psi$ or $\Box\psi$ of $\varphi$ end in this position and then one has to print so many additional closing brackets. So, how can one count how many subformulas of the form $K\psi$ or $\Box\psi$ of $\varphi$ end in the current position in the string $\varphi$? If the symbol in this position is an element of $\{(,\neg,\Box,K,\wedge,x\}$ then no subformula ends in this position. The same is true if the symbol in this position is either [math] or $1$ and this is followed by a bit [math] or $1$ as well. There are only the following possible cases for the last symbol of a subformula.

• •

If the symbol in the current position is a bit, so [math] or $1$, and this is not followed by a bit, then a subformula of the form $x{\rm bin}(j)$ for some $j$ ends in this position. Then we move to the left of the corresponding occurrence of $x$ and count the number of occurrences of $K$ and $\Box$ until we read a symbol not in $\{K,\Box,\neg\}$.

• •

If the symbol in the current position is a closing bracket $)$ then we go to the left step by step until we have found the corresponding opening bracket $($. This can be done by using a binary counter that is increased by $1$ for each closing bracket and decreased by $1$ for each opening bracket. One stops when this counter is back to its initial value [math]. Once we have found the corresponding opening bracket we move to the left of it and count the number of occurrences of $K$ and $\Box$ until we read a symbol not in $\{K,\Box,\neg\}$.

By using binary counters all this can be done in logarithmic space. This ends the description of the computation in logarithmic space of the described reduction function $\widetilde{T}$.

6 Reduction of $\mathrm{S4\times S5}$ to $\mathrm{K4\times S5}$

The $\mathrm{EXPSPACE}$-hardness of $\mathrm{K4\times S5}$ follows from the $\mathrm{EXPSPACE}$-hardness of $\mathrm{S4\times S5}$ and from the following result.

Theorem 6.1**.**

The satisfiability problem of the bimodal logic $\mathrm{S4\times S5}$ can be reduced in logarithmic space to the satisfiability problem of the bimodal logic $\mathrm{K4\times S5}$.

We start with the definition of the reduction function $\widehat{T}$ translating bimodal formulas in the language $\mathcal{L}$ to bimodal formulas in $\mathcal{L}$ such that for all $\varphi\in\mathcal{L}$:

[TABLE]

The problem that we face is that in general $\mathrm{K4\times S5}$-models are not reflexive. To handle this we add to the original formula $\varphi$ a formula that implies that all those instances of the reflexivity axiom scheme $\Box\psi\to\psi$ where $\Box\psi$ is a subformula of $\varphi$ must hold true in all reachable points.

Definition 6.2** (Translation $\widehat{T}$).**

For $\varphi\in\mathcal{L}$ we define a function $\widehat{T}:\mathcal{L}\to\mathcal{L}$ by

[TABLE]

We claim that the function $\widehat{T}$ is indeed a reduction function from the satisfiability problem of $\mathrm{S4\times S5}$ to the satisfiability problem of $\mathrm{K4\times S5}$.

Proposition 6.3**.**

The function $\widehat{T}:\mathcal{L}\to\mathcal{L}$ satisfies, for all $\varphi\in\mathcal{L}$,

[TABLE]

Proof.

Let $\varphi$ be $\mathrm{S4\times S5}$–satisfiable. There are an $\mathrm{S4\times S5}$-commutator model $M=(W,\stackrel{{\scriptstyle\Diamond}}{{\to}},\stackrel{{\scriptstyle L}}{{\to}},\sigma)$ and a point $w\in W$ such that $M,w\models\varphi$. Since the relation $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ in $M$ is reflexive we have for all $w^{\prime}\in W$ that $M,w^{\prime}\models\bigwedge_{\Box\psi\;\in\,\mathrm{sf}(\varphi)}(\Box\psi\to\psi)$. Hence, $M,w\models\bigwedge_{\Box\psi\;\in\,\mathrm{sf}(\varphi)}K((\Box\psi\to\psi)\wedge\Box(\Box\psi\to\psi))$, in other words, $M,w\models\widehat{T}(\varphi)$. Furthermore, $M$ satisfies the conditions for $\mathrm{K4\times S5}$-commutator models because the relation $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ in $M$ is transitive as well. Hence, $\widehat{T}(\varphi)$ is $\mathrm{K4\times S5}$-satisfiable.

For the other direction of the equivalence let us assume that $\widehat{T}(\varphi)$ is $\mathrm{K4\times S5}$-satisfiable. This implies that there exist a $\mathrm{K4\times S5}$–commutator model $M^{\prime}=(W^{\prime},\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}},\stackrel{{\scriptstyle L^{\prime}}}{{\to}},\sigma^{\prime})$ and a point $w\in W^{\prime}$ such that $M^{\prime},w\models\widehat{T}(\varphi)$, that is

[TABLE]

We construct an $\mathrm{S4\times S5}$–commutator model $M:=(W,\stackrel{{\scriptstyle\Diamond}}{{\to}},\stackrel{{\scriptstyle L}}{{\to}},\sigma)$ for $\varphi$ as follows. We construct $M$ as a rooted model, where all points are reachable from the point $w$:

[TABLE]

We define the relations $\stackrel{{\scriptstyle L}}{{\to}}$ and $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ on $W$ simply by

[TABLE]

Finally,

[TABLE]

for all $A\in AT$.

It is clear that $w\in W$, and it is straightforward to see that $M$ is an $\mathrm{S4\times S5}$-commutator model. We claim that $M,w\models\varphi$. By induction on the structure of $\psi$ we show the stronger assertion:

[TABLE]

for all $v\in W$ and for all $\psi\in\mathrm{sf}(\varphi)$. We distinguish the following cases:

• •

Case $\psi=A\in AT$. In this case the claim follows directly from the definition of $\sigma$.

• •

Case $\psi=\neg\chi$ or $\psi=(\chi_{1}\wedge\chi_{2})$. In both cases the claim follows directly from the induction hypothesis.

• •

Case $\psi=\Box\chi$. Let us first assume $M^{\prime},v\models\Box\chi$. We wish to show $M,v\models\Box\chi$. Consider an arbitrary $v^{\prime}\in W$ with $v\stackrel{{\scriptstyle\Diamond}}{{\to}}v^{\prime}$. It is sufficient to show $M,v^{\prime}\models\chi$. Note that the definition of $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ implies that $v\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}v^{\prime}$ or $v=v^{\prime}$. In the first case, $v\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}v^{\prime}$, the assumption $M^{\prime},v\models\Box\chi$ directly implies $M^{\prime},v^{\prime}\models\chi$. By induction hypothesis we obtain $M,v^{\prime}\models\chi$. In the second case, $v=v^{\prime}$, we use the fact that $M^{\prime},w\models K((\Box\chi\to\chi)\wedge\Box(\Box\chi\to\chi))$ and $v\in W$ imply $M^{\prime},v\models(\Box\chi\to\chi)$. Together with $M^{\prime},v\models\Box\chi$ this implies $M^{\prime},v\models\chi$, hence, $M^{\prime},v^{\prime}\models\chi$. By induction hypothesis we obtain $M,v^{\prime}\models\chi$ as well.

For the other direction let us assume that $M,v\models\Box\chi$. We wish to show $M^{\prime},v\models\Box\chi$. Consider an arbitrary $v^{\prime}\in W^{\prime}$ with $v\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}v^{\prime}$. It is sufficient to show $M^{\prime},v^{\prime}\models\chi$. But from $v\in W$ and $v\stackrel{{\scriptstyle\Diamond^{\prime}}}{{\to}}v^{\prime}$ we conclude $v^{\prime}\in W$ and $v\stackrel{{\scriptstyle\Diamond}}{{\to}}v^{\prime}$. Hence, $M,v\models\Box\chi$ implies $M,v^{\prime}\models\chi$. By induction hypothesis we obtain $M^{\prime},v^{\prime}\models\chi$.

• •

Case $\psi=K\chi$. This case can be treated similarly. For the direction “$\Rightarrow$” one needs to use left commutativity. The details are left to the reader. ∎

Proof of Theorem 6.1.

Let $\Sigma=:\{(,),\neg,\Box,K,\wedge,x,0,1\}$ be the alphabet over which bimodal formulas are defined. In order to prove the assertion we have to show that there is a logspace computable function $\widetilde{T}:\Sigma^{*}\to\Sigma^{*}$ such that, for all $\varphi\in\Sigma^{*}$,

[TABLE]

We define such a function $\widetilde{T}$ by formulating an algorithm for computing it that works in logarithmic space.

So, let $\varphi\in\Sigma^{*}$ be the input string. According to Corollary 5.7 we can first check in logarithmic space whether $\varphi$ is a bimodal formula or not, that is, whether $\varphi$ is an element of $\mathcal{L}$ or not. If not then the algorithm outputs $\widetilde{T}(\varphi):=\wedge$ (which is certainly not a bimodal formula). If, on the other hand, $\varphi$ is a bimodal formula then we wish to compute and print $\widetilde{T}(\varphi):=\widehat{T}(\varphi)$ as defined in Definition 6.2. The algorithm that prints $\widehat{T}(\varphi)$ works as follows.

It prints $\varphi$. 2. 2.

For each $\Box\psi\in\mathrm{sf}(\varphi)$ it prints the string

[TABLE]

Of course, for the second part, for every occurrence of the symbol $\Box$ in $\varphi$ one has to determine the uniquely determined formula $\psi$ beginning in $\varphi$ immediately to the right of this occurrence of $\Box$. Then one has to print the string above. All this can be done using several binary counters. First one sets a binary counter called StartOfPsi to the value of the position to the right of the current occurrence of $\Box$. In order to compute the correct value of a binary counter EndOfPsi that is supposed to be the position of the rightmost symbol in $\psi$ one proceeds as follows. Starting from the position StartOfPsi one reads the given string from left to right. As long as the read symbol is $\neg$ or $\Box$ or $K$ one continues reading. At some stage one will either read an $x$ or an opening bracket $($. If one reads an $x$ then EndOfPsi is set to the position of the rightmost bit, that is, the rightmost [math] or $1$, such that between this symbol and the just read occurrence of $x$ there are only bits. If one reads an opening bracket then EndOfPsi is set to the position of the first closing bracket to the right of this opening bracket such that the string between these two brackets contains as many closing as opening brackets. Note that all this can be done in logarithmic space.

Finally, using the two binary counters StartOfPsi and EndOfPsi containing the positions of the first and the last symbol of $\psi$ it is clear that one can print the string “$\wedge K((\Box\psi\to\psi)\wedge\Box(\Box\psi\to\psi))$”, again using additional binary counters that use only logarithmic space. This ends the description of the computation in logarithmic space of the described reduction function $\widetilde{T}$. ∎

Appendix A Reduction of Alternating Turing Machines Working in Exponential Time to $\mathrm{S4\times S5}$

In Section 4 we have shown that any language recognized by an Alternating Turing Machine working in exponential time can be reduced in logarithmic space to the satisfiability problem of $\mathrm{SSL}$. This shows that the satisfiability problem of $\mathrm{SSL}$ is $\mathrm{EXPSPACE}$-hard under logspace reduction. In Section 5 we have shown that the satisfiability problem of $\mathrm{SSL}$ can be reduced in logarithmic space to the satisfiability problem of $\mathrm{S4\times S5}$. This proves the following theorem.

Theorem A.1**.**

The satisfiability problem of $\mathrm{S4\times S5}$ is $\mathrm{EXPSPACE}$-hard under logarithmic space reduction.

In this appendix we wish to given an alternative, “direct” proof of this theorem by showing directly that any language $L$ recognized by an Alternating Turing Machine working in exponential time can be reduced in logarithmic space to the satisfiability problem of $\mathrm{S4\times S5}$. The proof is quite similar to the reduction of Alternating Turing Machines working in exponential time to the satisfiability problem of $\mathrm{SSL}$ presented in Section 4. But, there are also some important differences between the two reductions. On the one hand, we are going to use certain “shared variables” as well, but the mechanism of shared variables in $\mathrm{S4\times S5}$ is much easier than in $\mathrm{SSL}$. On the other hand, the fact that in $\mathrm{S4\times S5}$ the left commutativity property and the right commutativity property hold true (while in $\mathrm{SSL}$ only the left commutativity property has to hold true) causes problems that were not present in our treatment of $\mathrm{SSL}$ in Section 4. Similarly as in that section, for $\mathrm{S4\times S5}$ we will model nodes in an accepting tree of an Alternating Turing Machine by clouds in an $\mathrm{S4\times S5}$-product model. But the commutativity properties have the consequence that for every point in every cloud there exists a copy in every other cloud. The result is that in a cloud modeling a certain node on some path in an accepting tree there are also points that come from other nodes on other computation paths, perhaps even with the same time stamp. This makes the isolation of the correct points carrying the required information (in particular the information about the symbol to be read at a certain time on some computation path) more difficult. For details see Subsection A.2 where the reduction function is defined and explained.

In the first of the following five subsections we present an implementation of a binary counter in $\mathrm{S4\times S5}$, similar to the implementation of a binary counter in $\mathrm{SSL}$ in Subsection 3.2. In the second subsection we give an outline of the definition of the reduction function and then define the reduction function $f_{\mathrm{S4\times S5}}$ formally. In the third subsection we show that the reduction function $f_{\mathrm{S4\times S5}}$ can be computed in logarithmic space. The final two subsections are devoted to the correctness proof of the reduction. First we show that in the case $w\in L$ the formula $f_{\mathrm{S4\times S5}}(w)$ is $\mathrm{S4\times S5}$-satisfiable by explicitly constructing an $\mathrm{S4\times S5}$-product model for $f_{\mathrm{S4\times S5}}(w)$. In the last section we show that if $f_{\mathrm{S4\times S5}}(w)$ is $\mathrm{S4\times S5}$-satisfiable then $w$ is an element of $L$.

A.1 Binary Counters in $\mathrm{S4\times S5}$

Fix some natural number $n\geq 1$. We wish to implement in $\mathrm{S4\times S5}$ a binary $n$-bit counter that counts from [math] to $2^{n}-1$. That means, we wish to construct an $\mathrm{S4\times S5}$-satisfiable formula with the property that any model of it contains a sequence of pairwise distinct points $p_{0},\ldots,p_{2^{n}-1}$ such that, for each $i\in\{0,\ldots,2^{n}-1\}$, at the point $p_{i}$ the number $i$ is stored in binary form in a certain way.

Additionally, we need to copy and transmit various bits of information, both in the $\stackrel{{\scriptstyle\Diamond}}{{\to}}$-direction as well as in the $\stackrel{{\scriptstyle L}}{{\to}}$-direction This will be done by two kinds of formulas.

• •

On the one hand, we need formulas that have the same truth value in the vertical ($\stackrel{{\scriptstyle\Diamond}}{{\to}}$) direction but can change their truth values in the horizontal ($\stackrel{{\scriptstyle L}}{{\to}}$) direction. In the logic $\mathrm{S4\times S5}$ we can force certain propositional variables to be persistent by a suitable formula.

• •

On the other hand, we need formulas that have the same truth value in the horizontal ($\stackrel{{\scriptstyle L}}{{\to}}$) direction but can change their truth values in the vertical ($\stackrel{{\scriptstyle\Diamond}}{{\to}}$) direction. Such formulas will be called shared variables. In the logic $\mathrm{S4\times S5}$ they can be defined as follows. For $i\in\mathbb{N}$ let $A_{i}$ be special propositional variables. The shared variables $\alpha_{i}$ are defined as

[TABLE]

Note that $\neg\alpha_{i}\equiv K\neg A_{i}$.

In the following we use the abbreviations introduced above, in Table 1, and in Table 3.

The idea of the construction is the same as in Subsection 3.2.

• •

We store the counter values in a vector $\underline{\alpha}:=\alpha_{n-1},\ldots,\alpha_{0}$ of shared variables. To this end we embed the sequence $p_{0},\ldots,p_{2^{n}-1}$ of points in a sequence of clouds $\mathit{C}_{0},\ldots,\mathit{C}_{2^{n-1}}$ such that the cloud $\mathit{C}_{i}$ contains the point $p_{i}$ and such that the vector $\underline{\alpha}$ of shared variables satisfied at $p_{i}$ (and hence at all points in $\mathit{C}_{i}$) encodes the number $i$.

• •

Let $i\leq 2^{n}-1$ be the number encoded by $\underline{\alpha}$. If $\underline{\alpha}$ contains no [math] then $i$ has reached its highest posible value, the number $2^{n}-1$. Otherwise let $k$ be the position of the rightmost [math]. We determine the position $k$ with the aid of the formula $\mathrm{rightmost\_zero}(\alpha,k)$. In order to increment the counter we have to keep all $\alpha_{j}$ at positions $j>k$ unchanged and to switch all $\alpha_{j}$ at positions $j\leq k$. We do this in two steps:

First me make an $\stackrel{{\scriptstyle L}}{{\to}}$-step from the point $p_{i}$ to a point $p^{\prime}_{i}$ where we store the number $i+1$ in a vector $\underline{X}:=X_{n-1},\ldots,X_{0}$ of usual propositional variables by demanding that

[TABLE] 2. 2.

Then we make a $\stackrel{{\scriptstyle\Diamond}}{{\to}}$-step from the point $p^{\prime}_{i}$ to a point $p_{i+1}$ in the cloud $\mathit{C}_{i+1}$ and demand that

[TABLE]

Note that the value of $\underline{X}$ is copied from $p^{\prime}_{i}$ to its $\stackrel{{\scriptstyle\Diamond}}{{\to}}$-successor $p_{i+1}$ because by the formula

[TABLE]

we force the vector $\underline{X}$ of propositional variables to be persistent.

Altogether we demand that for the number $k$

[TABLE]

• •

Additionally we need a formula to ensure that the starting value is [math], that is we demand

[TABLE]

We now define the complete counter formula, for $n>0$.

[TABLE]

Proposition A.2**.**

For all $n\in\mathbb{N}\setminus\{0\}$, the formula $\mathrm{counter}_{\mathrm{S4\times S5},n}$ is $\mathrm{S4\times S5}$-satisfiable. 2. 2.

For all $n\in\mathbb{N}\setminus\{0\}$, for every $\mathrm{S4\times S5}$-commutator model of $\mathrm{counter}_{\mathrm{S4\times S5},n}$ and for every point $p_{0}$ in this model with $p_{0}\models\mathrm{counter}_{\mathrm{SSL},n}$ there exist a sequence of $2^{n}-1$ points $p_{1},p_{2},\ldots,p_{2^{n}-1}$ and a sequence of $2^{n}-1$ points $p_{0}^{\prime},p_{1}^{\prime},\ldots,p^{\prime}_{2^{n}-2}$ such that

• •

for $0\leq i\leq 2^{n}-1$,  $p_{i}\models(\underline{\alpha}=\mathrm{bin}_{n}(i))$,

• •

for $0\leq i\leq 2^{n}-2$,  $p_{i}\stackrel{{\scriptstyle L}}{{\to}}p^{\prime}_{i}$ and $p^{\prime}_{i}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{i+1}$ and $p^{\prime}_{i}\models(\underline{X}=\mathrm{bin}_{n}(i+1))$.

Proof.

For the following let us fix some $n>0$.

We construct an $\mathrm{S4\times S5}$-product model $M$ with a point $(0,0)$ in $M$ such that $M,(0,0)\models\mathrm{counter}_{\mathrm{S4\times S5},n}$ as follows; see Figure 6. We define an S4-frame $(W_{1},R_{\Diamond})$ by

[TABLE]

We define an S5-frame $(W_{2},R_{L})$ by

[TABLE]

Then the product frame $(W,\stackrel{{\scriptstyle\Diamond}}{{\to}},\stackrel{{\scriptstyle L}}{{\to}})$ with $W:=W_{1}\times W_{2}$ and with $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ and $\stackrel{{\scriptstyle L}}{{\to}}$ defined as in [8, Definition 2.2] is an $\mathrm{S4\times S5}$-frame. We define the valuation $\sigma$ by

[TABLE]

for $k\in\{0,\ldots,n-1\}$. This implies for all $i,j\in\{0,\ldots,2^{n}-1\}$

[TABLE]

We claim

[TABLE]

Indeed, it is clear that the propositional variables $X_{k}$ are persistent, hence, we have

[TABLE]

It is also clear that

[TABLE]

Let us assume that for some $(i,j)\in W$ and some $k\in\{0,\ldots,n-1\}$ we have

[TABLE]

It is sufficient to show that

[TABLE]

Indeed, $(i,j)\models\mathrm{rightmost\_zero}(\underline{\alpha},k)$ implies $\{0,\ldots,n-1\}\setminus\mathrm{Ones}(i)\neq\emptyset$ and $k=\min(\{0,\ldots,n-1\}\setminus\mathrm{Ones}(i))$. Note that this implies $i<2^{n}-1$, hence, $(i,i+1)\in W$ and $(i+1,i+1)\in W$. In view of $(i,j)\stackrel{{\scriptstyle L}}{{\to}}(i,i+1)\stackrel{{\scriptstyle\Diamond}}{{\to}}(i+1,i+1)$ it is sufficient to show

[TABLE]

and

[TABLE]

Both claims follow from the facts that $k=\min(\{0,\ldots,n-1\}\setminus\mathrm{Ones}(i))$ and that every point $(x,y)\in W$ satisfies the formulas $(\underline{\alpha}=\mathrm{bin}_{n}(x))$ and $(\underline{X}=\mathrm{bin}_{n}(y))$. 2. 2.

The proof for $\mathrm{S4\times S5}$-commutator models of the formula $\mathrm{counter}_{\mathrm{S4\times S5},n}$ is very similar to the proof for cross axiom models of the formula $\mathrm{counter}_{\mathrm{SSL},n}$ in Proposition 3.2. For completeness sake we explicate it in detail. Suppose there are an $\mathrm{S4\times S5}$-commutator model $M$ of the formula $\mathrm{counter}_{\mathrm{S4\times S5},n}$ and a point $p_{0}\in M$ with $M,p_{0}\models\mathrm{counter}_{\mathrm{S4\times S5},n}$. We show by induction that the claimed sequences of points $p_{1},\ldots p_{2^{n}-1}$ and $p^{\prime}_{0},\ldots p^{\prime}_{2^{n}-2}$ with the claimed properties exist. In addition, we show that there exist points $t_{i}$ with $p_{0}\stackrel{{\scriptstyle L}}{{\to}}t_{i}$ and $t_{i}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{i}$, for $1\leq i\leq 2^{n}-1$. Note that the sequences $p_{0},\ldots p_{2^{n}-1}$ and $p^{\prime}_{0},\ldots p^{\prime}_{2^{n}-2}$ are supposed to form a “staircase” as in Figure 3. By definition, $p_{0}\models\mathrm{persistent}(\underline{X})\wedge(\underline{\alpha}=\mathrm{bin}_{n}(0))$. By induction hypothesis, let us assume that for some $m$ with $0\leq m<2^{n}-1$ there exist $p_{1},\ldots,p_{m}$ and $p^{\prime}_{0},\ldots,p_{m-1}^{\prime}$ with

[TABLE]

with

[TABLE]

for $0\leq i\leq m$, and with

[TABLE]

for $0\leq i<m$, and that there are $t_{i}$ with $p_{0}\stackrel{{\scriptstyle L}}{{\to}}t_{i}$ and $t_{i}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{i}$, for $1\leq i\leq m$. Since $m<2^{n}-1$, the set $\{0,\ldots,n-1\}\setminus\mathrm{Ones}(m)$ is nonempty. With $k:=\min(\{0,\ldots,n-1\}\setminus\mathrm{Ones}(m))$ we have

[TABLE]

Due to $p_{0}\models\mathrm{counter}_{\mathrm{S4\times S5},n}$ as well as $p_{0}\stackrel{{\scriptstyle L}}{{\to}}t_{m}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{m}$ this implies

[TABLE]

Thus, there must exist points $p^{\prime}_{m}$ and $p_{m+1}$ satisfying $p_{m}\stackrel{{\scriptstyle L}}{{\to}}p^{\prime}_{m}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{m+1}$ as well as

[TABLE]

and

[TABLE]

We have to show

[TABLE]

and

[TABLE]

Due to the fact that $p^{\prime}_{m}$ is an element of the same cloud as $p_{m}$, and $\underline{\alpha}$ has the same value in all points in a cloud we obtain

[TABLE]

Together with

[TABLE]

this implies

[TABLE]

(the values of the leading bits $\alpha_{n-1},\ldots,\alpha_{k+1}$ of $\underline{\alpha}$ are copied to the leading bits $X_{n-1},\ldots,X_{k+1}$ and the other bits are defined explicitly by $p^{\prime}_{m}\models\mathrm{rightmost\_one}(\underline{X},k)$ so that the binary value of $\underline{X}$ is $m+1$). From $p_{0}\models\mathrm{persistent}(\underline{X})$ as well as $p_{0}\stackrel{{\scriptstyle L}}{{\to}}t_{m}\stackrel{{\scriptstyle\Diamond}}{{\to}}p^{\prime}_{m}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{m+1}$ we obtain $p_{m+1}\models(\underline{X}=\mathrm{bin}_{n}(m+1))$. Using $p_{m+1}\models(\underline{X}=\underline{\alpha})$ we obtain $p_{m+1}\models(\underline{\alpha}=\mathrm{bin}_{n}(m+1))$. Finally, the left commutativity property applied to $t_{m}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{m}$ and $p_{m}\stackrel{{\scriptstyle L}}{{\to}}p^{\prime}_{m}$ implies that there exists a point $t_{m+1}$ with $t_{m}\stackrel{{\scriptstyle L}}{{\to}}t_{m+1}$ and $t_{m+1}\stackrel{{\scriptstyle\Diamond}}{{\to}}p^{\prime}_{m}$. Using additionally $p_{0}\stackrel{{\scriptstyle L}}{{\to}}t_{m}$ and $p^{\prime}_{m}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{m+1}$ we obtain $p_{0}\stackrel{{\scriptstyle L}}{{\to}}t_{m+1}$ and $t_{m+1}\stackrel{{\scriptstyle\Diamond}}{{\to}}p_{m+1}$. This ends the proof of the second assertion. ∎

A.2 Construction of the Formula

Let $L\in\mathrm{EXPSPACE}$ be an arbitrary language over some alphabet $\Sigma$, that is, $L\subseteq\Sigma^{*}$. We are going to show that there is a logspace computable function $f_{\mathrm{S4\times S5}}$ mapping strings to strings such that, for any $w\in\Sigma^{*}$,

• •

$f_{\mathrm{S4\times S5}}(w)$ is a bimodal formula and

• •

$f_{\mathrm{S4\times S5}}(w)$ is $\mathrm{S4\times S5}$-satisfiable if, and only if, $w\in L$.

Once we have shown this, we have shown the result.

In order to define this desired reduction function $f_{\mathrm{S4\times S5}}$, we are going to make use of an Alternating Turing Machine for $L$. Since $\mathrm{EXPSPACE}=\mathrm{AEXPTIME}$, there exist an Alternating Turing Machine $M=(Q,\Sigma,\Gamma,q_{0},\delta)$ and a univariate polynomial $p$ such that $M$ accepts $L$, that is, $L(M)=L$, and such that the time used by $M$ on arbitrary input of length $n$ is bounded by $2^{p(n)}-1$. We can assume without loss of generality $Q=\{0,\ldots,|Q|-1\}$, $\Gamma=\{0,\ldots,|\Gamma|-1\}$, that the coefficients of the polynomial $p$ are natural numbers and that, for all $n\in\mathbb{N}$, we have $p(n)\geq n$ and $p(n)\geq 1$. In the following, whenever we have fixed some $n\in\mathbb{N}$, we set

[TABLE]

Let us consider an input string $w\in\Sigma^{n}$ of length $n$, for some $n\in\mathbb{N}$, and let us sketch the main idea of the construction of the formula $f_{\mathrm{S4\times S5}}(w)$. The formula $f_{\mathrm{S4\times S5}}(w)$ will describe the possible computations of $M$ on input $w$ in the following sense: any $\mathrm{S4\times S5}$-product model of $f_{\mathrm{S4\times S5}}(w)$ will essentially contain an accepting tree of $M$ on input $w$, and if there exists an accepting tree of $M$ on input $w$ then one can turn this into an $\mathrm{S4\times S5}$-product model of $f_{\mathrm{S4\times S5}}(w)$. In such a model, any node in an accepting tree of $M$ on input $w$ will be modeled by a cloud (that is, by an $\stackrel{{\scriptstyle L}}{{\to}}$-equivalence class) in which certain shared variables (we use the notion “shared variables” in the same sense as in Subsection A.1) will have values that describe the data of the computation node that are important in this computation step. Which data are these? First of all, we need the time of the computation node. We assume that the computation starts with the initial configuration of $M$ on input $w$ at time [math]. Since the ATM $M$ needs at most $2^{N}-1$ time steps, we can store the time of each computation node in a binary counter counting from [math] to $2^{N}-1$. Since during each time step at most one additional cell either to the right or to the left of the previous cell can be visited, we can describe any configuration reachable during a computation of $M$ on input $w$ by the following data:

• •

the state $q\in Q$ of the configuration,

• •

the current content of the tape, given by a string in $\Gamma^{2\cdot(2^{N}-1)+1}=\Gamma^{2^{N+1}-1}$,

• •

the current position of the tape head, given by a number in $\{0,\ldots,2^{N+1}-2\}$.

We assume that in the initial configuration on input $w$ the tape content is $\#^{2^{N}}w\#^{2^{N}-1-n}$ (remember that we use $\#$ for the blank symbol) and that the tape head scans the blank $\#$ to the left of the first symbol of $w$, that is, the position of the tape head is $2^{N}-1$. If a cloud in an $\mathrm{S4\times S5}$-product model of $f_{\mathrm{S4\times S5}}(w)$ describes a computation node of $M$ on input $w$ then in this cloud the following shared variables will have the following values:

• •

a vector $\underline{\alpha}^{\mathrm{time}}=(\alpha^{\mathrm{time}}_{N-1},\ldots,\alpha^{\mathrm{time}}_{0})$ giving in binary the current time of the computation,

• •

a vector $\underline{\alpha}^{\mathrm{pos}}=(\alpha^{\mathrm{pos}}_{N},\ldots,\alpha^{\mathrm{pos}}_{0})$ giving in binary the current position of the tape head,

• •

a vector $\underline{\alpha}^{\mathrm{state}}=(\alpha^{\mathrm{state}}_{0},\ldots,\alpha^{\mathrm{state}}_{|Q|-1})$ giving in unary the current state of the computation (here “unary” means: exactly one of the shared variables $\alpha^{\mathrm{state}}_{i}$ will be true, namely the one with $i$ being the current state),

• •

a vector $\underline{\alpha}^{\mathrm{read}}=(\alpha^{\mathrm{read}}_{0},\ldots,\alpha^{\mathrm{read}}_{|\Gamma|-1})$ giving in unary the symbol in the current cell (here “unary” means: exactly one of the shared variables $\alpha^{\mathrm{read}}_{i}$ will be true, namely the one with $i$ being the symbol in the current cell),

• •

a vector $\underline{\alpha}^{\mathrm{written}}=(\alpha^{\mathrm{written}}_{0},\ldots,\alpha^{\mathrm{written}}_{|\Gamma|-1})$ giving in unary the symbol that has just been written into the cell that has just been left, unless the cloud corresponds to the first node in the computation tree — in that case the value of this vector is irrelevant (here “unary” means: exactly one of the variables $\alpha^{\mathrm{written}}_{i}$ will be true, namely the one with $i$ being the symbol that has just been written),

• •

a vector $\underline{\alpha}^{\mathrm{prevpos}}=(\alpha^{\mathrm{prevpos}}_{N},\ldots,\alpha^{\mathrm{prevpos}}_{0})$ giving in binary the previous position of the tape head, that is, the position of the cell that has just been left, unless the cloud corresponds to the first node in the computation tree — in that case the value of this vector is irrelevant.

The formula $f_{\mathrm{S4\times S5}}(w)$ has to ensure that for any possible computation step starting from such a computation node in an accepting tree there exists a cloud describing the corresponding successor node in the accepting tree. In this new cloud, the value of the counter for the time $\underline{\alpha}^{\mathrm{time}}$ has to be incremented. This can be done by the technique for implementing a binary counter in $\mathrm{S4\times S5}$ that was described in Subsection A.1. In parallel, we have to make sure that in this new cloud also the vectors $\underline{\alpha}^{\mathrm{pos}}$, $\underline{\alpha}^{\mathrm{state}}$, $\underline{\alpha}^{\mathrm{read}}$, $\underline{\alpha}^{\mathrm{written}}$, and $\underline{\alpha}^{\mathrm{prevpos}}$ are set to the right values. The vector $\underline{\alpha}^{\mathrm{prevpos}}$ is a copy of the vector $\underline{\alpha}^{\mathrm{pos}}$ in the previous cloud (we will see below how one can copy it). For the vectors $\underline{\alpha}^{\mathrm{pos}}$, $\underline{\alpha}^{\mathrm{state}}$, and $\underline{\alpha}^{\mathrm{written}}$ these values can be computed using the corresponding element of the transition relation $\delta$ of the ATM. For example, $\underline{\alpha}^{\mathrm{pos}}$ has to be decremented by one if the tape head moves to the left, and it has to be incremented by one if the tape head moves to the right. Also the new state (to be stored in $\underline{\alpha}^{\mathrm{state}}$) and the symbol written into the cell that has just been left (to be stored in $\underline{\alpha}^{\mathrm{written}}$) are determined by the data of the previous computation node and by the corresponding element of the transition relation $\delta$.

But the vector $\underline{\alpha}^{\mathrm{read}}$ is supposed to describe the symbol in the current cell. This symbol is not determined by the current computation step but has either been written the last time when this cell has been visited during this computation or, when this cell has never been visited before, the symbol in this cell is still the one that was contained in this cell before the computation started. How can one ensure that $\underline{\alpha}^{\mathrm{read}}$ is set to the right value? We will do this by using persistent variables and a variable $B^{\mathrm{active}}$ that is neither shared nor persistent. We will ensure that any cloud corresponding to a node in the computation tree in which the cell $i$ is being visited contains a point with a persistent position vector $\underline{X}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(i)$ and with a persistent time vector $\underline{X}^{\text{time-apv}}$ that will be forced to contain in binary form the time one step after the previous visit of the cell $i$ or, if the cell $i$ has not been visited before, to contain the value [math]. Furthermore, there will be a third persistent vector $\underline{X}^{\mathrm{read}}$. If the cell $i$ has not been visited before then we will make sure that the vector $\underline{X}^{\mathrm{read}}$ encodes the initial symbol contained in cell $i$. If the cell $i$ has been visited before then we will make sure that the vector $\underline{X}^{\mathrm{read}}$ encodes the symbol that has been written into the cell during the previous visit of the cell. In order to do that we need to determine the time of the previous visit. For that the Boolean variable $B^{\mathrm{active}}$ is used and the fact that due to the left commutativity property the point has $\stackrel{{\scriptstyle\Diamond}}{{\to}}$-predecessors in all clouds corresponding to any node on the path in the accepting tree from the root to the current cloud. Then, when one knows this time, one can look at the shared variable vector $\underline{\alpha}^{\mathrm{written}}$ in the cloud corresponding to the step after the previous visit of this cell (this shared variable vector encodes the symbol that has just been written into the cell) and can copy its value to the persistent variable vector $\underline{X}^{\mathrm{read}}$. In order to implement all this we use the following persistent variables:

• •

a vector $\underline{X}^{\text{time-apv}}=(X^{\text{time-apv}}_{N-1},\ldots,X^{\text{time-apv}}_{0})$ containing in binary the time one step after the previous visit of the current cell (the exponent of $X^{\text{time-apv}}_{i}$ stands for “time after previous visit”) or, if the current cell has not been visited before, containing in binary the number [math],

• •

a vector $\underline{X}^{\mathrm{pos}}=(X^{\mathrm{pos}}_{N},\ldots,X^{\mathrm{pos}}_{0})$ containing in binary the current position of the tape head, that is, the position of the current cell,

• •

a vector $\underline{X}^{\mathrm{read}}=(X^{\mathrm{read}}_{0},\ldots,X^{\mathrm{read}}_{|\Gamma|-1})$ giving in unary the symbol in the cell described by $\underline{X}^{\mathrm{pos}}$ (here “unary” means: exactly one of the shared variables $\alpha^{\mathrm{read}}_{i}$ will be true, namely the one with $i$ being the symbol in the cell described by $\underline{X}^{\mathrm{pos}}$),

In fact, the current cell may have been visited several times already. Of course only the $\stackrel{{\scriptstyle\Diamond}}{{\to}}$-successor of the point corresponding to the previous visit (that is, corresponding to the very last visit of the cell before the current visit, not earlier visits) should be allowed to copy the value of its vector $\underline{\alpha}^{\mathrm{written}}$ to $\underline{X}^{\mathrm{read}}$. In order to determine the right point, we are going to use an additional Boolean

• •

variable $B^{\mathrm{active}}$ (which is neither persistent nor shared) saying whether the current point is active or not.

We shall explain later how all this works. Finally, there are two more vectors of persistent variables that are needed for changing the values of the shared variable vectors $\underline{\alpha}^{\mathrm{time}}$ and $\underline{\alpha}^{\mathrm{pos}}$:

• •

a vector $\underline{X}^{\mathrm{prevtime}}=(X^{\mathrm{prevtime}}_{N-1},\ldots,X^{\mathrm{prevtime}}_{0})$ containing in binary the current time of the computation minus one, unless the cloud corresponds to the first node in the computation tree — in that case the value of this vector is irrelevant,

• •

a vector $\underline{X}^{\mathrm{prevpos}}=(X^{\mathrm{prevpos}}_{N},\ldots,X^{\mathrm{prevpos}}_{0})$ containing in binary the previous position of the tape head, that is, the position of the cell that has just been left, unless the cloud corresponds to the first node in the computation tree — in that case the value of this vector is irrelevant.

Now we come to the formal definition of the formula $f_{\mathrm{S4\times S5}}(w)$. The formula $f_{\mathrm{S4\times S5}}(w)$ will have the following structure:

[TABLE]

The formula $f_{\mathrm{S4\times S5}}(w)$ will contain the following propositional variables:

[TABLE]

For $\mathit{string}\in\{\mathrm{time},\mathrm{pos},\mathrm{state},\mathrm{read},\mathrm{prevpos},\mathrm{written}\}$ and natural numbers $i$ we use $\alpha^{\mathit{string}}_{i}$ as an abbreviation for $LA^{\mathit{string}}_{i}$. These formulas $\alpha^{\mathit{string}}_{i}$ are the shared variables we talked about above.

We are now going to define the subformulas of $f_{\mathrm{S4\times S5}}(w)$. We will use the abbreviations introduced above, in Table 1, in Table 2, and in Table 3.

The following formula makes sure that certain propositional variables are persistent:

[TABLE]

The following formula makes sure that in each of the vectors of shared or persistent variables that describe in a unary way the current state respectively the written symbol exactly one variable is true:

[TABLE]

The vector $\underline{\alpha}^{\mathrm{read}}$ will satisfy the same uniqueness condition automatically due to another formula (due to the formula $\mathit{read\_a\_symbol}$).

The following formula ensures that the shared variables in the cloud corresponding to the first node in a computation tree have the correct values. The computation starts at time [math] with the tape head at position $2^{N}-1$ and in the state $q_{0}$. The vector $\underline{\alpha}^{\mathrm{read}}$ will automatically get the correct value $\#$ due to the formulas $\mathit{read\_a\_symbol}$ and $\mathit{initial\_symbols}$, that will be introduced next. For the vectors $\underline{\alpha}^{\mathrm{prevpos}}$ and $\underline{\alpha}^{\mathrm{written}}$ we do not need to fix any values.

[TABLE]

The following formula ensures that whenever an initial symbol on the tape is requested (by a point with persistent time $\underline{X}^{\text{time-apv}}$ equal to [math]) it is stored in a persistent vector $\underline{X}^{\mathrm{read}}$ of this point.

[TABLE]

We explain this formula. By another formula we will ensure that whenever a cell is visited for the first time there will be an “active” point storing the position of this cell in a persistent vector $\underline{X}^{\mathrm{pos}}$ and such that its persistent time vector $\underline{X}^{\text{time-apv}}$ has the binary value [math]. The formula above ensures that the persistent vector $\underline{X}^{\mathrm{read}}$ in this point stores the correct initial symbol in this cell. This is either a symbol $w_{i}$ of the input string $w=w_{1}\ldots w_{n}$ or the blank $\#$.

The following formula ensures that whenever a symbol that has just been written on the tape is requested (by an active point with the correct persistent time $\underline{X}^{\text{time-apv}}$) then it is copied into a persistent vector $\underline{X}^{\mathrm{read}}$ of this point.

[TABLE]

The following formula ensures that the shared variable vector $\underline{\alpha}^{\mathrm{read}}$ describes the symbol in the current cell.

[TABLE]

where

[TABLE]

We explain these formulas. The formula $\mathit{existence\_of\_a\_reading\_point}$ enforces the existence of an “active” point in the current cloud that contains in the persistent vector $\underline{X}^{\mathrm{pos}}$ the number of the current cell and that we wish to force to contain in the persistent vector $\underline{X}^{\text{time-apv}}$ the time one step after the previous visit of this cell, if this cell has been visited before, or the value [math], otherwise. How can we enforce that? We make essential use of the left commutativity property. The point whose existence is ensured by the formula $\mathit{existence\_of\_a\_reading\_point}$ has $\stackrel{{\scriptstyle\Diamond}}{{\to}}$-predecessors in all clouds corresponding to the nodes on the path in the accepting tree from the root to the node corresponding to the current cloud. Since we demand $\underline{X}^{\text{time-apv}}\leq\underline{\alpha}^{\mathrm{time}}$ the time stored in binary in the persistent variable $\underline{X}^{\text{time-apv}}$ must be identical with the time of one of the clouds corresponding to a node on this path. The formula $\mathit{time\_of\_previous\_visit}$ ensures that if it is positive then it can be equal to the time $\underline{\alpha}^{\mathrm{time}}$ of a cloud corresponding to a node on this path only when $\underline{X}^{\mathrm{pos}}=\underline{\alpha}^{\mathrm{prevpos}}$, that is, only when in the step leading to this node something has been written into the current cell. So, if the current cell has not been visited before, the binary value of $\underline{X}^{\text{time-apv}}$ must be [math]. Then the formula $\mathit{initial\_symbols}$ will ensure that the persistent variable $\underline{X}^{\mathrm{read}}$ gets the correct value. Otherwise, when the cell has been visited before, in fact, it may have been visited several times already. In this case, we have to make sure that the number stored in $\underline{X}^{\text{time-apv}}$ is the time after the very last visit to this cell immediately before the current visit. This is ensured by the formulas $\mathit{becoming\_inactive}$ and $\mathit{staying\_inactive}$. If the number stored in $\underline{X}^{\text{time-apv}}$ were strictly smaller than the the time after the very last visit to this cell immediately before the current visit then, due to $\mathit{becoming\_inactive}$ the corresponding point would be set to “inactive”, and, due to $\mathit{staying\_inactive}$, also its $\stackrel{{\scriptstyle\Diamond}}{{\to}}$-successor would stay inactive. But this would apply also to the point in the current cloud which is supposed to be active and to contain the correct value in $\underline{X}^{\text{time-apv}}$ according to formula $\mathit{existence\_of\_a\_reading\_point}$. Thus, the first four subformulas of $\mathit{read\_a\_symbol}$ ensure that the current cloud contains an active point that contains in the persistent vector $\underline{X}^{\mathrm{pos}}$ the number of the current cell and that contains in the persistent vector $\underline{X}^{\text{time-apv}}$ the time one step after the previous visit of this cell, if this cell has been visited before, or the value [math], otherwise. Finally, the formula $\mathit{storing\_the\_read\_symbol}$ makes sure that the value of $\underline{X}^{\mathrm{read}}$ (which contains the symbol written into the current cell during the previous visit of this cell, or, if the current cell has not been visited before, the initial symbol in this cell) is copied into the shared variable vector $\underline{\alpha}^{\mathrm{read}}$.

Next, we wish to define the formula $\mathit{computation}$ that describes the computation steps. We have to distinguish between the two cases whether the tape head is going to move to the left or to the right. If in a computation step the symbol $\theta\in\Gamma$ is written into the current cell, if the tape head moves to the right, and if the new state after this step is the state $r\in Q$, then the following formula $\mathit{compstep}_{\mathrm{right}}(r,\theta)$ guarantees the existence of a point and its cloud with suitable values in the shared variable vectors $\underline{\alpha}^{\mathrm{time}},\underline{\alpha}^{\mathrm{pos}},\underline{\alpha}^{\mathrm{prevpos}},\underline{\alpha}^{\mathrm{state}},\underline{\alpha}^{\mathrm{written}}$.

We explain this formula. The first four lines of this formula take care that the two binary counters $\underline{\alpha}^{\mathrm{time}}$ and $\underline{\alpha}^{\mathrm{pos}}$ for the current time and for the current position of the tape head are incremented at the same time. This is similar to the formula $\mathrm{counter}_{\mathrm{S4\times S5},n}$ in Subsection A.1. Furthermore, also the persistent vectors $\underline{X}^{\mathrm{prevtime}}$ (that we will not need otherwise) and $\underline{X}^{\mathrm{prevpos}}$ (that we use again in the fifth line of this formula) get the correct values. The fifth line ensures that the shared variable vectors $\underline{\alpha}^{\mathrm{prevpos}}$, $\underline{\alpha}^{\mathrm{state}}$ and $\underline{\alpha}^{\mathrm{written}}$ of the current point get the correct values. The shared variable vector $\underline{\alpha}^{\mathrm{read}}$ will get the correct value due to the formulas $\mathit{initial\_symbols}$, $\mathit{written\_symbols}$, and $\mathit{read\_a\_symbol}$.

[TABLE]

If in a computation step the symbol $\theta\in\Gamma$ is written into the current cell, if the tape head moves to the left, and if the new state after this step is the state $r\in Q$, then the following formula guarantees the existence of a point and its cloud with suitable values in the shared variables.

[TABLE]

This formula is very similar to the previous one with the exception that here the binary counter for the position of the tape head is decremented.

The computation is modeled by the following subformula. Remember that $Q$ is the disjoint union of the sets $\{q_{\mathrm{accept}}\}$, $\{q_{\mathrm{reject}}\}$, $Q_{\forall}$, $Q_{\exists}$.

[TABLE]

Finally, the subformula $\mathit{no\_reject}$ is defined as follows.

[TABLE]

We have completed the description of the formula $f_{\mathrm{S4\times S5}}(w)$ for $w\in\Sigma^{*}$. It is clear that $f_{\mathrm{S4\times S5}}(w)$ is a bimodal formula, for any $w\in\Sigma^{*}$. We still have to show two claims:

The function $f_{\mathrm{S4\times S5}}$ can be computed in logarithmic space. 2. 2.

For any $w\in\Sigma^{*}$,

[TABLE]

The first claim is shown in the following section. The two directions of the equivalence in the second claim are shown afterwards in separate sections.

A.3 LOGSPACE Computability of the Reduction

We wish to show that the function $f_{\mathrm{S4\times S5}}$ can be computed in logarithmic space. This is shown by the same argument as the corresponding claim for the function $f_{\mathrm{SSL}}$ in Subsection 4.2.

A.4 Construction of a Model

In this section we show for any $w\in\Sigma^{*}$, if $w\in L$ then the bimodal formula $f_{\mathrm{S4\times S5}}(w)$ is $\mathrm{S4\times S5}$-satisfiable. Let us assume $w\in L$. We are going to explicitly define an $\mathrm{S4\times S5}$-product model of $f_{\mathrm{S4\times S5}}(w)$.

There exists an accepting tree $T=(V,E,c)$ of $M$ on input $w$, where $V$ is the set of nodes of $T$, where $E\subseteq V\times V$ is the set of edges, and where the function $c:V\to Q\times\{0,\ldots,2^{N+1}-2\}\times\Gamma^{2^{N+1}-1}$ labels each node with a configuration (remember the discussion about the description of configurations at the beginning of Subsection A.2). Let $\mathit{root}\in V$ be the root of $T$. We will now construct an $\mathrm{S4\times S5}$-product model of $f_{\mathrm{S4\times S5}}(w)$. We define an $S4$-frame $(W_{1},R_{\Diamond})$ by

[TABLE]

That means, for any $v,v^{\prime}\in W_{1}$ we have $vR_{\Diamond}v^{\prime}$ iff in the tree $T$ there is a path from $v$ to $v^{\prime}$. We define an $S5$-frame $(W_{2},R_{L})$ by

[TABLE]

Then the product frame $(W,\stackrel{{\scriptstyle\Diamond}}{{\to}},\stackrel{{\scriptstyle L}}{{\to}})$ with $W:=W_{1}\times W_{2}$ and with $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ and $\stackrel{{\scriptstyle L}}{{\to}}$ defined as in [8, Definition 2.3] is an $\mathrm{S4\times S5}$-product frame. We still need to define a suitable valuation $\sigma$. We define the valuation $\sigma$ as follows.

[TABLE]

for $k\in\{0,\ldots,N-1\}$,

[TABLE]

for $k\in\{0,\ldots,N\}$,

[TABLE]

for $q\in Q$,

[TABLE]

for $\eta\in\Gamma$,

[TABLE]

We have defined an $\mathrm{S4\times S5}$-product model $(W_{1}\times W_{2},\stackrel{{\scriptstyle\Diamond}}{{\to}},\stackrel{{\scriptstyle L}}{{\to}})$. We claim that in this model $(\mathit{root},\mathit{root})\models f_{\mathrm{S4\times S5}}(w)$. For an illustration of an important detail of the model see Figure 7.

First, we observe that for $\mathit{string}\in\{\text{prevtime},\text{prevpos},\text{pos},\text{time-apv},\text{written}\}$ and natural numbers $i$ as well as for $(v,x)\in V\times V$ the truth value of the variable $X^{\mathit{string}}_{i}$ in the point $(v,x)$ does not depend on $v$. Hence, all these variables are persistent. So,

[TABLE]

Similarly, for $\mathit{string}\in\{\mathrm{time},\mathrm{pos},\mathrm{state},\mathrm{read},\mathrm{prevpos},\mathrm{written}\}$ and natural numbers $i$ as well as for $(v,x)\in V\times V$ the truth value of the variable $A^{\mathit{string}}_{i}$ in the point $(v,x)$ does not depend on $x$. Note that for $v\in V$ the set

[TABLE]

is the $\stackrel{{\scriptstyle L}}{{\to}}$-equivalence class of $(v,v)$. All of the vectors of shared variables have the expected values: for $v\in V$ and $s\in\mathrm{Cloud}(v)$. We see

[TABLE]

and for $v\in V\setminus\{\mathit{root}\}$ and $s\in\mathrm{Cloud}(v)$ we see

[TABLE]

Similarly, for the vectors of persistent variables we see, for $v,x\in V$:

[TABLE]

It is straightforward to check that for all $(v,x)\in W$

[TABLE]

(in fact, in order to achieve $(\mathit{root},x)\models\mathrm{unique}(\underline{\alpha}^{\mathrm{written}})$ we made a somewhat arbitrary choice for the value of $A^{\mathrm{written}}_{\eta}$ in $(\mathit{root},x)$, for $x\in V$ and $\eta\in\Gamma$). Hence, we have

[TABLE]

It is clear as well that

[TABLE]

As none of the nodes in the accepting tree $T$ is labeled with a configuration with the state $q_{\mathrm{reject}}$ we have $(v,x)\models\mathit{no\_reject}$, for all $(v,x)\in W$, hence

[TABLE]

We still need to show that

[TABLE]

It is sufficient to show that, for all $(v,x)\in W$,

[TABLE]

First, let us consider the formula $\mathit{initial\_symbols}$. We wish to show that

[TABLE]

for all $(v,x)\in W$. Nothing needs to be shown if $(v,x)\models(\underline{X}^{\text{time-apv}}=\mathrm{bin}_{N}(0))$ is not true. So, let us assume that $(v,x)\models(\underline{X}^{\text{time-apv}}=\mathrm{bin}_{N}(0))$. We noted above that the assumption $(v,x)\models(\underline{X}^{\text{time-apv}}=\mathrm{bin}_{N}(0))$ implies that the cell $\mathit{pos}(x)$ has not been visited before on the computation path from $\mathit{root}$ to $x$. Hence, $\mathit{read}(x)=\eta$, where $\eta$ is the initial symbol in the cell $x$. We obtain $(v,x)\models X^{\mathrm{read}}_{\eta}$. So, if the number $i:=\mathit{pos}(x)-(2^{N}-1)$ satisfies $1\leq i\leq n$ then $(v,x)\models X^{\mathrm{read}}_{w_{i}}$, otherwise $(v,x)\models X^{\mathrm{read}}_{\#}$. Remember that $(v,x)\models(\underline{X}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(\mathit{pos}(x))$. We have shown $(v,x)\models\mathit{initial\_symbols}$.

Next, we consider the formula $\mathit{written\_symbols}$ and show that

[TABLE]

for all $(v,x)\in W$. Let us assume

[TABLE]

(otherwise, nothing needs to be shown). The condition $(v,x)\models(\underline{X}^{\text{time-apv}}>\mathrm{bin}_{N}(0))$ implies $x\in V\setminus\{\mathit{root}\}$ and that the binary value $t$ of the vector $\underline{X}^{\text{time-apv}}$ in the point $(v,x)$ is equal to $1+$ the time of the previous visit of the cell $\mathit{pos}(x)$ on the computation path from $\mathit{root}$ to $x$. Note that $t\leq\mathit{time}(x)$. The condition $(v,x)\models(\underline{X}^{\text{time-apv}}=\underline{\alpha}^{\mathrm{time}})$ means $t=\mathit{time}(v)$. Now the condition $(v,x)\models B^{\mathrm{active}}$ implies that $v$ is an element of the path from $\mathit{root}$ to $x$. Actually, due to $t=\mathit{time}(v)$ the node $v$ is exactly the computation node on the computation path from $\mathit{root}$ to $x$ after the previous visit of the cell $\mathit{pos}(x)$. Thus, the symbol written during this visit and described by the value of $\underline{\alpha}^{\mathrm{written}}$ at the point $(v,x)$ is just the symbol still contained in the same cell when the computation node $x$ is reached. Hence, we have $(v,x)\models(\underline{X}^{\mathrm{read}}=\underline{\alpha}^{\mathrm{written}})$. For later purposes we note that for the same reason we have $(v,x)\models(\underline{X}^{\mathrm{pos}}=\underline{\alpha}^{\mathrm{prevpos}})$ as well. We have shown $(v,x)\models\mathit{written\_symbols}$.

Next, we consider the formula $\mathit{read\_a\_symbol}$. We wish to show that

[TABLE]

for all $(v,x)\in W$. We show this separately for the five subformulas of $\mathit{read\_a\_symbol}$. First, we show

[TABLE]

that is,

[TABLE]

Indeed, it is clear that $(v,x)\stackrel{{\scriptstyle L}}{{\to}}(v,v)$ and that $(v,v)\models(\underline{X}^{\mathrm{pos}}=\underline{\alpha}^{\mathrm{pos}})$ and $(v,v)\models B^{\mathrm{active}}$. Furthermore, the binary value of $\underline{X}^{\text{time-apv}}$ in the point $(v,v)$ is either $1+$ the time of the previous visit of the cell $\mathit{pos}(v)$ on the path from $\mathit{root}$ to $v$, if this cell has been visited before $v$ on this path, or [math], otherwise. In any case we obtain $(v,v)\models(\underline{X}^{\text{time-apv}}\leq\underline{\alpha}^{\mathrm{time}})$. Next, we show

[TABLE]

that is,

[TABLE]

Actually, we have seen this already in the proof of $(v,x)\models\mathit{written\_symbols}$ above. Next, we show

[TABLE]

that is,

[TABLE]

For the sake of a contradiction, let us assume $(v,x)\models((\underline{X}^{\mathrm{pos}}=\underline{\alpha}^{\mathrm{prevpos}})\wedge(\underline{X}^{\text{time-apv}}<\underline{\alpha}^{\mathrm{time}}))$ and $(v,x)\models B^{\mathrm{active}}$. Then $v$ is a node on the path from $\mathit{root}$ to $x$. Due to $(v,x)\models(\underline{X}^{\text{time-apv}}<\underline{\alpha}^{\mathrm{time}})$ we have $\mathit{time}(v)>0$. And due to $(v,x)\models(\underline{X}^{\mathrm{pos}}=\underline{\alpha}^{\mathrm{prevpos}})$ the node $v$ must have the property $\mathit{pos}(\mathit{pred}(v))=\mathit{pos}(x)$. That means that the cell $\mathit{pos}(x)$ has been visited before $x$ on the path from $\mathit{root}$ to $x$. But under these circumstances, the binary value $t$ of $\underline{X}^{\text{time-apv}}$ at the point $(v,x)$ is equal to $\mathit{time}(u)$ where $u$ is the last node on the path from $\mathit{root}$ to $x$ with the property $\mathit{pos}(\mathit{pred}(u))=\mathit{pos}(x)$. Note that $v$ is a node on the path from $\mathit{root}$ to $x$ with the property $\mathit{pos}(\mathit{pred}(u))=\mathit{pos}(x)$. On the other hand, the condition $(v,x)\models(\underline{X}^{\text{time-apv}}<\underline{\alpha}^{\mathrm{time}})$ implies $t<\mathit{time}(v)$. That is a contradiction. We have shown $(v,x)\models\mathit{becoming\_inactive}$. Next,we show

[TABLE]

that is,

[TABLE]

This is clear from the definition of $\sigma(B^{\mathrm{active}})$.

We come to the last subformula of $\mathit{read\_a\_symbol}$ and show

[TABLE]

that is,

[TABLE]

The condition $(v,x)\models B^{\mathrm{active}}$ implies that $v$ is a node on the path from $\mathit{root}$ to $x$. The condition $(v,x)\models(\underline{X}^{\mathrm{pos}}=\underline{\alpha}^{\mathrm{pos}})$ says that $\mathit{pos}(x)=\mathit{pos}(v)$. We claim that $v=x$. Once we have shown this, of course, we obtain $(v,x)\models(\underline{\alpha}^{\mathrm{read}}=\underline{X}^{\mathrm{read}})$. For the sake of a contradiction, let us assume $v\neq x$. Then the cell $\mathit{pos}(x)$ has been visited before $x$ on the path from $\mathit{root}$ to $x$. Let $u$ be the last node before $x$ on the path from $\mathit{root}$ to $x$ with $\mathit{pos}(u)=\mathit{pos}(x)$. We obtain $\mathit{time}(v)\leq\mathit{time}(u)$. For the binary value $t$ of $\underline{X}^{\text{time-apv}}$ in $(v,x)$ we obtain $t=1+\mathit{time}(u)$. Finally, the condition $(v,x)\models(\underline{X}^{\text{time-apv}}\leq\underline{\alpha}^{\mathrm{time}})$ implies $t\leq\mathit{time}(v)$. By putting all this together we arrive at the following contradiction:

[TABLE]

We have shown $(v,x)\models\mathit{storing\_the\_read\_symbol}$.

Finally, we have to show that

[TABLE]

for all $(v,x)\in W$. We will separately treat the conjunctions over the set $(q,\eta)\in Q_{\exists}\times\Gamma$ and over the set $Q_{\forall}\times\Gamma$. Let us first fix a pair $(q,\eta)\in Q_{\exists}\times\Gamma$ and let us assume that $(v,x)\in W$ is a point with $(v,x)\models(\alpha^{\mathrm{state}}_{q}\wedge\alpha^{\mathrm{read}}_{\eta})$. We have to show that there is an element $(r,\theta,\mathit{left})\in\delta(q,\eta)$ such that $(v,x)\models\mathit{compstep}_{\mathrm{left}}(r,\theta)$ or that there is an element $(r,\theta,\mathit{right})\in\delta(q,\eta)$ such that $(v,x)\models\mathit{compstep}_{\mathrm{right}}(r,\theta)$. As $T$ is an accepting tree and the state $q$ of $c(v)$ is an element of $Q_{\exists}$, the node $v$ is an inner node of $T$, hence, it has a successor $v^{\prime}$. Let us assume that $((q,\eta),(r,\theta,\mathit{left}))\in\delta$ is the element of the transition relation $\delta$ that leads from $v$ to $v^{\prime}$ (the case that this element is of the form $((q,\eta),(r,\theta,\mathit{right}))$ is treated analogously). We claim that then

[TABLE]

In fact, we observe $(v,x)\stackrel{{\scriptstyle L}}{{\to}}(v,v^{\prime})$ and $(v,v^{\prime})\stackrel{{\scriptstyle\Diamond}}{{\to}}(v^{\prime},v^{\prime})$. We claim that the two points $(v,v^{\prime})$ and $(v^{\prime},v^{\prime})$ have the properties formulated in the formula $\mathit{compstep}_{\mathrm{left}}(r,\theta)$. Let us check this. Let us assume that, for some $k\in\{0,\ldots,N-1\}$ and for some $l\in\{0,\ldots,N\}$,

[TABLE]

The number $i:=\mathit{time}(v)$ is an element of $\{0,\ldots,2^{N}-2\}$ because $v$ is an inner point of the tree $T$ and the length of any computation path is at most $2^{N}-1$. The number $j:=\mathit{pos}(v)$ is an element of $\{1,\ldots,2^{N+1}-3\}$ because the computation starts in cell $2^{N}-1$ and during each computation step the tape head can move at most one step to the left or to the right. We obtain $k=\min(\{0,\ldots,N-1\}\setminus\mathrm{Ones}(i))$ and $l=\min\mathrm{Ones}(j)$. As $v=\mathit{pred}(v^{\prime})$ we obtain

[TABLE]

and

[TABLE]

And as $\mathit{time}(v^{\prime})=\mathit{time}(v)+1=i+1$ and $\mathit{pos}(v^{\prime})=\mathit{pos}(v)-1=j-1$ we conclude that

[TABLE]

Finally, the condition

[TABLE]

is obviously satisfied and the condition

[TABLE]

follows from the fact that $((q,\eta),(r,\theta,\mathit{left}))\in\delta$ is the element of the transition relation $\delta$ that leads from $v$ to $v^{\prime}$. This ends the treatment of the conjunctions over the set $(q,\eta)\in Q_{\exists}\times\Gamma$ in the formula $\mathit{computation}$. Let us now consider a pair $(q,\eta)\in Q_{\forall}\times\Gamma$. Let us assume that $(v,x)\in W$ is a point such that $(v,x)\models(\alpha^{\mathrm{state}}_{q}\wedge\alpha^{\mathrm{read}}_{\eta})$. We have to show that for all elements $(r,\theta,\mathit{left})\in\delta(q,\eta)$ we have $(v,x)\models\mathit{compstep}_{\mathrm{left}}(r,\theta)$ and for all elements $(r,\theta,\mathit{right})\in\delta(q,\eta)$ we have $(v,x)\models\mathit{compstep}_{\mathrm{right}}(r,\theta)$. Let us consider an arbitrary element $(r,\theta,\mathit{left})\in\delta(q,\eta)$ (the case of an element $(r,\theta,\mathit{right})\in\delta(q,\eta)$ is treated analogously). As $q\in Q_{\forall}$ and $T$ is an accepting tree, in $T$ there is a successor $v^{\prime}$ of $v$ such that the element $((q,\eta),(r,\theta,\mathit{left}))$ leads from $v$ to $v^{\prime}$. Above, we have already seen that this implies

[TABLE]

Thus, we have shown $(v,x)\models\mathit{computation}$ for all $(v,x)\in W$. This ends the proof of the claim that in the $\mathrm{S4\times S5}$-product model $(W_{1}\times W_{2},\stackrel{{\scriptstyle\Diamond}}{{\to}},\stackrel{{\scriptstyle L}}{{\to}},\sigma)$ that we constructed for $w\in L$ we have $(\mathit{root},\mathit{root})\models f_{\mathrm{S4\times S5}}(w)$.

A.5 Existence of an Accepting Tree

We come to the other direction. Let $w\in\Sigma^{*}$. We wish to show that if $f_{\mathrm{S4\times S5}}(w)$ is $\mathrm{S4\times S5}$-satisfiable then $w\in L$. We will show that any $\mathrm{S4\times S5}$-product model essentially contains an accepting tree of the Alternating Turing Machine $M$ on input $w$. Of course, this implies $w\in L$.

Let us sketch the main idea. We will consider an $\mathrm{S4\times S5}$-product model of $f_{\mathrm{S4\times S5}}(w)$. And we will consider partial trees of $M$ on input $w$ as considered in Subsection 3.3, for any $w\in\Sigma^{*}$. First, we will show that a certain very simple partial tree of $M$ on input $w$ “can be mapped to” the model (later we will give a precise meaning to “can be mapped to”). Then we will show that any partial tree of $M$ on input $w$ that can be mapped to the model and that is not an accepting tree of $M$ on input $w$ can be properly extended to a strictly larger partial tree of $M$ on input $w$ that can be mapped to the model as well. If there would not exist an accepting tree of $M$ on input $w$ then we would obtain an infinite strictly increasing sequence of partial trees of $M$ on input $w$. But we show that this cannot happen by giving a finite upper bound on the size of partial trees of $M$ on input $w$.

Let $w\in\Sigma^{*}$ be a string such that the formula $f_{\mathrm{S4\times S5}}(w)$ is $\mathrm{S4\times S5}$-satisfiable. We set $n:=|w|$. Let $(W_{1},R_{\Diamond})$ be an $S4$-frame, let $(W_{2},R_{L})$ be an $S5$-frame, let $\sigma:AT\to\mathcal{P}(W_{1}\times W_{2})$ be a function such that the quadruple $(W_{1}\times W_{2},\stackrel{{\scriptstyle\Diamond}}{{\to}},\stackrel{{\scriptstyle L}}{{\to}},\sigma)$ where $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ and $\stackrel{{\scriptstyle L}}{{\to}}$ are defined as in [8, Definition 2.3] is an $\mathrm{S4\times S5}$-product model, and let $(r_{1},r_{2})\in W_{1}\times W_{2}$ be a point with $(r_{1},r_{2})\models f_{\mathrm{S4\times S5}}(w)$. The quintuple

[TABLE]

will be important in the following. We claim that we can assume without loss of generality that $r_{1}\stackrel{{\scriptstyle\Diamond}}{{\to}}x$ for all $x\in W_{1}$ and $R_{L}=W_{2}\times W_{2}$. Otherwise, instead of $W_{1}$ we could consider the set $W_{1}^{\prime}:=\{v\in W_{1}\mid r_{1}\stackrel{{\scriptstyle\Diamond}}{{\to}}v\}$ and instead of $W_{2}$ we could consider the set $W_{2}^{\prime}:=$ the $R_{L}$-equivalence class of $r_{2}$ and the restrictions $\stackrel{{\scriptstyle L}}{{\to}}^{\prime}$ resp. $\stackrel{{\scriptstyle\Diamond}}{{\to}}^{\prime}$ of $\stackrel{{\scriptstyle L}}{{\to}}$ resp. $\stackrel{{\scriptstyle\Diamond}}{{\to}}$ to $W_{1}^{\prime}\times W_{2}^{\prime}$. By structural induction one shows that for any bimodal formula $\varphi$ and for any $(v,x)\in W_{1}^{\prime}\times W_{2}^{\prime}$,

[TABLE]

So, we shall assume that $r_{1}\stackrel{{\scriptstyle\Diamond}}{{\to}}x$, for all $v\in W_{1}$, and $R_{L}=W_{2}\times W_{2}$. Note that this implies that if $\varphi$ is a formula with $(r_{1},r_{2})\models K\Box\varphi$ then, for all $(v,x)\in W_{1}\times W_{2}$, we have $(v,x)\models\varphi$.

For every $v\in W_{1}$, the set

[TABLE]

is the $\stackrel{{\scriptstyle L}}{{\to}}$-equivalence class (short: cloud) of any element $y\in W_{1}\times W_{2}$ whose first component is $v$. Remember that for every $\stackrel{{\scriptstyle L}}{{\to}}$-equivalence class and every shared variable $\alpha^{\mathit{string}}_{i}$ for $\mathit{string}\in\{\mathrm{time},\mathrm{pos},\mathrm{state},\mathrm{read},\mathrm{prevpos},\mathrm{written}\}$ and natural numbers $i$, the truth value of this shared variable is the same in all elements of the $\stackrel{{\scriptstyle L}}{{\to}}$-equivalence class.

Partial trees of $M$ on input $w$ as introduced in Subsection 3.3 will play an important role in the following. We will write a partial tree of $M$ on input $w$ similarly as in Subsection 3.3 as a triple $T=(V,E,c)$, but with the difference that we will describe configurations as at the beginning of Subsection A.2: the labeling function $c$ will be a function of the form $c:V\to Q\times\{0,\ldots,2^{N+1}-2\}\times\Gamma^{2^{N+1}-1}$. If $T=(V,E,c)$ is a partial tree of $M$ on input $w$ with root $\mathit{root}$ then a function $\pi:V\to W_{1}$ is called a morphism from $T$ to $\mathit{Model}$ if it satisfies the following four conditions:

$\pi(\mathit{root})=r_{1}$. 2. 2.

$\{(\pi(v),\pi(v^{\prime}))~{}:~{}v,v^{\prime}\in V\text{ and }vEv^{\prime}\}\subseteq R_{\Diamond}$. 3. 3.

\begin{array}[t]{l}(\forall v\in V\setminus\{\mathit{root}\})\,(\exists x\in W_{2})\\ (\pi(v),x)\models\bigl{(}(\underline{\alpha}^{\mathrm{prevpos}}=\mathrm{bin}_{N+1}(\mathit{pos}(\mathit{pred}(v))))\wedge\alpha^{\mathrm{written}}_{\mathit{written}(v)}\bigr{)}\end{array}. 4. 4.

\begin{array}[t]{l}(\forall v\in V)\,(\exists x\in W_{2})\\ (\pi(v),x)\models\bigl{(}(\underline{\alpha}^{\mathrm{time}}=\mathrm{bin}_{N}(\mathit{time}(v)))\wedge(\underline{\alpha}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(\mathit{pos}(v)))\\ \qquad\qquad\qquad\wedge\alpha^{\mathrm{state}}_{\mathit{state}(v)}\wedge\alpha^{\mathrm{read}}_{\mathit{read}(v)}\bigr{)}.\end{array}

We say that $T$ can be mapped to $\mathit{Model}$ if there exists a morphism from $T$ to $\mathit{Model}$. Below we shall prove the following lemma.

Lemma A.3**.**

If a partial tree $T=(V,E,c)$ of $M$ on input $w$ can be mapped to $\mathit{Model}$ and is not an accepting tree of $M$ on input $w$ then there exists a partial tree $T=(\widetilde{V},\widetilde{E},\widetilde{c})$ of $M$ on input $w$ that can be mapped to $\mathit{Model}$ and that satisfies $V\subsetneq\widetilde{V}$.

Before we prove this lemma, we deduce the desired assertion from it. Let

[TABLE]

Then, due to Condition III in the definition of a “partial tree of $M$ on input $w$”, any node in any partial tree of $M$ on input $w$ has at most $D$ successors. As any computation of $M$ on input $w$ stops after at most $2^{N}-1$ steps, any partial tree of $M$ on input $w$ has at most

[TABLE]

nodes.

We claim that the rooted and labeled tree

[TABLE]

is a partial tree of $M$ on input $w$ and that it can be mapped to $\mathit{Model}$. Indeed, Condition I in the definition of a “partial tree of $M$ on input $w$” is satisfied because the node $\mathit{root}$ is labeled with the initial configuration of $M$ on input $w$. Conditions II, III, and IV are satisfied because $T_{0}$ does not have any inner nodes. Condition $\mathrm{V}^{\prime}$ is satisfied because $\mathit{state}(\mathit{root})=q_{0}$ and, due to $(r_{1},r_{2})\models\alpha^{\mathrm{state}}_{q_{0}}$ (this is a part of $(r_{1},r_{2})\models\mathit{start}$) and $(r_{1},r_{2})\models\neg\alpha^{\mathrm{state}}_{q_{\mathrm{reject}}}$ (this follows from $(r_{1},r_{2})\models K\Box\mathit{no\_reject}$) we obtain $q_{0}\neq q_{\mathrm{reject}}$. Thus, $T_{0}$ is indeed a partial tree of $M$ on input $w$. Now we show that $T_{0}$ can be mapped to $\mathit{Model}$. Of course, we define the function $\pi:\{\mathit{root}\}\to W_{1}$ by $\pi(\mathit{root}):=r_{1}$.

The condition $\pi(\mathit{root})=r_{1}$ is true by definition. 2. 2.

The tree $T_{0}$ does not have any edges, that is, its set $E$ of edges is empty. So, the second condition is satisfied. 3. 3.

The third condition does not apply to the tree $T_{0}$ because $T_{0}$ has only one node, its root. 4. 4.

On the one hand, we have

[TABLE]

[TABLE]

On the other hand, the condition $(r_{1},r_{2})\models\mathit{start}$ says

[TABLE]

We still wish to show $(r_{1},r_{2})\models\alpha^{\mathrm{read}}_{\#}$. We have $(r_{1},r_{2})\models\mathit{read\_a\_symbol}$. This implies $(r_{1},r_{2})\models\mathit{existence\_of\_a\_reading\_point}$, and this implies that there exists some $y\in W_{2}$ with

[TABLE]

hence, with

[TABLE]

Now $(r_{1},y)\models\mathit{initial\_symbols}$ implies $(r_{1},y)\models X^{\mathrm{read}}_{\#}$. Finally, the condition

[TABLE]

implies $(r_{1},y)\models\alpha^{\mathrm{read}}_{\#}$, and this implies $(r_{1},r_{2})\models\alpha^{\mathrm{read}}_{\#}$.

If there would not exist an accepting tree of $M$ on input $w$ then, starting with $T_{0}$ and using Lemma A.3, we could construct an infinite sequence of partial trees $T_{0},T_{1},T_{2},\ldots$ of $M$ on input $w$ that can be mapped to $\mathit{Model}$ such that the number of nodes in these trees is strictly increasing. But we have seen that any partial tree of $M$ input $w$ can have at most $\widetilde{D}$ nodes. Thus, there exists an accepting tree of $M$ on input $w$. We have shown $w\in L$.

In order to complete the proof of Theorem A.1 it remains to prove Lemma A.3.

Proof of Lemma A.3.

Let $T=(V,E,c)$ be a partial tree of $M$ on input $w$ that is not an accepting tree of $M$ on input $w$ and that can be mapped to $\mathit{Model}$. Then $T$ has a leaf $\widehat{v}$ such that the state $q:=\mathit{state}(\widehat{v})$ is either an element of $Q_{\exists}$ or of $Q_{\forall}$. First we treat the case that it is an element of $Q_{\exists}$, then the case that it is an element of $Q_{\forall}$. Let $\pi:V\to W_{1}$ be a morphism from $T$ to $\mathit{Model}$.

So, let us assume that $q\in Q_{\exists}$. We define $\eta:=\mathit{read}(\widehat{v})$. As $\pi:V\to W_{1}$ is a morphism from $T$ to $\mathit{Model}$ there exists an $x^{\prime}\in W_{2}$ with

[TABLE]

Hence, due to $(\pi(\widehat{v}),x^{\prime})\models\mathit{computation}$,

[TABLE]

Let us assume there is an element $(r,\theta,\mathit{left})\in\delta(q,\eta)$ such that $(\pi(\widehat{v}),x^{\prime})\models\mathit{compstep}_{\mathrm{left}}(r,\theta)$ (the other case, the case when there is an element $(r,\theta,\mathit{right})\in\delta(q,\eta)$ such that $(\pi(\widehat{v}),x^{\prime})\models\mathit{compstep}_{\mathrm{right}}(r,\theta)$, is treated analogously). We claim that we can define the new tree $\widetilde{T}=(\widetilde{V},\widetilde{E},\widetilde{c})$ as follows:

• •

$\widetilde{V}:=V\cup\{\widetilde{v}\}$ where $\widetilde{v}$ is a new element (not in $V$),

• •

$\widetilde{E}:=E\cup\{(\widehat{v},\widetilde{v})\}$,

• •

\widetilde{c}(x):=\begin{cases}c(x)&\text{for all }x\in V,\\ c^{\prime}&\text{for }x=\widetilde{v},\text{ where c^{\prime}$is the configuration that is reached from$c(\widehat{v})}\\ &\text{in the computation step given by }((q,\eta),(r,\theta,\mathit{left}))\in\delta.\end{cases}

We have to show that $\widetilde{T}$ is a partial tree of $M$ on input $w$. Condition I in the definition of “a partial tree of $M$ on input $w$” is satisfied because $\widetilde{T}$ has the same root as $T$, and the label of the root does not change. A node in $\widetilde{T}$ is an internal node of $\widetilde{T}$ if, and only if, it is either an internal node of $T$ or equal to $\widehat{v}$. For internal nodes of $T$ Conditions II, III, and IV are satisfied by assumption (and due to the fact that the labels of nodes in $V$ do not change when moving from $T$ to $\widetilde{T}$). The new internal node $\widehat{v}$ satisfies Condition II by our definition of $\widetilde{c}(\widetilde{v})$. Condition III is satisfied for $\widehat{v}$ because $\widehat{v}$ has exactly one successor. And Condition IV does not apply to $\widehat{v}$ because $\widehat{v}\in Q_{\exists}$. A node in $\widetilde{T}$ is a leaf if, and only if, it is either equal to $\widetilde{v}$ or a leaf in $T$ different from $\widehat{v}$. For the leaves in $T$ different from $\widehat{v}$ Condition $\mathrm{V}^{\prime}$ is satisfied by assumption (and due to the fact that the labels of nodes in $V$ do not change). Finally, we have to show that Condition $\mathrm{V}^{\prime}$ is satisfied for the new leaf $\widetilde{v}$ in $\widetilde{T}$ as well. We postpone this until after the definition of a morphism from $\widetilde{T}$ to $\mathit{Model}$.

We also have to show that $\widetilde{T}$ can be mapped to $\mathit{Model}$. Let us define a function $\widetilde{\pi}:\widetilde{V}\to W_{1}$ that we will show to be a morphism from $\widetilde{T}$ to $\mathit{Model}$. As $\widehat{v}$ is an element of a partial tree of $M$ on input $w$ with $\mathit{state}(\widehat{v})\in Q_{\exists}$, at least one more computation step can be done. As any computation of $M$ on input $w$ stops after at most $2^{N}-1$ steps, we observe that the number $i:=\mathit{time}(\widehat{v})$ satisfies $0\leq i<2^{N}-1$. Then $\{0,\ldots,N-1\}\setminus\mathrm{Ones}(i)\neq\emptyset$. We set $k:=\min(\{0,\ldots,N-1\}\setminus\mathrm{Ones}(i))$. Together with $(\pi(\widehat{v}),x^{\prime})\models(\underline{\alpha}^{\mathrm{time}}=\mathrm{bin}_{N}(i))$ we conclude $(\pi(\widehat{v}),x^{\prime})\models\mathrm{rightmost\_zero}(\underline{\alpha}^{\mathrm{time}},k)$. As during each computation step, the tape head can move at most one step to the left or to the right and as the computation started in position $2^{N}-1$ the number $j:=\mathit{pos}(\widehat{v})$ satisfies $0<j\leq 2^{N+1}-3$. Then $\mathrm{Ones}(j)\neq\emptyset$. We set $l:=\min\mathrm{Ones}(j)$. Together with $(\pi(\widehat{v}),x^{\prime})\models(\underline{\alpha}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(j))$ we conclude $(\pi(\widehat{v}),x^{\prime})\models\mathrm{rightmost\_one}(\underline{\alpha}^{\mathrm{pos}},l)$. Thus, we have

[TABLE]

Due to $(\pi(\widehat{v}),x^{\prime})\models\mathit{compstep}_{\mathrm{left}}(r,\theta)$ there exist an element $y\in W_{2}$ and an element $x\in W_{1}$ such that $\pi(\widehat{v})R_{\Diamond}x$ as well as

[TABLE]

and

[TABLE]

We claim that we can define the desired function $\widetilde{\pi}:\widetilde{V}\to W_{1}$ by

[TABLE]

Before we show that $\widetilde{\pi}$ is a morphism from $\widetilde{T}$ to $\mathit{Model}$, let us complete the proof that $\widetilde{T}$ is a partial tree of $M$ on input $w$. We still need to show that Condition $\mathrm{V}^{\prime}$ is satisfied for the new leaf $\widetilde{v}$ in $\widetilde{T}$ as well. It is sufficient to show that the state $r$ of the configuration $c^{\prime}$ is not the rejecting state $q_{\mathrm{reject}}$. But this follows from $(x,y)\models\alpha^{\mathrm{state}}_{r}$ and $(x,y)\models\neg\alpha^{\mathrm{state}}_{q_{\mathrm{reject}}}$ (this follows from $(r_{1},r_{2})\models K\Box\mathit{no\_reject}$). We have shown that $\widetilde{T}$ is a partial tree of $M$ on input $w$.

Now we show that $\widetilde{\pi}$ is a morphism from $\widetilde{T}$ to $\mathit{Model}$. The first condition in the definition of a “morphism from $\widetilde{T}$ to $\mathit{Model}$” is satisfied because $\widetilde{\pi}(\mathit{root})=\pi(\mathit{root})=r_{1}$. For the second condition let us consider $v,v^{\prime}\in\widetilde{V}$ with $v\widetilde{E}v^{\prime}$. We have to show $\pi(v)R_{\Diamond}\pi(v^{\prime})$. There are two possible cases.

• •

In the case $v,v^{\prime}\in V$ we have $vEv^{\prime}$ and, hence, $\pi(v)R_{\Diamond}\pi(v^{\prime})$. As $\widetilde{\pi}(v)=\pi(v)$ and $\widetilde{\pi}(v^{\prime})=\pi(v^{\prime})$ we obtain $\widetilde{\pi}(v)R_{\Diamond}\widetilde{\pi}(v^{\prime})$.

• •

The other possible case is $v=\widehat{v}$ and $v^{\prime}=\widetilde{v}$. But we know $\widetilde{\pi}(\widehat{v})=\pi(\widehat{v})$, $\widetilde{\pi}(\widetilde{v})=x$, and $\pi(\widehat{v})R_{\Diamond}x$.

Next, we verify that the third condition in the definition of a “morphism from $\widetilde{T}$ to $\mathit{Model}$” is satisfied. For $v\in V\setminus\{\mathit{root}\}$ it is satisfied by assumption (and by $\widetilde{\pi}(v)=\pi(v)$ and $\widetilde{c}(v)=c(v)$). For $\widetilde{v}$ it is sufficient to show that

[TABLE]

(remember that $\widetilde{\pi}(\widetilde{v})=x$). These are really two conditions. We prove them separately.

• •

In the tree $\widetilde{T}$ we have $\mathit{pos}(\mathit{pred}(\widetilde{v}))=\mathit{pos}(\widehat{v})=j$, and in $T$ we have $\mathit{pos}(\widehat{v})=j$ as well. The assumption $(\pi(\widehat{v}),x^{\prime})\models(\underline{\alpha}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(j))$, for some $x^{\prime}\in W_{2}$, implies $(\pi(\widehat{v}),y)\models(\underline{\alpha}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(j))$, and the conditions $(\pi(\widehat{v}),y)\models(\underline{X}^{\mathrm{prevpos}}=\underline{\alpha}^{\mathrm{pos}})$ and $(x,y)\models(\underline{\alpha}^{\mathrm{prevpos}}=\underline{X}^{\mathrm{prevpos}})$ as well as the persistence of $\underline{X}^{\mathrm{prevpos}}$ imply $(x,y)\models(\underline{\alpha}^{\mathrm{prevpos}}=\mathrm{bin}_{N+1}(j))$.

• •

In $\widetilde{T}$ we have $\mathit{written}(\widetilde{v})=\theta$. And we have $(x,y)\models\alpha^{\mathrm{written}}_{\theta}$, hence, $(x,y)\models\alpha^{\mathrm{written}}_{\mathit{written}(\widetilde{v})}$.

We come to the fourth condition in the definition of a “morphism from $\widetilde{T}$ to $\mathit{Model}$”. It is satisfied for $v\in V$ by assumption (and due to $\widetilde{\pi}(v)=\pi(v)$ and $\widetilde{c}(v)=c(v)$). We still need to show that it is satisfied for $v=\widetilde{v}$. Remember $\widetilde{\pi}(\widetilde{v})=x$. It is sufficient to show

[TABLE]

This assertion consists really of four assertions. We treat them one by one.

• •

In the trees $T$ and $\widetilde{T}$ we have $\mathit{time}(\widehat{v})=i$, and in the tree $\widetilde{T}$ we have $\mathit{time}(\widetilde{v})=i+1$. We have already seen that $(\pi(\widehat{v}),x^{\prime})\models(\underline{\alpha}^{\mathrm{time}}=\mathrm{bin}_{N}(i))$ and that $(\pi(\widehat{v}),x^{\prime})\models\mathrm{rightmost\_zero}(\underline{\alpha}^{\mathrm{time}},k)$. Of course, we get

[TABLE]

The conditions

[TABLE]

and the persistence of $\underline{X}^{\mathrm{prevtime}}$ imply $(x,y)\models(\underline{\alpha}^{\mathrm{time}}=\mathrm{bin}_{N}(i+1))$.

• •

In the trees $T$ and $\widetilde{T}$ we have $\mathit{pos}(\widehat{v})=j$, and in the tree $\widetilde{T}$ we have $\mathit{pos}(\widetilde{v})=j-1$. We have already seen $(\pi(\widehat{v}),x^{\prime})\models(\underline{\alpha}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(j))$, and $(\pi(\widehat{v}),x^{\prime})\models\mathit{rightmost\_one}(\underline{\alpha}^{\mathrm{pos}},l)$. Of course, we get

[TABLE]

The conditions

[TABLE]

and the persistence of $\underline{X}^{\mathrm{prevpos}}$ imply $(x,y)\models(\underline{\alpha}^{\mathrm{pos}}=\mathrm{bin}_{N+1}(j-1))$.

• •

We have $\mathit{state}(\widetilde{v})=r$. And we have $(x,y)\models\alpha^{\mathit{state}}_{r}$.

• •

Let $\gamma:=\mathit{read}(\widetilde{v})$ in $\widetilde{T}$. We wish to show $(x,y)\models\alpha^{\mathrm{read}}_{\gamma}$. We remark that the proof is a formal version of the informal explanation after the definition of the formula $\mathit{read\_a\_symbol}$. It is sufficient to show that there is some $z\in W_{2}$ with $(x,z)\models\alpha^{\mathrm{read}}_{\gamma}$. The condition $(x,y)\models\mathit{existence\_of\_a\_reading\_point}$ implies that there exists some $z\in W_{2}$ such that

[TABLE]

Remember that the binary value of $\underline{\alpha}^{\mathrm{time}}$ in $(x,y)$ and, hence, also in $(x,z)$, is equal to $i+1$ and that the binary value of $\underline{\alpha}^{\mathrm{pos}}$ in $(x,y)$ and, hence, also in $(x,z)$, is equal to $j-1$. Hence, the binary value of $\underline{X}^{\mathrm{pos}}$ in $(x,z)$ is equal to $j-1$. Let $t$ be the unique number in $\{0,\ldots,i+1\}$ with $(x,z)\models(\underline{X}^{\text{time-apv}}={\rm bin}_{N}(t))$. Let $v_{t}$ be the unique node in the computation path in $\widetilde{T}$ from $\mathit{root}$ to $\widetilde{v}$ with $\mathit{time}(v_{t})=t$.

First, we claim that $(\widetilde{\pi}(u),z)\models B^{\mathrm{active}}$ for all nodes $u$ on the path from $\mathit{root}$ to $\widetilde{v}$. Any such $u$ satisfies $uE^{*}\widetilde{v}$. We obtain $\widetilde{\pi}(u)R_{\Diamond}\widetilde{\pi}(\widetilde{v})$, hence, $\widetilde{\pi}(u)R_{\Diamond}x$. If $(\widetilde{\pi}(u),z)\models\neg B^{\mathrm{active}}$ then due to $(\widetilde{\pi}(u),z)\models\mathit{staying\_inactive}$, we would obtain $(x,z)\models\neg B^{\mathrm{active}}$. But this is a contradiction to the condition $(x,z)\models B^{\mathrm{active}}$ with which we started. Thus, for all nodes on the path from $\mathit{root}$ to $\widetilde{v}$ we have $(\widetilde{\pi}(u),z)\models B^{\mathrm{active}}$.

Can there be a node $u\neq v_{t}$ in the path from $v_{t}$ to $\widetilde{v}$ with $\mathit{pos}(\mathit{pred}(u))=j-1=\mathit{pos}(\widetilde{v})$? We claim that this is not the case. Indeed, if there were such a $u$ then for this node $u$ we would have $(\widetilde{\pi}(u),z)\models(\underline{X}^{\mathrm{pos}}=\underline{\alpha}^{\mathrm{prevpos}})\wedge(\underline{X}^{\text{time-apv}}<\underline{\alpha}^{\mathrm{time}})$. But then $(\widetilde{\pi}(u),z)\models\mathit{becoming\_inactive}$ would imply $(\widetilde{\pi}(u),z)\models\neg B^{\mathrm{active}}$ in contradiction to what we have just shown. Hence, we have shown that there is no node $u\neq v_{t}$ in the path from $v_{t}$ to $\widetilde{v}$ with $\mathit{pos}(\mathit{pred}(u))=j-1=\mathit{pos}(\widetilde{v})$. Let us now distinguish the two cases $t=0$ and $t>0$.

First we treat the case $t=0$. Then $v_{t}=\mathit{root}$. We have just seen that the cell $j-1$ has not been visited before $\widetilde{v}$ on the path from $\mathit{root}$ to $\widetilde{v}$. Hence, the initial symbol in the cell $j-1$ is still the symbol in this cell when the node $\widetilde{v}$ is reached. Thus $\gamma$ is the initial symbol in this cell. Due to $(x,z)\models\mathit{initial\_symbols}$ we obtain $(x,z)\models X^{\mathrm{read}}_{\gamma}$. Due to $(x,z)\models\mathit{storing\_the\_read\_symbol}$ we obtain $(x,z)\models\alpha^{\mathrm{read}}_{\gamma}$.

Finally, we treat the case $t>0$. Then $v_{t}\neq\mathit{root}$. And we have just seen that the cell $j-1$ has not been visited before $\widetilde{v}$ on the path from $\mathit{v_{t}}$ to $\widetilde{v}$. But we claim that it has been visited in the predecessor of $v_{t}$. Indeed, we have (\widetilde{\pi}(v_{t}),z)\models\bigl{(}(\underline{X}^{\text{time-apv}}>\mathrm{bin}_{N}(0))\wedge(\underline{X}^{\text{time-apv}}=\underline{\alpha}^{\mathrm{time}})\wedge B^{\mathrm{active}}\bigr{)}. Hence, due to $(\widetilde{\pi}(v_{t}),z)\models\mathit{time\_of\_previous\_visit}$, we obtain $(\widetilde{\pi}(v_{t}),z)\models(\underline{X}^{\mathrm{pos}}=\underline{\alpha}^{\mathrm{prevpos}})$. Above we have seen that the binary value of $\underline{X}^{\mathrm{pos}}$ in $(x,z)$ is $j-1$. As $\underline{X}^{\mathrm{pos}}$ is persistent, the binary value of $\underline{X}^{\mathrm{pos}}$ in $(\widetilde{\pi}(v_{t}),z)$ is $j-1$ as well. Hence, the binary value of $\underline{\alpha}^{\mathrm{prevpos}}$ in $(\widetilde{\pi}(v_{t}),z)$ is $j-1$ as well. That implies $\mathit{pos}(\mathit{pred}(v_{t}))=j-1$. We have shown that the predecessor of the node $v_{t}$ is the last node before $\widetilde{v}$ in which the cell $j-1=\mathit{pos}(\widetilde{v})$ has been visited. Hence, the symbol $\gamma$ that is read when the node $\widetilde{v}$ is reached, has been written in the computation step from $\mathit{pred}(v_{t})$ to $v_{t}$. Hence, we have $(\widetilde{\pi}(v_{t}),z)\models\alpha^{\mathrm{written}}_{\gamma}$. Due to $(\widetilde{\pi}(v_{t}),z)\models\mathit{written\_symbols}$ we obtain $(\widetilde{\pi}(v_{t}),z)\models X^{\mathrm{written}}_{\gamma}$. As above in the other case, due to $(x,z)\models\mathit{storing\_the\_read\_symbol}$, we finally obtain $(x,z)\models\alpha^{\mathrm{read}}_{\gamma}$.

Thus, $\widetilde{T}$ is not only a partial tree of $M$ on input $w$ but can also be mapped to $\mathit{Model}$. This ends the treatment of the case $q\in Q_{\exists}$.

Now we consider the other case, the case $q\in Q_{\forall}$. We define $\eta:=\mathit{read}(\widehat{v})$. Let

[TABLE]

be the elements of $\delta(q,\eta)$ where $d\geq 1$ and $\mathit{dir}_{m}\in\{\mathit{left},\mathit{right}\}$, for $m=1,\ldots,d$. We claim that we can define the new tree $\widetilde{T}=(\widetilde{V},\widetilde{E},\widetilde{c})$ as follows:

• •

$\widetilde{V}:=V\cup\{\widetilde{v}_{1},\ldots,\widetilde{v}_{d}\}$ where $\widetilde{v}_{1},\ldots,\widetilde{v}_{d}$ are new (not in $V$) pairwise different elements,

• •

$\widetilde{E}:=E\cup\{(\widehat{v},\widetilde{v}_{1}),\ldots,(\widehat{v},\widetilde{v}_{d})\}$,

• •

\widetilde{c}(x):=\begin{cases}c(x)&\text{for all }x\in V,\\ c^{\prime}_{m}&\text{for }x=\widetilde{v}_{m},\text{ where c^{\prime}_{m} is the configuration that is reached from }c(\widehat{v})\\ &\text{in the computation step given by }((q,\eta),(r_{m},\theta_{m},\mathit{dir}_{m}))\in\delta.\end{cases}

Before we show that $\widetilde{T}$ is a partial tree of $M$ on input $w$, we define a function $\widetilde{\pi}:\widetilde{V}\to W_{1}$ that we will show to be a morphism from $\widetilde{T}$ to $\mathit{Model}$. Since $T$ can be mapped to $\mathit{Model}$, we have

[TABLE]

for some $x^{\prime}\in W_{2}$, hence, due to $(\pi(\widehat{v}),x^{\prime})\models\mathit{computation}$,

[TABLE]

As in the case $q\in Q_{\exists}$ one shows that the numbers $i:=\mathit{time}(\widehat{v})$ and $j:=\mathit{pos}(\widehat{v})$ satisfy $0\leq i<2^{N}-1$ and $0<j\leq 2^{N+1}-3$, and one defines

[TABLE]

As in the case $q\in Q_{\exists}$ one obtains

[TABLE]

Let us consider some $m\in\{1\ldots,d\}$. If $\mathit{dir}_{m}=\mathit{left}$ then, due to $(\pi(\widehat{v}),x^{\prime})\models\mathit{compstep}_{\mathrm{left}}(r,\theta)$, there exist an element $y_{m}\in W_{2}$ and an element $x_{m}\in W_{1}$ such that $\pi(\widehat{v})R_{\Diamond}x_{m}$ as well as

[TABLE]

and

[TABLE]

Similarly, if $\mathit{dir}_{m}=\mathit{right}$ then, due to $(\pi(\widehat{v}),x^{\prime})\models\mathit{compstep}_{\mathrm{right}}(r,\theta)$, there exist an element $y_{m}\in W_{2}$ and an element $x_{m}\in W_{1}$ such that $\pi(\widehat{v})R_{\Diamond}x_{m}$ as well as

[TABLE]

and

[TABLE]

We claim that we can define the desired function $\widetilde{\pi}:\widetilde{V}\to W_{1}$ by

[TABLE]

Similarly as in the case $q\in Q_{\exists}$ one shows that $\widetilde{T}$ is a partial tree of $M$ on input $w$. Note that also Condition IV is satisfied for $\widehat{v}$. Finally, similarly as in the case $q\in Q_{\exists}$ one shows that $\widetilde{\pi}$ is a morphism from $\widetilde{T}$ to $\mathit{Model}$. This ends the treatment of the case $q\in Q_{\forall}$. We have proved Lemma A.3. ∎