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

Re: [tlaplus] Comparison between TLA+ and LTL



Someone has embedded TLA (some of the "+", too, I think) in Coq: https://www.osti.gov/biblio/1367058

On Wednesday, June 27, 2018 at 10:14:41 AM UTC+1, Apostolis Xekoukoulotakis wrote:
I will need to look into your response more thoroughly but let me make some preliminary remarks.

I have experience with an embedding of LTL in agda and agda has dependent types and existential quantification.
Even though, I know LTL, I have only done practical specification through the new TLA+ video courses.

Alan Jeffrey in his papers, does not make use of dependent types that much, if none at all. This is something that I am experimenting in , behaviors whose type depend on other behaviors.

I hope to use the techniques used in TLA+ and express them in (LTL in agda).

The paper I mentioned has to do with the main goal, to actually use the type system to write the implementation of distributed systems with what is called type-driven development.

Sorry for any vagueness, I need to become a bit more experienced with the subject.

2018-06-26 13:17 GMT+03:00 Stephan Merz <step...@xxxxxxxxx>:
Hello,

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,
Stephan


On 25 Jun 2018, at 16:23, Apostolis Xekoukoulotakis <xek...@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...@googlegroups.com.
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.

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/IdPcWGdQ_Jw/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
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.



--

   ,
     Apostolis Xekoukoulotakis