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

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Fri, 2 Dec 2016 04:30:00 -0800 (PST)*References*: <e4123a8c-3214-4eac-9a84-60d10fe34168@googlegroups.com> <480442a3-f977-4b29-9291-27ca22a52224@googlegroups.com>

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

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

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

**Re: Rigid and flexible variables***From:*Leslie Lamport

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