I'm studying Computation Tree Logic for a course at university. However, I seem to have forgotten an important detail about set builder notation that I haven't found online yet. I'm wondering if this is just a creative notation used by my university.
The formulas I encounter describe formal semantics of CTL in the form of:
$M ,s \models p$ iff $p\;\epsilon \; L(s)$
However, some are more complex, including an interpunct:
$M ,s \models AX f$ iff $\forall\pi\;\epsilon \; \Pi(M,s) \cdot M,\pi[1] \models f$
And below, which defines the set of execution paths for a Kripke structure:
$\Pi(M,s) \equiv $ { $\pi\;|\;\pi[0] = s \wedge\forall n \;\cdot (\pi[n], \pi[n+1])\;\epsilon\;R$ }
What does the $\cdot$ mean here?
It looks like the dot is just part of the author's notation for quantifiers:
$$ \forall x \in A \cdot \varphi(x) $$ means "the property $\varphi$ holds for all elements of the set $A$". The dot is just there to separate the $A$ from the $\varphi$ (since each of them can be multiple symbols long).
In $\forall n \cdot (\pi[n],\pi[n+1]\in R$ there is no $\in A$ part, but the dot is still there to separate the quantifier from the formula being quantified over.