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

[tlaplus] Re: Proving Prefix Safety Properties

Straightforward propositional temporal logic reasoning shows that to prove

   THEOREM  Init /\ [][Next]_vars => [](P => []Q)

it suffices to prove:

   THEOREM  Init /\ [][Next]_vars => []Inv
   THEOREM  P /\ []Inv /\ [][Next]_vars => []Q

both of which are proofs of invariance.



On Thursday, September 24, 2020 at 6:48:42 AM UTC-7 will...@xxxxxxxxx wrote:
To amend an apparent error in my above post, I think that the formula []~(P ~> Q) should actually be [](P => []~Q) to express what I was intending. I guess this teaches me a lesson that expressing non trivial properties in temporal logic can be error prone.

On Sunday, September 13, 2020 at 3:53:41 PM UTC-4, Willy Schultz 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 pointed out in [2], an algorithm's transition behavior depends only on the current state, not on its history of states, 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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ef9f235e-0870-40ad-8193-b5ba5466948cn%40googlegroups.com.