The paper introduces the Temporal Logic of Actions (TLA), a logic designed for specifying and reasoning about concurrent systems. TLA combines two logics: a logic of actions and a standard temporal logic. The logic of actions represents algorithms as assigning values to variables, while the temporal logic handles sequences of states and temporal properties. TLA is simple, with its syntax and formal semantics summarized in about a page, yet it is powerful for both theoretical and practical purposes. The paper discusses how TLA is used to specify and verify concurrent algorithms, emphasizing the importance of reasoning about abstract algorithms rather than real, compiled programs. It also covers the use of rigid variables, quantifiers, and the enabled predicate, and introduces the Raw Temporal Logic of Actions (RTLA) as a precursor to TLA. The paper provides examples and detailed explanations of how to describe programs and properties using TLA, including the concept of stuttering steps and fairness conditions. Finally, it outlines the syntax, semantics, and proof rules of Simple TLA, which is sufficient for specifying and reasoning about concurrent systems.The paper introduces the Temporal Logic of Actions (TLA), a logic designed for specifying and reasoning about concurrent systems. TLA combines two logics: a logic of actions and a standard temporal logic. The logic of actions represents algorithms as assigning values to variables, while the temporal logic handles sequences of states and temporal properties. TLA is simple, with its syntax and formal semantics summarized in about a page, yet it is powerful for both theoretical and practical purposes. The paper discusses how TLA is used to specify and verify concurrent algorithms, emphasizing the importance of reasoning about abstract algorithms rather than real, compiled programs. It also covers the use of rigid variables, quantifiers, and the enabled predicate, and introduces the Raw Temporal Logic of Actions (RTLA) as a precursor to TLA. The paper provides examples and detailed explanations of how to describe programs and properties using TLA, including the concept of stuttering steps and fairness conditions. Finally, it outlines the syntax, semantics, and proof rules of Simple TLA, which is sufficient for specifying and reasoning about concurrent systems.