This is a paper by Leslie Lamport, a computer scientist who created LaTex and TLA+ (Temporal Logic of Actions), among other innovations in the areas of distributed computing, concurrent and reactive systems.
He retired from Microsoft earlier this year. A draft of his newest book is available on the same site as this post.