In modal logic, is there a formula that could express the inverse of accessibility relation? For example, in S4, is there a formula that corresponds to the proposition "p is true in every world from which u is accessible (but is not accessible from u)"? 
 A: No there is not.
To be a little more precise on the formalism involved, we consider the following language of propositional modal logic over a set $Var=\{p_0,p_1,\dots\}$ of propositional variables:
$$\mathcal L_\Box:\phi::=p\mid\neg\phi\mid (\phi\land\phi)\mid\Box\phi$$
for $p\in Var$.
$\mathbf{S4}$ is strongly complete w.r.t. the class of transitive and reflexive Kripke models which will be important later on.

Consider the following argument. Take a Kripke model $\mathfrak M=\langle W,R,V\rangle$ and a world $w\in W$ and construct from it the model $\mathfrak M^{p(w)}=\langle W^{p(w)},R^{p(w)},V^{p(w)}\rangle$ (let's call it the $w$-previous companion of $\mathfrak M$) as follows:


*

*Take $W^{p(w)}=W\setminus\{v\in W\mid (v,w)\in R\text{ but }(w,v)\not\in R\}$

*Set $R^{p(w)}=R\cap (W^{p(w)}\times W^{p(w)})$

*Set $V^{p(w)}(p)=V(p)\cap W^{p(w)}$ for any $p\in Var$.


Note, that $w\in W^{p(w)}$ as either $(w,w)\in R$ or $(w,w)\not\in R$. We now show that in $\mathcal L_\Box$ a model $\mathfrak M$ and it's $w$-previous companion $\mathfrak M^{p(w)}$ for some world $w$ in $\mathfrak M$ are not distinguishable, i.e. we show the following lemma:

Lemma: Let $\mathfrak M=\langle W,R,V\rangle$ be a transitive and reflexive Kripke model and $w\in W$. Then for any $\phi\in\mathcal L_\Box$ and any $v\in W^{p(w)}$ where $(w,v)\in R$: $(\mathfrak M, v)\models\phi$ iff $(\mathfrak M^{p(w)},v)\models\phi$.

Proof: By induction on $\mathcal L_\Box$:
For the induction base, note that $v\in V(p)$ iff $v\in V(p)\cap W^{p(w)}=V^{p(w)}(p)$ as $v\in W^{p(w)}$.
For the induction step, let $\phi,\psi$ be two formulas for which the claim is true and let $v\in W^{p(w)}$ be arbitrary such that $(w,v)\in R$. Then the cases for $\neg,\land$ are straightforward by the induction hypothesis and we only look at $\Box\phi$.
For this, first suppose that $(\mathfrak M,v)\models\Box\phi$, i.e. $\forall u\in W:(v,u)\in R$ implies $(\mathfrak M,u)\models\phi$. Now, take any $u'\in W^{p(w)}\subseteq W$ and suppose $(v,u')\in R^{p(w)}$, then $(v,u')\in R$ and thus $(\mathfrak M,u')\models\phi$. Also, by transitivity of $R$, we have $(w,u')\in R$. By the induction hypothesis, we have $(\mathfrak M^{p(w)},u')\models\phi$ which shows $(\mathfrak M^{p(w)},v)\models\Box\phi$.
For the other direction, suppose that $(\mathfrak M,v)\not\models\Box\phi$, i.e. there is a $u\in W$ such that $(v,u)\in R$ but $(\mathfrak M,u)\not\models\phi$. By transitivity $(w,u)\in R$ and thus also $u\in W^{p(w)}$. Therefore $(v,u)\in R^{p(w)}$. By the induction hypothesis, we have $(\mathfrak M^{p(w)},u)\not\models\phi$ and thus $(\mathfrak M^{p(w)},v)\not\models\Box\phi$. $\tag*{$\blacksquare$}$

In the last step, we now show that the new operator you proposed, which I denote here by $\overset\leftarrow{\Box}$, is capable is distinguishing $(\mathfrak M,w)$ and $(\mathfrak M^{p(w)},w)$ for $\mathfrak M$ a transitive and reflexive Kripke model.
Formally, we interpret $\overset\leftarrow{\Box}$ in a pointed Kripke model $(\mathfrak M,w)$ as follows:
$$(\mathfrak M,w)\models\overset\leftarrow{\Box}\phi\text{ iff }\forall v\in W:(v,w)\in R\text{ and }(w,v)\not\in R\text{ implies }(\mathfrak M,v)\models\phi$$
For this, consider the following model: $\mathfrak M=\langle \{1,2\},\{(1,1),(2,2),(2,1)\},V\rangle$ where $V(p_0)=\{1\}$ and $V(p_i)=\emptyset$ for all $i>0$. Then $\mathfrak M^{p(1)}=\langle\{1\},\{(1,1)\},V^{p(1)}\rangle$ and we have that
$$(\mathfrak M,1)\not\models\overset\leftarrow{\Box}p_0$$
and $2$ is the corresponding witness but 
$$(\mathfrak M^{p(1)},1)\models\overset\leftarrow{\Box}p_0$$
as there is no world in $\mathfrak M^{p(1)}$ which can access $1$ but which is not accessible from $1$ (because $1$ accesses itself).
By the above Lemma, there is no formula $\phi\in\mathcal L_\Box$ where for any transitive and reflexive Kripke model $\mathfrak M$ and any world $w$ from $\mathfrak M$: $(\mathfrak M,w)\models\phi$ iff $(\mathfrak M,w)\models\overset\leftarrow{\Box}p_0$.

Note that this also works for the following alternative semantics for $\overset\leftarrow{\Box}$:
$$(\mathfrak M,w)\models\overset\leftarrow{\Box}\phi\text{ iff }\forall v\in W:(v,w)\in R\text{ implies }(\mathfrak M,v)\models\phi$$
