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

*From*: Ioannis Filippidis <jfili...@xxxxxxxxx>*Date*: Tue, 29 Nov 2016 10:45:42 -0800 (PST)*References*: <e4123a8c-3214-4eac-9a84-60d10fe34168@googlegroups.com> <22770D7A-793F-4B75-8770-4469432D7BCC@gmail.com> <b8c7514a-6626-45d0-b62c-0177287906d7@googlegroups.com>

On Tuesday, November 29, 2016 at 6:55:35 AM UTC-8, fl wrote:

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

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

**Follow-Ups**:

**References**:**Rigid and flexible variables***From:*fl

**Re: [tlaplus] Rigid and flexible variables***From:*Stephan Merz

**Re: [tlaplus] Rigid and flexible variables***From:*fl

- Prev by Date:
**Re: [tlaplus] Rigid and flexible variables** - Next by Date:
**Re: [tlaplus] Rigid and flexible variables** - Previous by thread:
**Re: [tlaplus] Rigid and flexible variables** - Next by thread:
**Re: [tlaplus] Rigid and flexible variables** - Index(es):