Rigid and flexible variables

[fl]

I've just read Leslie Lamport's "Temporal Logic of Actions" ACM Transactions on Programming Languages and Systems, 1994:

http://dl.acm.org/citation.cfm?id=177726

http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-actions.pdf

(I suppose this article is an exact description of what is implemented currently by TLA+ and TLAPS).

And I just wonder: when in a proof the goal is:

   \A x \in A : P (A a set, P an action),

and then you have the step:

   TAKE x \in A,

what is the status of x?

I bet for a rigid variable (see p. 6). (The other possibility would be a variable neither rigid nor flexible but I don't think so.)

I think the "only" difference between a flexible and a rigid variable only consists in their semantic interpretation (p. 34)
"sequences of state functions" versus "elements of Val" and in the way of quantifying them: \AA \EE versus \A \E.

--
FL

[Stephan Merz]

> On 27 Nov 2016, at 19:09, 'fl' via tlaplus <tla...@googlegroups.com> wrote:
>
>
> I've just read Leslie Lamport's "Temporal Logic of Actions" ACM Transactions on Programming Languages and Systems, 1994:
>
> http://dl.acm.org/citation.cfm?id=177726
>
> http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-actions.pdf
>
> (I suppose this article is an exact description of what is implemented currently by TLA+ and TLAPS).
>

The TOPLAS paper describes the temporal logic TLA, whereas the specification language TLA+, supported by TLC and TLAPS, combines (Zermelo-Fraenkel) set theory for data structures and TLA for specifying behavior.

> And I just wonder: when in a proof the goal is:
>
> \A x \in A : P (A a set, P an action),
>
> and then you have the step:
>
> TAKE x \in A,
>
> what is the status of x?
>
> I bet for a rigid variable (see p. 6). (The other possibility would be a variable neither rigid nor flexible but I don't think so.)

Yes, variables introduced by TAKE are rigid. TLAPS has no support so far for the quantifiers \AA and \EE.

Best regards,

Stephan

[fl]

Hi Stephan,

thank you for this confirmation.

--

FL 

[fl]

 

The TOPLAS paper describes the temporal logic TLA,

And by the way : what has been added by Leslie Lamport to what had been discovered by Pnuelli?

The actions I guess: a certain way of combining primed and unprimed flexible variables.

But how could Pnuelli  manage an algorithm  without them?

--

FL

[Ioannis Filippidis]

Hi FL,

A few comments that come to my mind about comparing TLA(+) to LTL,
certainly an incomplete answer:


1) Sec.10.2.3 "Temporal logics" from [3] compares TLA to other temporal logics.
Quoting part of it:

"All logics that include existential quantification over flexible variables in principle
have essentially the same expressive power. TLA can express all formulas invariant
under stuttering that Manna and Pnueli’s logic can.  However, their logic can
also express formulas that are not invariant under stuttering. Such formulas yield
specifications that cannot be refined. Although all TLA formulas are expressible
in Manna and Pnueli’s logic, there is no simple translation from TLA to their logic
because its quantification operator is not invariant under stuttering."


2) By using the next operator (\X below),
and if we assumed that LTL was untyped (if it was formally defined, as TLA+ is)
then I think we can rewrite actions as follows:

TLA+: [][ x' = x + 1 ]_x
LTL: []( (\X x) = x + 1 ) \/ (\X x = x) )

However, LTL with types raises other concerns (Note 14 in [3], and [6, 8]).


3) LTL doesn't prevent one from writing stutter-sensitive properties.
TLA formulae are "by construction" stutter-invariant.
A paper relevant to this topic is [2].


4) Temporal quantification in TLA is defined so as to ensure stutter-invariance.
In LTL with temporal quantification (QPTL), this is not the case.


5) Stutter invariance is quite convenient when reasoning about whether
one formula implements (implies) another.

If one rewrites the two formulae in LTL (No.2 above),
then hiding won't work properly without defining temporal
quantification so that it allow stuttering. Altering LTL to define such an
operator essentially is like re-creating a version of TLA using different
notation.

Without some version of \EE, I think that one could try to rename all the
variables that appear in both low and high level formulae to avoid conflicts,
and then prove that one implies the other, but that wouldn't be the
right mathematical description of hiding (it would leave internal  variables visible).
(related to rule E2, Fig.9 [3], see also Sec.5 [4])

Without ensuring that all LTL formulae involved are stutter-invariant,
reasoning about (step) refinement can become more complicated [5].


6) TLA does not encourage a variety of temporal operators,
guiding people to write specifications that others are more likely to understand.
One can still use history variables and temporal quantification to
express what in LTL is expressed with "until" and other operators.
But, it is more direct to use history variables related to the problem at
hand. This way, nesting of temporal operators is not common practice.
See also Secs.8.9.6 and 8.9.5, p.116 [1], Sec.10.2.3 [3].


7) Temporal logic was studied also earlier by philosophers,
   in particular Arthur Prior [7].


[1] Leslie Lamport, "Specifying systems", Addison-Wesley, 2002
    https://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf

[2] Stephan Merz, "A more complete TLA", FM, 1999
    https://members.loria.fr/SMerz/papers/gtla.html
    http://dl.acm.org/citation.cfm?id=730638

[3] Leslie Lamport, "The temporal logic of actions", TOPLAS, 1994
    https://doi.org/10.1145/177492.177726

[4] Leslie Lamport, "Composition: A way to make proofs harder", COMPOS, 1997
    https://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#lamport-composition

[5] Amir Pnueli, "System specification and refinement in temporal logic",
    FSTTCS, 1992
    http://link.springer.com/chapter/10.1007/3-540-56287-7_92
    http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.6060

[6] Leslie Lamport, Lawrence C. Paulson
    "Should your specification language be typed?", TOPLAS, 1999
    https://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#lamport-types

[7] https://en.wikipedia.org/wiki/Temporal_logic

[8] https://groups.google.com/d/msg/tlaplus/N2NYc-xwQ4U/MFf1quC858MJ


Best regards,
ioannis

[fl]

Hi Ioannis,

Thank you for this long answer. I will study it carefully.

--

FL

[Leslie Lamport]

I'm sorry for my two incomprehensible posting.  I accidentally left off the beginning of the first one when I copied it.  I corrected it on the Web site, but the correction did not get emailed.  So, I will try to delete the original from the site.  Meanwhile, when trying to send this, the Web page acted very bizarrely and I wound up sending the second, brief and incomprehensible resend of fl’s previous posting.   Here is the complete first message.

 

Ioannis wrote that one could write [][ x' = x + 1 ]_x in LTL using the next operator \X as

 

(*)   []( (\X x) = x + 1 ) \/ ((\X x) = x) )

 

That's not true in ordinary LTL, in which \X is an operator on formulas, not on expressions.  At one point, I believe that Manna and Pnueli introduced \X on expressions (they wrote \X as a circle) by defining (*) to be an abbreviation for something like

 

   [] (\A a : (x=a) => \X(x = a+1) \/ \X(x = a))

 

I presume this never went very far because having to reason about the translation would have been a nightmare. 

 

FL asked how Pnueli could express an algorithm without using the prime operator.  Given that Manna and Pnueli did introduce the prime notation, except writing \X y instead of y', it's interesting that they didn't see how easily algorithms could be described with it and then develop TLA instead of using \X as an abbreviation for writing complicated formulas.  I wonder if the reason is as simple as \X y  not being as good a notation as y'.

In any event, the answer to FL's question is that Manna and Pnueli didn't express algorithms with LTL. They used something like a programming language (I think it was called Step) to write algorithms, and then expressed correctness properties in LTL. They used a model checker that worked like TLC--describing the algorithm as a state-machine and generating its state/transition graph, and then checking if the behaviors determined by that graph satisfied the temporal-logic properties.

 

Leslie

 

[fl]

 

FL asked how Pnueli could express an algorithm without using the prime operator.  Given that Manna and Pnueli did introduce the prime notation, except writing \X y instead of y', it's interesting that they didn't see how easily algorithms could be described with it and then develop TLA instead of using \X as an abbreviation for writing complicated formulas.  I wonder if the reason is as simple as \X y  not being as good a notation as y'.

Every mathematical discovery is a collaboration. The decimal notation of numbers looks rather natural but if you compare

it with the ancient methods, like the Roman one, it turns out that the easy way was not the first one that was

 found. The same story holds true for the propositional calculus. It looks rather silly for us but Leibniz was never

able to design it, even if he provably looked for it .

And the question of the notation as a brake on the emergence of the right theory deserves  to be taken into consideration.

 

In any event, the answer to FL's question is that Manna and Pnueli didn't express algorithms with LTL. They used something like a programming language (I think it was called Step) to write algorithms, and then expressed correctness properties in LTL. They used a model checker that worked like TLC--describing the algorithm as a state-machine and generating its state/transition graph, and then checking if the behaviors determined by that graph satisfied the temporal-logic properties.

It is complicated indeed.

--

FL 

[fl]

Every mathematical discovery is a collaboration. The decimal notation of numbers looks rather natural but if you compare

it with the ancient methods, like the Roman one, it turns out that the easy way was not the first one that was

 found.

It just comes to my mind that if the Romans never found the decimal notation it is because they used an abacus (or an equivalent device)

to make their calculations. But the decimal notation is only welcome when you use the "algorithm", I mean the "schoolbook

addition".

It is parallel to your idea about notation.

--

FL