I'm reading Nir Friedman and Daphne Koller's "Probabilistic Graphical Models: Principles and Techniques". The authors occasionally use the notation
$$p\models X\perp Y \mid Z$$
to indicate that the set of random variables $X$ is independent of $Y$ given $Z$, under $p$ (which is a joint distribution over the values of all of these variables).
I've never studied mathematical logic, but I read a little about models, semantic and syntactic consequences and am still unclear as to the precise meaning of the symbol $\models$ in the expression above. How is this analogous to formal logic systems? Are the conditional independence assertions analogous to formulae? Axioms?
As Mauro ALLEGRANZA explains in the above, double turnstile is a model operator. To get into a bit more detail: double turnstile is the validity operator, which expresses validity of a proposition in a model. So, given a model p, A is valid in p is expressed by p|=A. It is worth noting that this is a little bit different from truth: a model is composed of worlds (if we are using Kripke semantics, which are quite popular, and works for this case if we reinterpret things). So, let p be a set of worlds. A may be true at some worlds in p, or not. If A is true at all worlds in p, then we say A is valid in p, and express this using p|=A (read: "A is valid in p").
In your case, the author apparently uses p|=A to mean "across the whole joint distribution p, A is the case." This is more or less explaining a hieroglyph, but if you want to look into the nuances of |=, looking up kripke semantics for modal logic is a great way of getting into it without necessarily dealing with very heavy logic.