Checking or proving machine closure of a temporal formula

[Andrew Helwer]

All the proofs of machine closure of a temporal formula I've seen are written outside of TLA, talking about things like prefixes of behaviors and other such things that can't really be expressed inside TLA. So how do you:

1. State "formula F is machine-closed" as a proposition in TLA

2. Write a proof of that theorem using functionality available in TLAPS

3. Alternatively, model-check that F is machine closed over a finite model

Is it possible to do any of these things? Thanks!

Andrew Helwer

[Stephan Merz]

Hi Andrew,

I don’t know an elegant expression of machine closure in TLA+, below is a clumsy way to express the closure of a given formula F. 

For notational simplicity, let’s assume that F contains a single (free) state variable x. I’ll write F(x) to make this explicit, and write F(y) for the formula F with y substituted for x. Let’s start by defining a couple of auxiliary formulas:

H(x,h) == h = << x >> /\ [][x’ # x /\ h’ = Append(h,x’)]_<<x,h>>

The variable h is a history variable that records the previous values of x. Note that both of the following are valid:

\AA x : \EE h : H(x,h)

F(x) <=> \EE h : F(x) /\ H(x,h)

Now we can define the machine closure of F(x) as the formula

CF(x) == \EE hx : 

   /\ H(x, hx)       \* record the values of x as hx

   /\ [](LET n == Len(hx)  \* fix the current length of the history

         IN  \EE y, hy :  \* find a new sequence y and history hy such that

             /\ F(y) /\ H(y,hy)   \* y satisfies F and agrees with x on all values up to step n

             /\ [](\A i \in 1 .. Min(n, Len(hy)) : hy[i] = hx[i]))

Note that, like F(x), CF(x) again has precisely one free state variable x. Now, F is machine closed iff

\AA x, hx : 

    CF(x) /\ H(x,hx) => 

    [](LET n == Len(hx)

       IN  \EE y, hy : F(y) /\ H(y,hy) /\ [](\A i \in 1 .. Min(n, Len(hy)) : hy[i] = hx[i]))

that is, any finite prefix of a behavior satisfying CF can be extended to some behavior satisfying F. Really, all these formulas do is mirror the semantic definitions of machine closure in TLA+, that’s why they are not really satisfactory.

Because no tool supports reasoning about \EE and \AA, I don’t see how to mechanically check machine closure of a formula.

What do you think?

Stephan 

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUVOPq401185sHDHdbgkuZeagncnsTtw9265ZPVdE82MKA%40mail.gmail.com.

[Andrew Helwer]

Thanks, Stephan. I am not very acquainted with reasoning using \EE and \AA (since, as you say, nothing really uses them) but what you have written makes sense. Basically at every index in every x-behavior we try to produce a witness y-behavior satisfying F whose prefix is that x-behavior up to the index being considered. Lamport does say we can do this in his Proving Possibility Properties paper, although doesn't state the formula:

What is a good resource for proof rules for \EE and \AA statements? Like given a proposition which uses \EE or \AA, what suffices as proof of that proposition?

Andrew Helwer

[Stephan Merz]

Hi Andrew,

first of all, the second part of my answer to your original question was really nonsense. When we talk about machine closed specs, we need a pair (S,L) of properties where S is a safety property and L an arbitrary (but typically a liveness) property, and the question is if L adds a safety constraint on top of S. The pair is machine closed if S(x) \equiv CF(x) where CF(x) is the formula defined in the first part of my answer, but with S /\ L substituted for F.

The basic rules for \EE and \AA are the standard quantifier rules such as

(\EE-intro)  F(exp) => \EE x : F(x)           where exp is a state formula

and      

(\EE-elim)  F(y) => G |= (\EE x : F(x)) => G    where y is a fresh (state) variable

However, the introduction rule (which corresponds to refinement mappings) is notoriously incomplete because it only accounts for state-by-state witnesses whereas semantically one quantifiers over an entire behavior. One way to achieve completeness is to supplement these rules by construction for auxiliary (history, stuttering, prophecy) variables as described in [1,2].

Stephan

[1] L. Lamport, S. Merz: Prophecy Made Simple. https://lamport.azurewebsites.net/pubs/pubs.html#simple. 

See also https://lamport.azurewebsites.net/pubs/pubs.html#auxiliary for the TLA+ versions of these rules.

[2] L. Lamport: A Science of Concurrent Programs, ch.7. https://lamport.azurewebsites.net/pubs/pubs.html#science-book