I am reading the Wikipedia page for Interactive proof systems and am having trouble understand the notation in the definition of soundness, many of which is left unspecified.
Given a formal language of strings $L$, a verifier $\mathcal{V}$ for this language satisfies the soundness property if for every prover $(\tilde{\mathcal{P}})$ and every $y \notin \mathcal{L}$,
$$ \operatorname{Pr}[(\bot,(\text{accept})) \leftarrow (\tilde{\mathcal{P}})(y) \leftrightarrow (\mathcal{V})(y)] < \epsilon $$
for some small $\epsilon \ll 1$. What is meant by the use of $\leftarrow$ and $\leftrightarrow$, as well as $(\bot,(\text{accept}))$? I would appreciate if someone could answer this or point me to a reference that uses (and defines) the same notation.