# Definition of soundness for interactive proof systems

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.

• $$\tilde{\mathcal{P}}(y)\leftrightarrow\mathcal{V}(y)$$ denotes that $$\tilde{\mathcal{P}}$$ and $$\mathcal{V}$$ are interactive machines involved in an interactive protocol with common input the statement $$y$$ (an alternative is to use $$\langle\tilde{\mathcal{P}},\mathcal{V}\rangle(y)$$)
• $$\leftarrow$$ usually denotes the randomised output that results from this interaction (the verifier and the prover could use random coins)
• $$\bot$$ denotes that the (malicious) prover $$\tilde{\mathcal{P}}$$ has no (private) output at the end of the protocol (think of zero-knowledge protocols, e.g.)
• $$\text{accept}$$ denotes that the verifier accepts at the end of the protocol (again, think of zero-knowledge protocols)