## TLA

swMATH ID: | 4442 |

Software Authors: | L. Lamport |

Description: | 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. |

Homepage: | http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html |

Related Software: | SPIN; z3; Z; ByMC; Uppaal; PEPA; Isabelle/UTP; Verdi; Distal; PSync; nuXmv; MathSAT5; SPLLIFT; Featherweight Java; PlusCal; LaTeX; TLAPS; Mizar; Design/CPN; Intel TBB |

Referenced in: | 26 Publications |

Further Publications: | http://research.microsoft.com/en-us/um/people/lamport/tla/papers.html |

all
top 5

### Referenced by 65 Authors

all
top 5

### Referenced in 7 Serials

### Referenced in 4 Fields

25 | Computer science (68-XX) |

7 | Mathematical logic and foundations (03-XX) |

1 | General and overarching topics; collections (00-XX) |

1 | Biology and other natural sciences (92-XX) |