You will want to replace the "+" in TLA+ (the language for writing state and action formulas) with a typed language. Since you can't achieve both the simplicity and expressiveness of TLA+ with a typed language, you will probably choose a less expressive language. If you want a language that is useful for engineers, you will need to make sure that it will be able to describe the kind of distributed systems that engineers build. Ideally, you'd look at real industrial TLA+ specs. However, those aren't made public. (One exception is the user interface spec of Cosmos DB that Microsoft has promised to make public, but I don't know if it's available yet.) But you should look at the "academic" TLA+ specs that are available. One is the PaxosCommit spec that is mentioned in the video course. A more complicated example is the spec of the Castro-Liskov Byzantine agreement algorithm. The spec is described here
http://lamport.azurewebsites.net/pubs/pubs.html#web-byzpaxos
and the actual TLA+ files are available here:
http://lamport.azurewebsites.net/tla/byzpaxos.html
(You can ignore the proofs and just look at the algorithms and the correctness conditions, which assert that the Castro-Liskov algorithm implements a higher-level spec under a suitable refinement mapping.)
Leslie
On Wednesday, June 27, 2018 at 2:14:41 AM UTC-7, 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 MerzHello,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 LTLG(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 asx' = 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 asUntil(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,StephanOn 25 Jun 2018, at 16:23, Apostolis Xekoukoulotakis 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 toTo post to this group, send email to
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.
To post to this group, send email to
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
--
--,Apostolis Xekoukoulotakis
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.