What's the meaning this DOT notation?

1.1k Views Asked by At

I'm reading a chapter in a Model Checking book. I came across this chapter "Symbolic Model Checking", in which the author mentions Fixed Point representation.

I don't know how to explain the context, so I took a photo of that paragraph instead.

In another example that I found:

This example talks about reachability games

I really appreciate your help.

Thang

1

There are 1 best solutions below

5
On BEST ANSWER

It seems to me, that dots in these two examples might have a different meaning.

The first one looks very much like a dot from Lambda calculus, and given that the chapter talks about fixpoints, I find that highly probable. If this is the case, then the dot is only a delimiter, and it is to indicate that the symbols that come between the operator ($\nu$ or $\mu$ in your example, or $\lambda$ in lambda calculus) are variables bound by that particular operator. To give you a more common example, you can write quantifiers like this: $\forall x. \phi(x)$ instead of $\forall x (\phi(x))$, $\forall x : \phi(x)$ or yet some other notation.

The second dot seems like some kind of conjunction, perhaps a composition of states, or sequence concatenation or something similar, there should be an explanation before in the text.

I hope this helps $\ddot\smile$