I am looking for modal logics, which are axiomatised by a finite set of axioms of modal nesting depth one, and whose satisfiability / derivability problem is unlikely to be in PSPACE. Without the restriction on the modal nesting depth this is not a problem, see for example PDL. But it seems that in proving for example EXPTIME-hardness by reduction to some kind of tiling problem or acceptance problem for Turing machines, one would need some kind of transitivity, which is axiomatised in depth two. There are also undecidable logics with a binary modality (Kurucz et al.: Decidable and undecidable logics with a binary modality, 1995), but these typically require associativity, which is depth two as well. In Conditional Logic, again it seems that we need depth two for EXPTIME-hardness (Friedman, Halpern: On the Complexity of Conditional Logics, 1994).
Can we get EXPTIME-hardness with axioms of nesting depth one?
Background: We are trying to find generic decision procedures of a good complexity for logics axiomatised with nesting depth one.