0
$\begingroup$

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

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

1 Answer 1

0
$\begingroup$

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$

$\endgroup$
5
  • $\begingroup$ what do you think they mean in the second context? There is no explanation prior to this though $\endgroup$
    – Thang Do
    Commented May 6, 2016 at 9:55
  • $\begingroup$ @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 ..." $\endgroup$
    – dtldarek
    Commented May 6, 2016 at 10:00
  • $\begingroup$ It's actually the first time it appears. i.sstatic.net/5aAkl.jpg $\endgroup$
    – Thang Do
    Commented May 6, 2016 at 10:06
  • $\begingroup$ @csessh Maybe in some other chapter, when dealing with sequences or sets? What is the title of the book? $\endgroup$
    – dtldarek
    Commented May 6, 2016 at 10:54
  • $\begingroup$ 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. $\endgroup$
    – Thang Do
    Commented May 6, 2016 at 11:26

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .