On Tuesday, November 29, 2016 at 6:55:35 AM UTC-8, fl wrote:
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
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