Hello, first of all, TLA+ is a specification language that is based on ZermeloFraenkel set theory and TLA (the temporal logic of actions), but it is not a logic itself. It is therefore more appropriate to compare TLA and LTL. Indeed, TLA is a variant of LTL that contains the constructs that Leslie considers useful for the practice of specifying and verifying algorithms. Below is a (rough) comparison; I'll use letters (G,F,X,U) to refer to the operators of LTL and symbols ([] and <>) to refer to those of TLA. You can find some more details in [2]. 1. From a purely logical point of view, LTL contains the basic temporal operators X (next) and U (until), from which the other operators can be derived. For example, F phi is an abbreviation for "true U phi". TLA contains the temporal operators [] and <>, as well as the operators [][_]_ and <><_>_ that take an action and a state function to yield a temporal formula. It does not contain X, but the priming operator constructs an action from a state formula. In particular, TLA cannot express the basic induction principle of LTL G(phi => X phi) => (phi => G phi) but only a restricted version for state formulas [][P => P']_P => (P => []P). The different levels of formulas (state functions, actions, temporal formulas) help ensure syntactically that every (temporal) formula of TLA is invariant w.r.t. finite stuttering. 2. Pragmatically, TLA is oriented towards writing specifications of state machines. Typically, actions are composed from formulas such as x' = x+y (or similar constructs) that are awkward to express in LTL because they are not propositional in nature: you'd have to write something like \E z : z = x+y /\ X (x=z) 3. The above restriction in expressiveness is compensated for by the fact that TLA has quantifiers over state variables (\EE and \AA). These can be used to represent hiding of internal implementation details within the logic, they can also be used to express hyperproperties (see e.g. [1]). It is not very difficult to show that using these quantifiers, purely propositional TLA expresses exactly omegaregular expressions or, equivalently, monadic secondorder logic over linear orders, both restricted to their stutteringinvariant fragments, whereas LTL is equivalent to starfree omegaregular expressions resp. monadic firstorder logic over linear orders. In particular, you can express the "until" operator of LTL as Until(phi, psi) == \EE p, q, r : /\ [](phi <=> p) /\ [](psi <=> q) /\ r <=> q /\ [][ \/ r \/ p /\ (r' <=> q')]_<<p,q,r>> /\ <>r (modulo any typos that I may have made). The first conjunct introduces propositional variables p and q that represent the temporal formulas phi and psi within the remainder of the formula; the rest of the formula describes the mechanics of "until" as a state machine. Note that the TLC model checker does not support \EE or \AA (and TLAPS doesn't support them either at this point, but eventually should). If there is any connection with the article that you mention is beyond my understanding. Best regards, Stephan
