[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Comparison between TLA+ and LTL


first of all, TLA+ is a specification language that is based on Zermelo-Fraenkel 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 omega-regular expressions or, equivalently, monadic second-order logic over linear orders, both restricted to their stuttering-invariant fragments, whereas LTL is equivalent to star-free omega-regular expressions resp. monadic first-order 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,

[1] https://www.cs.cornell.edu/fbs/publications/Hyperproperties.pdf
[2] https://members.loria.fr/SMerz/papers/tla+logic2008.html

On 25 Jun 2018, at 16:23, Apostolis Xekoukoulotakis <xeko...@xxxxxxxxx> wrote:

Is there any short document that describes the differences of TLA+ and LTL?

Linear Temporal Logic types Functional Reactive Programs. ( http://www.asaj.org/papers/plpv12.pdf )
One could then use the type system to provide a correct implementation of the specification.

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.