> 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 synchrono

> 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.