I have used Computational Tree Logic before (https://www.firebase.com/blog/2014-02-04-firesafe-complex-security-logic-for-firebase.html https://www.firebase.com

I have used Computational Tree Logic before (https://www.firebase.com/blog/2014-02-04-firesafe-complex-security-logic-for-firebase.html 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/book-02-08-08.pdf http://research.microsoft.com/en-us/um/people/lamport/tla/bo... EDIT2: Ahh... TLA has sets for one thing