A forum for Spin users

You are not logged in.

- Topics: Active | Unanswered

Pages: **1**

**älgbjörn****Member**- Registered: 2016-09-30
- Posts: 4

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.

Offline

all ltl properties are either safety or liveness properties -- there is no other type than these two.

the main reason for restricting to a single dfs when search for safety properties is that it is more efficient.

Offline

**älgbjörn****Member**- Registered: 2016-09-30
- Posts: 4

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).

Offline

**älgbjörn****Member**- Registered: 2016-09-30
- Posts: 4

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

Offline

Yes, temporal logic, and specifically linear temporal logic, is defined over infinite sequences.

(You can read more about this in my book, where these things are explained in detail. Also how finite sequences can be interpreted as special cases of infinite sequence using stuttering semantics -- which is part of the standard theory that underlies Spin.)

So any LTL formula that you can specify in Spin can be split into a safety property and/or a liveness property. And, the key thing is that there isn't any other type of property than those two main categories.

You're right that one could just always use pan option -a, to make sure that liveness is property checked -- but it would be overkill if all you want to check is a safety property (which is perhaps 90% of what people use model checkers for). So such a default would be a bit wasteful of your scarce computational resources.

Offline

**älgbjörn****Member**- Registered: 2016-09-30
- Posts: 4

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.

Offline

**marc15****Member**- Registered: 2019-02-07
- Posts: 34

I'm still confused,

#define p ([](x -> (a U y)))

p is not(safe) and not(live) but it can be REpresented by an intersection of a live and a safe property?

https://cstheory.stackexchange.com/questions/29400/ltl-property-safety-or-liveness

Offline

a simple way to check if a property is a liveness property is to generate the Buchi automaton from it:

spin -f '[] (x -> (a U y))' which produces this result:

never { /* [] (x -> (a U y)) */

T0_init:

do

:: (((! ((x))) || ((y)))) -> goto accept_S20

:: ((a)) -> goto T0_S27

od;

accept_S20:

do

:: (((! ((x))) || ((y)))) -> goto T0_init

:: ((a)) -> goto T0_S27

od;

accept_S27:

do

:: ((y)) -> goto T0_init

:: ((a)) -> goto T0_S27

od;

T0_S27:

do

:: ((y)) -> goto accept_S20

:: ((a)) -> goto T0_S27

:: ((a) && (y)) -> goto accept_S27

od;

}

the accept states are omega-acceptance states, which means that this is a liveness property.

another way to think about this is to see what type of execution could be be accepted by the automaton: if it can only be an infinite execution then it is a liveness property. if it can be a finite execution, then it is a safety property.

In this case both the property and its negation are liveness properties.

Offline

**marc15****Member**- Registered: 2019-02-07
- Posts: 34

oah, perhaps (at least :- ) one step back,

property shall be <>a (Liveness)

'negation' !(<>a) <=> []!a (Safety)

SPIN looks for an intersection of automata M and 'negation',

if intersection is empty, then M |=property,

(2) if intersection is not empty, SPIN found a counterexample (there is a state found, where M does not hold the property)

to my surprise, for the property <>a the counterexample is with 'START OF CYCLE' (so there was another negation?)

so I'm completely wrong when I thought the counterexample is the result

from step (2)?

Offline

if you specify the property inline with the prefix "ltl name ...

then the negation (to find a counter-example) happens by default.

if on the other hand you specify it as a never claim (using spin -f ...) then

it is as you specify it, and spin finds the matching behavior (i.e., you have

to do the negation if you want a counter-example)

so if you specify inline ltl p <> a then spin looks for a counter-example by

using the buchi automaton for []!a

Offline

**marc15****Member**- Registered: 2019-02-07
- Posts: 34

yes, that was my thinking,

but why is the counterexample with "START OF CYCLE" ?

it is stating there was an intersection of automaton M and 'negation' with liveness,

but the 'negation' of <>a is safety

where is my mistake?

Offline

**marc15****Member**- Registered: 2019-02-07
- Posts: 34

I've specified the inline ltl-property prop with <>a

the promela model incl. inline ltl-property is:

//////////////////////////////////////////////////////////

/* file.pml */

bit x,a,y

active proctype seq1(){

x = 1

}

active proctype seq2(){

a = 0

y = 1

}

ltl prop {<>a}

//////////////////////////////////////////////////////////

the output for 'spin -run -a file.pml' is

//////////////////////////////////////////////////////////

ltl prop: <> (a)

pan:1: acceptance cycle (at depth 10)

pan: wrote promela_translation.pml.trail

(Spin Version 6.4.8 -- 2 March 2018)

Warning: Search not completed

+ Partial Order Reduction

Full statespace search for:

never claim + (ltl_0)

assertion violations + (if within scope of claim)

acceptance cycles + (fairness disabled)

invalid end states - (disabled by never claim)

State-vector 28 byte, depth reached 11, errors: 1

6 states, stored

0 states, matched

6 transitions (= stored+matched)

0 atomic steps

hash conflicts: 0 (resolved)

Stats on memory usage (in Megabytes):

0.000 equivalent memory usage for states (stored*(State-vector + overhead))

0.292 actual memory usage for states

128.000 memory used for hash table (-w24)

0.534 memory used for DFS stack (-m10000)

128.730 total actual memory usage

pan: elapsed time 0 seconds

//////////////////////////////////////////////////////////

the counterexample with ./pan -r -v :

//////////////////////////////////////////////////////////

depth 1: Claim, state 3 (line 4)

1: proc 0 (ltl_0) file.pml:4 (state 3) trans {5,3} [(!(a))]

global vars:

bit a: 0

2: proc 2 (seq2) file.pml:9 (state 1) trans {2,5} [a = 0]

global vars:

bit a: 0

3: proc 0 (ltl_0) file.pml:4 (state 3) trans {5,3} [(!(a))]

global vars:

bit a: 0

4: proc 2 (seq2) file.pml:10 (state 2) trans {3,6} [y = 1]

global vars:

bit a: 0

5: proc 0 (ltl_0) file.pml:4 (state 3) trans {5,3} [(!(a))]

global vars:

bit a: 0

6: proc 2 (seq2) -:0 (state 0) trans {4,7} [-end-]

global vars:

bit a: 0

7: proc 0 (ltl_0) file.pml:4 (state 3) trans {5,3} [(!(a))]

global vars:

bit a: 0

8: proc 1 (seq1) file.pml:4 (state 1) trans {0,8} [x = 1]

global vars:

bit a: 0

9: proc 0 (ltl_0) file.pml:4 (state 3) trans {5,3} [(!(a))]

global vars:

bit a: 0

10: proc 1 (seq1) -:0 (state 0) trans {1,9} [-end-]

global vars:

bit a: 0

<<<<<START OF CYCLE>>>>>

11: proc 0 (ltl_0) file.pml:4 (state 3) trans {5,3} [(!(a))]

global vars:

bit a: 0

12: proc 0 (ltl_0) file.pml:4 (state 3) trans {5,3} [(!(a))]

global vars:

bit a: 0

spin: trail ends after 12 steps

#processes 1:

12: proc 0 (ltl_0) file.pml:4 (state 3) (invalid end state)

(!(a))

global vars:

bit a: 0

//////////////////////////////////////////////////////////

"START OF CYCLE" inside the counterexample is confusing me, because the negation of the inline ltl-property <>a is safety.

But why is then "START OF CYCLE" there? (<=> SPIN output 'pan:1: acceptance cycle (at depth 10)')

the never claim for the negation of the inline ltl-property is

never { /* []!a */

accept_init:

T0_init:

do

:: (! ((a))) -> goto T0_init

od;

}

Is there really a pattern to tell safety in a never claim?

Offline

Okay -- the ltl inline property is considered a positive property: you claim this to be true.

So spin generates the negation !<>a = [](!a) which can generate a counter-example if it can find an execution where a stays false forever. The claim generated from the negated property is:

$ spin -f '!<>a'

never { /* !<>a */

accept_init:

T0_init:

do

:: (! ((a))) -> goto T0_init

od;

}

and you see that this is now expressed as a liveness property: any infinite sequence where 'a' remains false.

There could in principle be executions (though not in this case) where 'a' eventually becomes true, but as long as there is at least one execution where 'a' can remain false, Spin can find it and report it.

Ltl is defined over executions (runs), so it's not a branching logic like Ctl.

You can express the stronger safety property that 'a' is invariant directly in a never claim as:

never {

do

:: assert(!a)

od

}

Never claims formalize general omega regular properties (anything expressible in a Buchi automaton), which is a broader class of properties than what can be formalized in LTL alone.

Offline

**marc15****Member**- Registered: 2019-02-07
- Posts: 34

Thank you very much!!!

Offline

Pages: **1**