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*.

- Familiar mathematical operators (
- Combination of two logics:
- A logic of actions.
- A standard temporal logic.

Wolfgang.Schreiner@risc.uni-linz.ac.at

$$Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine $$