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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Wed, 30 Nov 2016 14:52:00 -0800 (PST)*References*: <e4123a8c-3214-4eac-9a84-60d10fe34168@googlegroups.com>

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

**Follow-Ups**:**Re: Rigid and flexible variables***From:*fl

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

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