The following variant of modal UDT seems to satisfy the notion of injectivity by using the "time of decidability", but I'm not sure if it will work:

Consider a sequence of possible actions $a_n$ and utilities $u_n$. At stage $n$, the agent sees if PA proves ${\square }_n\left(U\right()\ge u_n)\wedge \neg {\square }_{n-1}\left(U\right()\ge u_n)$, and returns $a_n$ if it succeeds.

I haven't yet tried this out with the model checker, but it's an intriguing idea; you don't even need to explicitly include the proposed action in the thing you're trying to prove!