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.LeslieOn 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 NaturalsVARIABLE x, hasBeenOneMInit ==/\ 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.Stephan[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, SequencesVARIABLE x, xHistInit ==/\ 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.