News for hackers. Stuff that matters.

A comment on Leslie Lamport: Video course on TLA+. Parent comment

Re:Leslie Lamport: Video course on TLA+ by Aclassifier on Monday March 27, 2017 @03:41AM (#13965833)
> Well I respect Mr.Lamport`s point, but to prove liveness you are almost doomed to use temporal logic.

I thought CSPm/FDR4 proved liveness on infinite event trails without temporal logic? Can't one extract "never" and "sooner or later" by just exploring the whole state space? Deadlock/livelock will never happen etc.

[ Parent | on HN ]
Re:Leslie Lamport: Video course on TLA+ by unboxed_type on Tuesday March 28, 2017 @06:58AM (#13975558)
Yes, but what if you are unable to explore the whole state space due to its unboundedness? Then the only way I know is by deducing properties thru temporal reasoning.
[ Parent | on HN ]