# What's the meaning this DOT notation?

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

Thang

• $\mu Z.\tau(Z)$ is not an "operation": it is a "complete" symbol meaning: "the least $Z$ such that..." Commented May 6, 2016 at 8:55
• See $\mu$ operator. Commented May 6, 2016 at 10:00
• should I look at $\tau$ operator too? Commented May 6, 2016 at 10:09
• No; $\tau$ is the mapping; they use $\nu$ for the "maximal", but I think that it is not standard. Commented May 6, 2016 at 10:17
• right, that makes sense to what I read in the book. Thanks Mauro. Commented May 6, 2016 at 10:23

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$

• what do you think they mean in the second context? There is no explanation prior to this though Commented May 6, 2016 at 9:55
• @csessh I still think there should be some description. Find the place where it appears for the first time, maybe there? Check carefully, it might be easy to overlook, for example "let $\langle \mathcal{S}, \cdot, \varepsilon \rangle$ be a monoid such that ..." Commented May 6, 2016 at 10:00
• It's actually the first time it appears. i.sstatic.net/5aAkl.jpg Commented May 6, 2016 at 10:06
• @csessh Maybe in some other chapter, when dealing with sequences or sets? What is the title of the book? Commented May 6, 2016 at 10:54
• The book is Model Checking by Edmund M. Clarke. But the screenshot I took is from a past exam paper. I'm looking through other chapters of the book right now. Commented May 6, 2016 at 11:26