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

Re: [tlaplus] Proving Prefix Safety Properties

Thank you Stephan. Proving the property by using your monitor example makes sense to me, but I suppose it doesn't fully resolve my conceptual concern around history variables. Primarily, I was wary that using history variables caused me to fall into a mode of writing proofs based on behavioral reasoning, rather than using state based reasoning. For example, the reason the above specification satisfies the safety property is because of the state it maintains, not because of its history of states. So, to understand why the algorithm is correct, my goal would be to understand why the state it maintains protects any future transitions from violating an invariant. Obviously for this example it's trivial to understand why safety holds, but in examining safety properties of other, more complicated, protocols I have at times been unsure if I properly understood these details correctly. 

In an attempt to formalize my thoughts a bit, consider the following, abbreviated spec:

Init == (x = 1)
Next ==
    /\ x < 2 
    /\ x' = x + 1

My intuition would be that proving that ~(x=1) is an invariant of this spec* is sufficient to prove the original safety property from my original example. More generally, if we want to prove a property specifically of the type []~(P ~> Q) for state predicates P and Q, then we construct a spec where P is the initial state predicate, the next state predicate is the same as the original spec, and prove that ~Q is an invariant of this spec. Since ~Q is simply a state invariant, we can use the standard technique of proving an inductive invariant, without resorting to history variables. Perhaps this approach ends up providing little benefit over a history variable approach, but it is a thought I had when trying to think about how an algorithm maintains a certain "prefix invariance" property even though it doesn't have access to historical state.

* It's not strictly an invariant since it only holds in non initial states, but presumably that could be addressed by explicitly marking initial states with some auxiliary boolean variable.


On Sunday, September 20, 2020 at 12:17:53 PM UTC-4 Leslie Lamport wrote:
To expand on Stephan's remark that using history variables is the standard way of expressing and proving safety properties:  Temporal logic fans will advocate expressing them in some kind of temporal logic, usually involving more expressive operators than [].  This is practical only for simple safety properties.  For more complicated properties, most formalisms have to rely on history variables.  TLA is one of the few formalisms in which you can assert that one system/algorithm/program/... implements another, so it is possible to write the safety property to be verified the same way you write the system.  I regard that as the "standard" way to verify that a system satisfies an arbitrary safety property in TLA.


On Sunday, September 20, 2020 at 12:20:01 AM UTC-7 Stephan Merz wrote:
Any safety property can be expressed as a state invariant about the history of the execution, and I agree that adding history variables is the standard way for expressing and proving such properties.

Alternatively, you could express the property using a specification that monitors the property, and show that your spec refines the monitor. For your example, this could be written as follows: [1]

-------------- MODULE Monitor --------------
EXTENDS Naturals
VARIABLE x, hasBeenOne

MInit == 
  /\ x \in Nat
  /\ hasBeenOne = (x = 1)

MNext ==
  /\ x' \in Nat
  /\ hasBeenOne => x' # 1
  /\ hasBeenOne' = (hasBeenOne \/ (x' = 1))

MSpec == MInit /\ [][MNext]_<<x, hasBeenOne>>

Now, in order to prove that your spec refines (\EE hasBeenOne : MSpec), you will in general need a history variable. For the example that you show in your post, instantiating hasBeenOne by "x >= 1" happens to work.


[1] The conjuncts "x \in Nat" and "x' \in Nat" could be omitted and are included only so that the spec can be checked with TLC.

On 13 Sep 2020, at 21:53, Willy Schultz <will...@xxxxxxxxx> wrote:

My understanding is that it should always be possible to prove a safety property of a specification by finding an inductive invariant [1]. For safety properties that can be expressed as state predicates (i.e. invariants), the technique is clear to me i.e. find an inductive invariant, prove that it holds in the initial state and prove the inductive step. There are some safety properties, however, that cannot be expressed as state predicates. For example, a property such as "x=1 at most once" is a safety property, since it will be violated at a discrete point in the behavior, but its truth value depends on a behavior prefix rather than a single state.

My question is about how one should go about proving a safety property of this form i.e. a safety property that is not a "state invariance" property, but a "prefix invariance" (for lack of a better term) property. I have worked on one specification where I encountered this issue, and it's easy enough to use history variables in that case to remedy the problem. That is, maintain a history variable that stores enough information about the previous states of the current behavior so that a "prefix invariance" property can be expressed as a state predicate on the appropriate history variables. Here's a simple example of using history variables to illustrate the "x=1 at most once" example. (As a possibly related aside, I was also unable to figure out a way to express a property like "x=1 at most once" in TLA+ without using a history variable.)

------------ MODULE history -----------------
EXTENDS Naturals, Sequences


Init == 
    /\ x = 0
    /\ xHist = <<>>

Next ==
    /\ x < 2 
    /\ x' = x + 1
    /\ xHist' = Append(xHist, x+1)

\* Safety property: x = 1 at most once.
Inv == ~(\E i,j \in DOMAIN xHist : i # j /\ xHist[i] = 1 /\ xHist[j] = 1)


From a practical standpoint, this seems to work fine, but I'm curious if there are alternative proof techniques to deal with safety properties of this type. I am slightly confused by the fact that an inductive proof would necessarily require history variables. As Lamport points out, an algorithm's transition behavior depends only on the current state, not on its history of states [2], so if a safety property can be proved by an inductive invariant, it seems like history variables shouldn't be fundamentally needed, since the algorithm itself doesn't have access to these history variables, and yet it manages to uphold the invariant.

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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/91ccc7aa-6a12-4e46-84e0-54c5282d39een%40googlegroups.com.

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6ed2280f-5da5-4a94-ae4e-9a1e7acd626fn%40googlegroups.com.