How does it compare with TLA+ though? I've tried reading through your document, but I can't seem to understand how the interweaving is done and the blocking.
Harel and Pnueli wanted a formalism that makes it easy for both humans and machines (formal verification) to understand. Formal verification with model checking is, of course, also central in behavioral programming. I guess you could say that synchronous programming (and so behavioral programming, which is a kind of SP) is related to TLA+ in a similar way to how Haskell is related to, say, Agda.
Thanks for the info. I'll have to dive a bit more into TLA+. Even though I still don't see how the request/wait/block is implemented in TLA+... I mean you still need an even selection mechanism for it or not?
Next2 ==
/\ turn' = turn + 1 \* A
/\ current' = Opponent \* B
/\ ∃i,j∈1..N: \* C
/\board[i,j] = Empty \* C.1
/\ board'[i,j] = current \* C.2
Yes, but LSC are also based on temporal logic, as were Harel's Statecharts (perhaps the first synchronous programming language).
> I mean you still need an even selection mechanism for it or not?
Not sure what you mean by "even." TLA+ is nondeterministic, and the formulas can serve as rules to restrict that nondeterminism (where simple logical conjunction is used to compose the rules). Also, nothing is really "implemented" in TLA+, as it's not a programming language. It's a formal specification language that describes the behavior of discrete systems.