I thought BP was built on top of Live Sequence Charts
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.
Comments
Yes, but LSC are also based on temporal logic, as were Harel's Statecharts (perhaps the first synchronous programming language).
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.