Commentary by Chris Pressey

This work is distributed under a CC-BY-ND-4.0 license, with the following explicit exception: the ratings may be freely used for any purpose with no limitations.

TLA+

The Temporal Logic of Actions

• rating: classic

I'm doing myself a disservice by not glossing this in full.

TLA+ is reasonably well known but this paper itself is seemingly little-known.

TLA is a temporal logic, but it is also a dynamic logic ("action logic"; logic of sequential progression of states). It seems to be a "good" combination of these two approaches, in that its combination does not annul the benefits of either of the individual component logics.

There is more detail to it than this: the Wikipedia article on dynamic logic has a section about "endogenous" vs "exogenous" logic; endogenous logics (such as temporal logic) are more abstract in some sense, and so better equipped to deal with questions of concurrent behaviour.

The TLA combination seems to combine the two into (an endogenous?) single logic without losing that capacity to deal effectively with concurrency.

This is possibly due to the so-called "stuttering" - handling of what are basically an unbounded set of null transitions between real transitions - which is apparently critical to use TLA effectively, and I can kind of see why.

Another thing is that it's not just a logic, it's also a synax for logic (the indented groups of conjunctions and disjunctions). I have to wonder how much this has dampened its adoption.

The TLA+ Home Page

• rating: 1

.

Learn TLA+ --- Learn TLA+

• rating: 1

.

Practical TLA+ by Hillel Wayne

• rating: 1

.

tlaplus/PlusPy: Python interpreter for TLA+ specifications

• rating: 2

Most TLA+ tools do model checking or theorem proving, but this one is actually an interpreter.