Go backward to Logic Versus ProgrammingGo up to TopGo forward to The Logic of Actions |

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.

Author: Wolfgang Schreiner

Last Modification: May 14, 1998