What is TLA?
Last modified 21 September 2012
What is TLA?
TLA stands for the Temporal Logic of Actions, but it has become a
shorthand for referring to the TLA+ specification language and the PlusCal
algorithm language, together with their associated tools.
TLA+ is based on the idea that the best way to describe things
formally is with simple mathematics, and that a specification language
should contain as little as possible beyond what is needed to write
simple mathematics precisely. TLA+ is especially well suited for
writing high-level specifications of concurrent and distributed
systems.
PlusCal is an algorithm language that, at first glance, looks like a
typical tiny toy programming language. However, a PlusCal expression
can be any TLA+ expression, which means anything that can be expressed
with mathematics. This makes PlusCal much more expressive than any
(real or toy) programming language. A PlusCal algorithm is translated
into a TLA+ specification, to which the TLA+ tools can be applied.
The principal TLA+ tools are the TLC model checker and TLAPS, the TLA+
proof system. All the tools are normally used from the Toolbox, an
IDE (integrated development environment). Go to
the TLA home page
to find out more about TLA.
