I have used Computational Tree Logic before (https://www.firebase.com/blog/2014-02-04-firesafe-complex-se...)

I wonder if anybody knows what the main differences between CTL and TLA are. Maybe I should switch camps?

EDIT: oooh, you can read the book for free http://research.microsoft.com/en-us/um/people/lamport/tla/bo...

EDIT2: Ahh... TLA has sets for one thing