The definitions i am working with are:
U is the until operator:
To show U is not definable i'm trying to come up with two bisimilar models that disagree over some formula involving U.
The textbook showed something similar for the progressive operator:
But i dont quite understand this example. Why is $\Pi q$ true at 4? And are the numbers supposed to represent the times? I dont think so? Otherwise this is clearly not true as there is no time greater than 4. How are times defined then in these models? Is $t_1 <t_2$ if there is a path from $t_1$ to $t_2$ and $t_2>t_1$ if there is path from $t_2$ to $t_1$? But then $\Pi 4$ is true in both models. But if edges are not how you go about showing if $t_1<t_2$ then what exactly do edges do in temporal modals?
Any help clearing these questions above and showing why U is undefinable is greatly appreciated!
Regarding the case of progressive tense. The numbers are just names of states, the flow of time is represented by the relation between states. Thus, in the figure on the right, for example, after state 3 we enter state 1, and not vice versa. Yes, $t_1 < t_2$ means that there is an arrow starting at $t_1$ and ending at $t_2$.
Now, let us see why $\Pi q$ holds in $M,4$ on the left. By the semantics, $M,4 \models \Pi q$ iff $\exists t_1 <4, t_2>4$ such that $\forall u (t_1 < u < t_2 \to M,u \models q)$. Let us take $t_1 = 3$ and $t_2 = 2$ that is diagonal to the chosen $3$. It is clear that there is only state $4$ between states $3$ and the diagonal $2$, and $M,4 \models q$. At the same time, on the right, if we try to choose $3$ and $2$, there are two available paths: one going through a $q$-state $4$, and another going through a $\lnot q$-state $1$. There are no other candidates for states that are strictly 'greater' and 'less' than four, and thus $M,4 \not \models \Pi q$.
Undefinability of Until. You are right that we need to use a bisimulation argument, but we will need a weaker notion of $n$-bisimulation. Note that formulas with Until cannot distinguish bisimilar models. Now, to the undefinability.
Proof. Consider $\varphi \mathsf{U} \psi$, and assume towards a contradiction that there is an equivalent formula $\chi$ of Priorean Temporal Logic (PTL). Here I for simplicity assume that PTL has only diamonds, i.e. $\mathsf{F}$ and $\mathsf{P}$, and that there are no conditions on relations between states.
Now, since $\chi$ is finite, it has some finite modal depth $n$. Consider further two models that are finite chains of length $n+1$ so that the models are identical up to step $n$ and differ only on the last step $n+1$. Your carefully chosen $\varphi$ and $\psi$ should be so that $\varphi \mathsf{U} \psi$ is true in one model, and false in the other.
At the same time, use the fact that $n$-bisimilarity implies $n$-modal equivalence to argue that the models are not distinguished by the PTL formula $\chi$ of modal depth $n$. QED.
In the proof above, feel free to add details like formulas $\varphi$ and $\psi$, and also the two models.
The main intuition behind the proof is that Until can 'see' at an arbitrary finite distance, while modalities of PTL can 'see' only one step ahead.