How should I interpret the above? I can see that succs is what this function is being named and that in the second line we have an example of it's use. I can also see that Q, which is predefined as a finite set of states, and the powerset of Q have some stake in this operation but I just can't work out what.
Any thoughts? Is this common notation and am I missing something obvious or have I just asked a very narrow question with niche notation?
It means that "succs" is a function whose domain is $Q$--that is, $Q$ is the set of allowable inputs--and whose codomain is the power set of $Q$--that is, every output will be a subset of $Q$.
The second line tells how to determine the output, given any input.