A forum for Spin users
You are not logged in.
Pages: 1
I see. What I do not like about this approach is that it puts so much responsibility on the user. The user has to decide whether something is a safety or liveness property, and if neither, either (manually) split the formula into a safety and a liveness formulas, or use -a anyway. Maybe I haven't thought about this enough, but what I meant by "in terms of infinite sequences of states and automata" not being (directly) applicable here is that it seems difficult (or at least not easy) to decide whether an arbitrarily LTL formula is a safety or liveness formula based on those definitions. For example, I have not been able to find a simple syntax-based procedure that can be used to decide whether a formula is a safety or liveness formula. Maybe in practice it's often obvious and the informal definitions are enough, but there are always corner cases and intuition is not always reliable.
Thanks for the link, but, the characterization of safety and liveness in that paper is in terms of infinite sequences of states and automata, and according to the paper safety and liveness properties are the only properties only in the sense that any property can be decomposed into an intersection of a safety and a liveness property. To me it doesn’t seem to (directly) apply to this situation, because here we only have an LTL formula.
Apparently there’s an analogous decomposition theorem for LTL [1], but it doesn’t seem very practical either.
Maybe this isn’t a problem in practice, but: One can use -a to check (any) LTL formula, but as omitting -a is faster one wants to omit -a in as many cases as possible. One then wonders, how do we know when this is possible?
I assume that one sound approach would be to use -a by default, and omit it if one for some reason know that the property one is checking is a safety property (in an informal sense, I guess).
(A note to other people following this thread: In my first post I mentioned that I was confused about the asserts in the never claim. This is only a way to get more debug information out of a failed verification I think, the asserts could be replaced by a jump to the end of the never claim … given this, then the correspondence between automata and never claims are no longer unclear.)
[1] http://www.sciencedirect.com/science/article/pii/S0020019014000386
Hm, for what definition of safety and liveness? If we have a safety property S and a liveness property L, it's not immediately clear what kind of property S&&L or S||L are (at least not to me).
Hej! First some context: In Principles of the Spin Model Checker we are told in chapter 4, “Verification with Temporal Logic”, that we can invoke pan without any arguments to check LTL safety properties. We are then told that pan must be invoked with -a to check liveness properties (to search for cycles). We are, however, as far as I can see, not told how to verify properties that are neither safety nor liveness properties.
I know that LTL properties are translated into never claims by a preprocessing step before verification. And never claims are equivalent to Büchi automata. I also know, from reading The Spin Model Checker: Primer and Reference, that pan does a DF-search when invoked without any flags, and a nested DF-search (to find acceptance cycles) when invoked with the -a flag.
This is where I get confused. In the automata-theoretic description on how to model check LTL properties I’ve seen we always check for acceptance cycles in some automata construction (based on a system model + negation of a property to check). We do not care about what kind of property it is, we always check for an acceptance cycle. But in Spin what kind of property we want to check is apparently important (because we need to know whether to include the -a flag or not)!
If we inspect a never claim translation of a property that is “obviously” a safety property such as []p (where p is a boolean variable) we see that the never claim is based on asserts rather than acceptance cycles. And []p && <>q (that is, a property that is neither a safety nor liveness claim as far as I can see) is translated into some mix of asserts and acceptance cycles.
My problem is that I do not understand how these asserts fit in into the automata-theoretic framework. They make it confusing regarding how to model check properties in general. I assume that the -a mode can be used to check all properties (including safety properties), because if no acceptance states are found in the "outer search" in the search it's basically the same search as the standard DF-search. But this makes it unclear why the standard DF-search is needed at all. I assume it has something to do with performance in some way I cannot see based only on the simplified descriptions of the algorithms in the Spin reference book?
And: Does Spin have any opinions about what is considered a safety property and what is considered a liveness property or are these notions only informal?
Sorry for a long and rambling post, and if I'm being unclear.
Pages: 1