The work described here could be extended to multi-modal logics.
In \dKt, the structural connective $\bullet$ is a proxy for the logical
connectives $\BlkDia$ and $\WhtBox$.
The structural construction $* \bullet *$ is a proxy for the logical
connectives $\WhtDia$ and $\BlkBox$,
since $*$ is a proxy for Boolean negation $\lnot$.
As noted in \S\ref{faxsr},
further primitive axioms can be added to \dKt\ as structural rules
to obtain numerous 
modal extensions.
\comment{catering for Kripke models where the reachability relation is
reflexive, serial, symmetric, euclidean or transitive, to name but a few.
The beauty of Display Logic is that these axioms can be encoded as structural
rules \cite{kracht-power}, thus preserving cut-elimination.
}

To cater for multiple modalities like 
$\WhtDia_i$, $\BlkDia_i$, $\WhtBox_i$, $\BlkBox_i$, $1 \leq i \leq n$,
we simply invent $n$ structural proxies $\bullet_i$,
$1 \leq i \leq n$.
Adding appropriate structural rules then allows
you to build a hybrid multi-modal logic of your choice.
Furthermore, if the interaction axioms for these modalities are
\emph{primitive} \cite{kracht-power},
you can add these interactions as structural rules.
Cut-elimination then comes for free.

Cut-free display calculi do not enjoy the substructure property, although
they do enjoy the subformula property.
Therefore our rules do not immediately give a decision procedure.
Since many tense logics are decidable, further work is required to control
\emph{automatic} proof search using display calculi.