Pith. sign in

REVIEW 1 major objections 5 minor 33 references

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

T0 review · 1 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The logics K4×S5, S4×S5, and SSL are EXPSPACE-hard under logspace reduction.

desk verdict Genuinely new EXPSPACE lower bounds for three modal logics, with a careful ATM simulation; the only real gap is an omitted standard lemma that the logspace reductions depend on. read the letter →

arxiv 1908.03509 v1 pith:N5DUQHGA submitted 2019-08-09 cs.LO cs.CCmath.LO

Peter Hertling , Gisela Krommes This is my paper · ORCID
classification cs.LOcs.CCmath.LO MSC 03B4568Q1703D15
keywords EXPSPACE-completenessbimodalproductlogicssubsetspacelogicsatisfiabilityproblemalternatingTuringmachineslogspacereductionK4×S5S4×S5
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper proves that the satisfiability problems of the product logics K4×S5 and S4×S5 and of the subset-space logic SSL are EXPSPACE-hard under logspace reduction. Together with the matching upper bound proved in the companion paper, this makes all three satisfiability problems EXPSPACE-complete and resolves the previously open complexity question for the two product logics. The proof reduces any exponential-time alternating Turing machine computation to the satisfiability of an SSL formula by encoding accepting computation trees as equivalence classes, then transfers the lower bound by logspace translations from SSL to S4×S5 and from S4×S5 to K4×S5. Since these logics are used for reasoning about knowledge and about subset spaces, the result gives a precise worst-case space bound for their satisfiability algorithms.

What carries the argument

The load-bearing device is the shared variable: in SSL it is the formula $\alpha_i := \mathsf{L}(A_i \land \Box_L B)$, and in S4×S5 it is the simpler $\alpha_i := \mathsf{L}\,A_i$. A shared variable is constant along $\mathsf{L}$-equivalence classes (the clouds) but can change along the vertical $\lozenge$-direction, while ordinary propositional variables have the opposite persistence; this lets the encoding copy and update bit vectors for time, tape-head position, state, and written symbol. These vectors feed binary-counter formulas that force a staircase of points $p_i \xrightarrow{\mathsf{L}} p'_i \xrightarrow{\lozenge} p_{i+1}$, so any model of the reduction contains an accepting tree of the alternating Turing machine realized as clouds. The later translations between logics work by adding a fresh variable $\mathit{main}$ whose false points act as universal successors, and by forcing reflexivity instances for the modal subformulas involved.

What would settle it

Test the omitted lemma directly: for families of bimodal formulas with deeply nested $\mathsf{K}$ and $\Box$ prefixes, try to decide well-formedness using only logarithmic working space; any concrete family that provably exceeds logarithmic space would falsify the lemma and break the logspace strength of all three reductions.

Watch

Extended reading notes

Core claim

The central claim is Theorem 1.1: the satisfiability problems of K4×S5, S4×S5, and SSL are each EXPSPACE-hard under logspace reduction. Starting from EXPSPACE = AEXPTIME, the paper fixes an alternating Turing machine M running in time $2^{p(n)}$ and builds, for input w, a bimodal formula $f_{SSL}(w)$ that is satisfiable in a cross-axiom model exactly when M has an accepting tree on w. In such a model, $\mathsf{L}$-equivalence classes (clouds) stand for computation-tree nodes; shared variables carry time, head position, state, and read and written symbols; and the cross property lets a later cloud retrieve the symbol written at an earlier visit to the same tape cell. The formula has polynomial size and is generated in logarithmic space, and both directions of the satisfiability equivalence are verified. The paper then gives a logspace translation of SSL formulas into S4×S5 formulas and of S4×S5 formulas into K4×S5 formulas, so the lower bound transfers. With the companion upper bound, Theorem 1.2 follows: all three logics are EXPSPACE-complete under logspace reduction.

Load-bearing premise

The load-bearing premise is that checking whether a string is a well-formed bimodal formula can be done in logarithmic space; the paper states this as Lemma 5.6, explicitly says the proof is omitted, and every logspace claim in the reduction chain depends on that fact.

Editorial extensions

If this is right

  • The three satisfiability problems are EXPSPACE-complete, not merely NEXPTIME-hard or PSPACE-hard as previously known.
  • Any solver for SSL, S4×S5, or K4×S5 must face instances that require exponentially much space on infinitely many inputs, unless EXPSPACE collapses to a smaller class.
  • The logspace chain SSL ≤ S4×S5 ≤ K4×S5 transfers lower bounds uniformly, so future lower-bound proofs for any one of these logics immediately apply to the others.
  • The direct reduction in the appendix shows that exponential-time alternating Turing machine computations can be encoded straight into S4×S5, without passing through subset-space semantics.
  • The previously open conjecture reported in the introduction—that K4×S5 and S4×S5 are EXPSPACE-complete—is confirmed by the paper together with its companion.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial inference: the shared-variable construction is a reusable encoding trick for any bimodal logic with an equivalence relation in one dimension, a preorder in the other, and a cross property: such logics can simulate alternating time-bounded computation directly.
  • Editorial inference: the delicate subformula is the one that recovers the symbol written at the previous visit to a tape cell; streamlining that bookkeeping could adapt the reduction to prove lower bounds for fragments with fewer propositional variables or restricted modal depth.
  • Editorial inference: because Lemma 5.6 is stated without proof, any reuse of these reductions should first supply the omitted ALOGTIME membership argument; a reader who wants only the satisfiability equivalence rather than the logspace strength can bypass that lemma.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

1 major / 5 minor

Summary. This paper establishes EXPSPACE-hardness under logspace reductions for the satisfiability problems of three bimodal logics: K4×S5, S4×S5, and the logic SSL of subset spaces (Theorem 1.1). The proof proceeds in three stages. Section 4 gives the main construction: a logspace reduction from AEXPTIME (= EXPSPACE) to SSL satisfiability. The reduction encodes accepting trees of exponential-time alternating Turing machines by cross axiom models, using shared variables and binary counters (Section 3) to store time, tape head position, state, and read/written symbols, and to propagate the content of revisited cells via the cross property. Both directions are verified: from accepting trees one constructs a model (Section 4.3), and from any model one extracts an accepting tree by an extension argument on partial trees (Section 4.4, Lemma 4.2). Sections 5 and 6 then give logspace translations SSL→S4×S5 and S4×S5→K4×S5; their correctness is proved as Propositions 5.3 and 6.3, and their logspace computability relies on Corollary 5.7 (the language of bimodal formulas is in LOGSPACE), which rests on Lemma 5.6 (L ∈ ALOGTIME). An appendix provides an alternative direct logspace reduction from AEXPTIME to S4×S5. With the ESPACE upper bounds of the companion paper [8], the paper concludes EXPSPACE-completeness (Theorem 1.2).

Significance. The result is substantial and, if the logspace gap discussed below is closed, settles a conjecture of Marx reported in Kurucz et al. [13, Problem 6.67], improving the known NEXPTIME lower bounds for K4×S5 and S4×S5 and the PSPACE lower bound for SSL to the presumably optimal EXPSPACE bound matching the upper bounds of [8]. The paper's strengths include the original 'shared variable' mechanism for SSL, the explicit binary counters in cross axiom models, and the unusually detailed bidirectional verification of the ATM simulation: the model construction (Section 4.3) and the partial-tree extraction (Section 4.4) are spelled out with full case analyses, and the appendix's direct S4×S5 reduction provides an independent route to the same lower bound for S4×S5. The logspace computability of the Section 4 reduction is argued directly with counter bounds; the only load-bearing missing piece is the proof of Lemma 5.6.

major comments (1)
  1. [§5.3, Lemma 5.6 and Corollary 5.7; also used in §6] The logspace claim for two of the three reductions rests on an unproved lemma. Lemma 5.6 states that the language L of bimodal formulas is in ALOGTIME, and Corollary 5.7 concludes L ∈ LOGSPACE. The proof of Lemma 5.6 is explicitly omitted ('we omit the proof of Lemma 5.6'). This lemma is load-bearing in two places: the SSL→S4×S5 reduction (§5.3) first decides membership of the input string in L and then parses ϕ to locate subformulas, match parentheses, and count modal subformulas; the S4×S5→K4×S5 reduction (proof of Theorem 6.1) likewise invokes Corollary 5.7 before any parsing. If L were not decidable in logspace, Theorems 5.1 and 6.1 would only yield polynomial-time reductions, and Theorem 1.1 would be reduced to a polynomial-time hardness statement for S4×S5 and K4×S5. The lemma is standard (a Buss-style ALOGTIME argument should suffice), but as written the paper contains a load-bearing gap. Please supply a proof of Lemma 5.6 or replace Corollary 5.7 with a direct logspace parsing algorithm that also justifies the subformula-extraction steps.
minor comments (5)
  1. [§5.2/§5.3 (Definition 5.2)] Definition 5.2 chooses main as the alphabetically first propositional variable not occurring in sf(ϕ), while the algorithm in §5.3 searches for the numerically smallest index j with xbin(j)∉sf(ϕ); these two orders need not coincide, and although any fresh variable works semantically, the definition and the implementation should be reconciled.
  2. [Appendix A.1 (Proposition A.2)] In Proposition A.2(2), the statement 'p0|= counter SSL,n' should read 'p0|= counterS4×S5,n', since the proposition concerns S4×S5 models.
  3. [Abstract and §1] The paper uses both 'ESPACE' and 'EXPSPACE' for exponential space; please either standardize the notation or state explicitly on first use that the two names denote the same class.
  4. [§6 (Proposition 6.3)] In the backward direction of Proposition 6.3, the verification that the constructed model M is an S4×S5-commutator model and the K-case of the induction are both delegated to 'similar' arguments without stating the key observation that every L'-successor and every ♦'-successor of a point in W lies in W; stating this observation explicitly would make the proof easier to check.
  5. [§2] Several definitions used throughout the paper (cross axiom models, the induced cloud relation, the exact syntax of bimodal formulas) are deferred to the companion paper [8]; given that Theorem 1.2 is conditional on [8], it would improve self-containedness to restate the most load-bearing definitions.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the hardness proofs are self-contained reductions with one acknowledged non-circular proof gap.

full rationale

The paper's claimed derivations are self-contained against external computational-complexity benchmarks rather than against their own conclusions. The EXPSPACE-hardness proof for SSL in Section 4 works by reducing an arbitrary AEXPTIME language to SSL satisfiability, using the external fact AEXPTIME = EXPSPACE, and then gives a full model construction and a converse accepting-tree extraction argument; no step defines SSL satisfiability in terms of the constructed formula or fits parameters to the target data. The reductions in Sections 5 and 6 are logical translations whose satisfiability equivalences are proven directly in Lemmas 5.4, 5.5, and Proposition 6.3, without invoking the paper's own upper-bound result. The only load-bearing gap is Lemma 5.6, where the paper says 'we omit the proof of Lemma 5.6' and relies on that lemma for the logspace computability of the SSL-to-S4xS5 and S4xS5-to-K4xS5 reductions. That omitted proof is a genuine correctness concern, but it is not circularity: the lemma is presented as a standard ALOGTIME fact supported by Buss's external work, and the semantic equivalence of the reductions is established independently of it. The companion paper [8] by the same authors is cited for terminology and for the matching ESPACE upper bound, but the EXPSPACE-hardness derivations do not reduce to that citation. No fitted input is relabeled as a prediction, no uniqueness theorem from the authors is imported to force a choice, and no known result is merely renamed. The central claim therefore has independent mathematical content, and the circularity score is 0.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The paper relies on standard complexity theorems (AEXPTIME = EXPSPACE, efficient one-tape ATM simulation) and on two unproved or externally deferred items: the LOGSPACE parsability of bimodal formulas (Lemma 5.6) and the semantic definitions from the companion paper [8]. There are no fitted numerical parameters and no newly posited objects beyond the logical formulas themselves.

assumptions (4)
  • standard math AEXPTIME = EXPSPACE
    Used in Section 4 to move from EXPSPACE languages to exponentially time-bounded alternating Turing machines; cited to Chandra and Stockmeyer [3, Corollary 3.6].
  • standard math One-tape alternating Turing machines simulate multi-tape ATMs with polynomial time overhead
    Invoked in Section 3.3 to justify using one-tape ATMs; cited to [3, Proposition 3.4].
  • domain assumption Bimodal formulas can be recognized in logarithmic space (Lemma 5.6)
    Stated in Section 5.3 and used by Corollary 5.7 and the logspace reduction algorithms, but the proof is omitted; the paper says 'Therefore, we omit the proof of Lemma 5.6.' The result is plausible from Buss's ALOGTIME work but is not demonstrated here.
  • domain assumption The semantics of SSL, K4×S5, and S4×S5 are as defined in the companion paper [8]
    Section 2 directs the reader to [8] for definitions of cross axiom models, commutator models, and satisfaction. These definitions are load-bearing for every proof in this paper, but are not restated.

how reviews work

0 comments
Cite this review

Pith. "Pith review of EXPSPACE-Completeness of the Logics K4xS5 and S4xS5 and the Logic of Subset Spaces, Part 2: EXPSPACE-Hardness." pith.science (2026). https://pith.science/paper/N5DUQHGA

@misc{pith2026190803509,
  author       = {Pith},
  title        = {Pith review of: EXPSPACE-Completeness of the Logics K4xS5 and S4xS5 and the Logic of Subset Spaces, Part 2: EXPSPACE-Hardness},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/N5DUQHGA}},
  note         = {Machine review of arXiv:1908.03509}
}
read the original 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.

Figures

Figures reproduced from arXiv: 1908.03509 by the authors.

Figure 1
Figure 1. Cross axiom model of α ∧ ♦(¬α ∧ ♦α). • For a natural number i, we define the finite set Ones(i) ⊆ N by X k∈Ones(i) 2 k = i, that is, 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 0). • We will also need the bits bk(i) ∈ {0, 1} of the binary representation of i, for i, k ∈ N. They are defined by bk(i) := ( 1 if k ∈ Ones(i), … view at source ↗
Figure 2
Figure 2. A cross axiom model of the formula counterSSL,n. It is straightforward to check that ♦→ is reflexive and transitive. The cross property is satisfied as well. Thus, (W, L →, ♦→) is a cross axiom frame. We define the valuation σ by σ(Ak) := {ui,k : i ∈ {0, . . . , 2 n }} ∪ {si,k : i ∈ {0, . . . , 2 n − 1} and k ∈ Ones(i)}, σ(B) := P, σ(Xk) := {pi,j : i, j ∈ {0, . . . , 2 n − 1} and k ∈ Ones(j)}, for k ∈ {0, . . . , n … view at source ↗
Figure 3
Figure 3. Staircase of points. and hence on the one hand pi,i+1 |= (X = binn(i + 1)). Due to (3.1), we have on the other hand pi,i+1 |= (α = binn(i)). This proves the first claim. For the second claim we observe that by definition of σ also pi+1,i+1 |= (X = binn(i + 1)). Since pi+1,i+1 ∈ Ci+1 we also have by (3.1) that pi+1,i+1 |= (α = binn(i + 1)) and hence pi+1,i+1 |= (X = α). Thus, we have constructed a cross axiom model f… view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: A possible detail of a cross axiom model of the formula [PITH_FULL_IMAGE:figures/full_fig_p024_4.png]
Figure 5
Figure 5. Figure 5: Illustration of the S4 × S5-commutator model associated in the proof of Lemma 5.4 with a cross axiom model. Finally we define σ 0 (main) := W, σ 0 (A) := σ(A), for A ∈ AT \ {main}. We wish to show the following: 1. M0 is an S4 × S5-commutator model, 2. M0 , w |= Tb(ϕ).…
Figure 6
Figure 6. Figure 6: An S4 × S5-product model of the formula counterS4×S5,n. We define an S5-frame (W2, RL) by W2 := {0, . . . , 2 n − 1} and RL := W2 × W2. Then the product frame (W, ♦→, L →) with W := W1 × W2 and with ♦→ and L → defined as in [8, Definition 2.2] is an S4 × S5-frame. We d…
Figure 7
Figure 7. Figure 7: A possible detail of an S4 × S5-product model of the formula fS4×S5(w). Consider a certain cell and let us assume that v1, v2, v3 are the first three computation nodes on some computation path in which this cell is visited. Let ti := time(vi). The diagram on the left s…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

33 extracted references · 33 canonical work pages

  1. [8]

    Hertling and G

    P. Hertling and G. Krommes. EXPSPACE-completeness of the logics K4× S5 and S4× S5 and the logic of subset spaces, part 1:ESPACE-algorithms, 8 2019. Submitted for publication

    work page 2019

  2. [1]

    S. R. Buss. The Boolean formula value problem is in ALOGTIME. In A. V. Aho, editor, Proceedings of the 19th Annual ACM Symposium on Theory of Computing, New York, pages 123–131. ACM, 1987

    work page 1987

  3. [2]

    A. K. Chandra, D. C. Kozen, and L. J. Stockmeyer. Alternation.ACM, 28(1):114–133, Jan. 1981

    work page 1981

  4. [3]

    A. K. Chandra and L. J. Stockmeyer. Alternation. In 17th Annual Symposium on Foundations of Computer Science, 1976, pages 98–108. IEEE, 1976

    work page 1976

  5. [4]

    P. Clote. Computation models and function algebras. In Handbook of Computabil- ity Theory, volume 140 ofStud. Logic Found. Math., pages 589–681. North-Holland, Amsterdam, 1999

    work page 1999

  6. [5]

    Dabrowski, L

    A. Dabrowski, L. S. Moss, and R. Parikh. Topological reasoning and the logic of knowl- edge. Ann. Pure Appl. Logic, 78:73–110, 1996

    work page 1996

  7. [6]

    Heinemann

    B. Heinemann. Augmenting subset spaces to cope with multi-agent knowledge. In International Symposium on Logical Foundations of Computer Science, pages 130–145. Springer, 2016

    work page 2016

  8. [7]

    Heinemann

    B. Heinemann. A subset space perspective on agents cooperating for knowledge. In International Conference on Knowledge Science, Engineering and Management, pages 503–514. Springer, 2016

    work page 2016

Show all 33 references
  1. [9]

    O. H. Ibarra, T. Jiang, and B. Ravikumar. Some subclasses of context-free languages in NC1. Information Processing Letters, 29(3):111–117, 1988

    1988

  2. [10]

    D. Kozen. On parallelism in Turing machines. In17th Annual Symposium on Founda- tions of Computer Science, pages 89–97. IEEE, 1976

    1976

  3. [11]

    G. Krommes. A new proof of decidability for the modal logic of subset spaces. InEighth ESSLLI Student Session, pages 137–148. Citeseer, 2003

    2003

  4. [12]

    G. Krommes. Untersuchungen zur modalen Logik von Mengenräumen: Vollständigkeit, Entscheidbarkeit, Komplexität. Master’s thesis, FernUniversität Hagen, 2003

    2003

  5. [13]

    Kurucz, F

    A. Kurucz, F. Wolter, M. Zakharyaschev, and D. M. Gabbay.Many-Dimensional Modal Logics: Theory and Applications, Volume 148 (Studies in Logic and the Foundations of Mathematics). North Holland, 2003

    2003

  6. [14]

    Lange and C

    M. Lange and C. Lutz. 2-EXPTIME lower bounds for propositional dynamic logics with intersection. The Journal of Symbolic Logic, 70(4):1072–1086, 2005. References 49

    2005

  7. [15]

    M. Marx. Complexity of products of modal logics.Journal of Logic and Computation, 9(2):197–214, 1999

    1999

  8. [16]

    C. H. Papadimitriou. Computational Complexity. Amsterdam: Addison-Wesley Pub- lishing Company, 1994

    1994

  9. [17]

    Parikh, L

    R. Parikh, L. S. Moss, and C. Steinsvold. Topology and epistemic logic. InHandbook of Spatial Logics, pages 299–341. Springer, 2007

    2007

  10. [18]

    shared variables

    W. J. Paul, E. J. Prauß, and R. Reischuk. On alternation.Acta Informatica, 14(3):243– 255, 1980. A Reduction of ATMs Working in Exponential Time to S4× S5 50 A Reduction of Alternating Turing Machines Working in Exponential Time to S4× S5 In Section 4 we have shown that any la...

    1980

  11. [19]

    First me make an L →-step from the point pi to a point p′ i where we store the number i + 1 in a vectorX := Xn−1,...,X 0 of usual propositional variables by demanding that p′ i|= (X =α,>k )∧ rightmost_one(X,k )

  12. [20]

    Note that the value ofX is copied fromp′ i to its ♦ →-successorpi+1 because by the formula persistent(X) we force the vectorX of propositional variables to be persistent

    Then we make a ♦ →-step from the pointp′ i to a pointpi+1 in the cloudCi+1 and demand that pi+1|= (X =α). Note that the value ofX is copied fromp′ i to its ♦ →-successorpi+1 because by the formula persistent(X) we force the vectorX of propositional variables to be persistent. ...

  13. [21]

    For all n∈ N\{ 0}, for every S4× S5-commutator model of counterS4×S5,n and for every pointp0 in this model withp0|= counter SSL,n there exist a sequence of2n− 1 pointsp1,p 2,...,p 2n−1 and a sequence of2n− 1 pointsp′ 0,p′ 1,...,p ′ 2n−2 such that • for 0≤i≤ 2n− 1, pi|= (α = bi...

  14. [22]

    We define an S4-frame(W1,R ♦) by W1 :={0,..., 2n− 1} and, fori,i′∈W1, iR♦i′ :⇐⇒ i≤i′

    We construct an S4× S5-product model M with a point (0, 0) in M such that M, (0, 0)|= counterS4×S5,n as follows; see Figure 6. We define an S4-frame(W1,R ♦) by W1 :={0,..., 2n− 1} and, fori,i′∈W1, iR♦i′ :⇐⇒ i≤i′. A Reduction of ATMs Working in Exponential Time to S4× S5 53 Bina...

  15. [23]

    staircase

    The proof forS4× S5-commutator models of the formulacounterS4×S5,n is very similar to the proof for cross axiom models of the formulacounterSSL,n in Proposition 3.2. For completeness sake we explicate it in detail. Suppose there are anS4× S5-commutator modelM oftheformula coun...

  16. [24]

    The functionfS4×S5 can be computed in logarithmic space

  17. [25]

    can be mapped to

    For anyw∈ Σ∗, w∈L ⇐⇒ the bimodal formulafS4×S5(w) is S4× S5-satisfiable. 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...

  18. [26]

    So, we shall assume thatr1 ♦ →x, for allv∈W1, andRL =W2×W2

    By structural induction one shows that for any bimodal formulaϕ and for any(v,x )∈W′ 1×W′ 2, (W1×W2, ♦ →, L →,σ ), (v,x )|=ϕ ⇐⇒ (W′ 1×W′ 2, ♦ → ′ , L → ′ ,σ ), (v,x )|=ϕ. So, we shall assume thatr1 ♦ →x, for allv∈W1, andRL =W2×W2. Note that this implies that ifϕ is a formula w...

  19. [27]

    2.{(π(v),π (v′)) : v,v′∈V and vEv′}⊆ R♦

    π(root) =r1. 2.{(π(v),π (v′)) : v,v′∈V and vEv′}⊆ R♦

  20. [28]

    A Reduction of ATMs Working in Exponential Time to S4× S5 72

    (∀v∈V\{ root}) (∃x∈W2) (π(v),x )|= ( (αprevpos = binN+1(pos(pred(v))))∧αwritten written(v) ) . A Reduction of ATMs Working in Exponential Time to S4× S5 72

  21. [29]

    partial tree ofM on inputw

    (∀v∈V ) (∃x∈W2) (π(v),x )|= ( (αtime = binN(time(v)))∧ (αpos = binN+1(pos(v))) ∧αstate state(v)∧αread read(v) ) . We say thatT can be mapped toModel if there exists a morphism fromT to Model. Below we shall prove the following lemma. Lemma A.3. If a partial treeT = (V,E,c ) of...

  22. [30]

    The conditionπ(root) =r1 is true by definition

  23. [31]

    So, the second condition is satisfied

    The treeT0 does not have any edges, that is, its setE of edges is empty. So, the second condition is satisfied

  24. [32]

    The third condition does not apply to the treeT0 because T0 has only one node, its root

  25. [33]

    a partial tree ofM on inputw

    On the one hand, we have time(root) = 0, pos(root) = 2N− 1, state(root) =q0, and read(root) = #. A Reduction of ATMs Working in Exponential Time to S4× S5 73 On the other hand, the condition(r1,r 2)|= start says (r1,r 2)|= ( (αtime = binN(0))∧ (αpos = binN+1(2N− 1))∧αstate q0 ...

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.