Proving Possibility Properties

One never wants to assert possibility properties as correctness properties of a system. It’s not interesting to know that a system might produce the correct answer. You want to know that it will never produce the wrong answer (safety) and that it eventually will produce an answer (liveness). Typically, possibility properties are used in branching-time logics that cannot express liveness. If you can’t express the liveness property that the system must do something, you can at least show that the system might do it. In particular, process algebras typically can express safety but not liveness.

But the trivial system that does nothing implements any safety property, so process algebraists usually rule out such trivial implementations by requiring bisimulation–meaning that the implementation allows all the same possible behaviors as the specification.

People sometimes argue that possibility properties are important by using the ambiguities of natural language to try to turn a liveness property into a possibility property. For example, they may say that it should be possible for the user of a bank’s ATM to withdraw money from his account. However, upon closer examination, you don’t just want this to be possible. (It’s possible for me to withdraw money from an ATM, even without having an account, if a medium-sized meteorite hits it.) The real condition is that, if the user presses the right sequence of buttons, then he must receive the money.

Since there is no reason to prove possibility properties of a system, I was surprised to learn from Bob Kurshan–a very reasonable person–that he regularly uses his model checker to verify possibility properties. Talking to him, I realized that although verifying possibility properties tells you nothing interesting about a system, it can tell you something interesting about a specification, which is a mathematical model of the system. For example, you don’t need to specify that a user can hit a button on the ATM, because you’re specifying the ATM, not the user. However, we don’t reason about a user interacting with the ATM; we reason about a mathematical model of the user and the ATM. If, in that mathematical model, it were impossible for the button to be pushed, then the model would be wrong. Proving possibility properties can provide sanity checks on the specification. So, I wrote this paper explaining how you can use TLA to prove possibility properties of a specification–even though a linear-time temporal logic like TLA cannot express the notion of possibility.

I originally submitted this paper to a different journal. However, the editor insisted that, to publish the paper, I had to add a discussion about the merits of branching-time versus linear-time logic. I strongly believe that it’s the job of an editor to judge the paper that the author wrote, not to get him to write the paper that the editor wants him to. So, I appealed to the editor-in-chief. After receiving no reply for several months, I withdrew the paper and submitted it to TCS.