Reasoning about concurrent algorithms.
- Simpler alternative to programming languages.
- No point in trading language for a complicated logic.
- Expressive to describe real algorithms.
- Formulas must not be too long and complicated to understand.
- TLA formulas:
- Familiar mathematical operators (and).
- ' (prime), always , exists .
- Combination of two logics:
- A logic of actions.
- A standard temporal logic.