For any set S, S_w denote the set of all infinite sequences of elements in S. For set of states Sigma (state space), a behaviour is an element of Sigma_w.

[2003, book | www]

Lamport, L. (2003). Specifying Systems Addison Wesley.

[1991, article]

Abadi, M., & Lamport, L. (1991). The Existence of Refinement Mappings. Theoretical Computer Science, 82(2), 253-284.