Spinroot

A forum for Spin users

You are not logged in.

#1 2019-04-10 11:45:43

marc15
Member
Registered: 2019-02-07
Posts: 17

sequences in ltl

a model with
bit a,b,c,d,e,f,g

what is the best LTL way to express and test, if c,d,e are getting true in sequence AND
not "being interrupted" by an event with setting a,b,f or g true?

so the combination of a,b,f,g before c = 1
d=1
e=1
should be the same as behind e = 1

Offline

#2 2019-04-10 16:13:17

spinroot
forum
Registered: 2010-11-18
Posts: 636
Website

Re: sequences in ltl

This is difficult to express in LTL (though not impossible), because you'd have to use deeply nested until clauses.
It would be relatively straightforward to express directly as a never claim though.
Assuming you'd want to find a trace matching the behavior you describe (rather than traces deviating from it), something like:

#define INV    (!a && !b && !f && !g)

never {
    do
    :: !c && INV
    :: c && INV -> break
    od
    do
    :: !d && INV
    :: d && INV -> break
    od
    do
    :: !e && INV
    :: e && INV -> break
    od
}

Offline

#3 2019-04-10 20:09:18

marc15
Member
Registered: 2019-02-07
Posts: 17

Re: sequences in ltl

Thank you very much!!

    But what, if sum of a,b,f,g is 2 or 3 before c = 1?

Offline

#4 2019-04-10 23:08:33

spinroot
forum
Registered: 2010-11-18
Posts: 636
Website

Re: sequences in ltl

you can adjust the definition of INV to match what values you need for a, b, f, and g

Offline

#5 2019-04-11 05:44:22

marc15
Member
Registered: 2019-02-07
Posts: 17

Re: sequences in ltl

before the process starts INV is not known, the combination of a,b,f,g before c = 1 is not deterministic or at least unknown

Offline

#6 2019-04-11 11:39:44

marc15
Member
Registered: 2019-02-07
Posts: 17

Re: sequences in ltl

not sure, but I think this could be a solution, in any case, it's good I cannot specify the future :-)
(I had problems with precedence from c to e. Moreover, how can the first part of l1 formulae be shortened?)

#define seq (c && d && e)
#define seqneg (!c && !d && !e)

/* M |= l1 */
ltl l1 {
    (
       ((!a U seq)||(seqneg U a))
    && ((!b U seq)||(seqneg U b))
    && ((!f U seq)||(seqneg U f))
    && ((!g U seq)||(seqneg U g))
    /* c before d && d before e*/
    && ((!d U c) && (!e U d) && (true U e))
    )
}

Offline

#7 2019-04-11 18:53:25

spinroot
forum
Registered: 2010-11-18
Posts: 636
Website

Re: sequences in ltl

not sure if this captures the values of a, b, f, g that must remain constant?
you could set those values in the first "break" transition in auxiliary variables, to "remember" what the values should be
(in and atomic or d_step):
   do
   :: !c
   :: atomic { c -> val_a = a; val_b = b; val_f = f; val_g = g; break }
   od
and then use the rememberver values in the invariant clause for the following transitions....

Offline

#8 2019-04-11 21:54:21

marc15
Member
Registered: 2019-02-07
Posts: 17

Re: sequences in ltl

yes, that was the missing link, thank you!!

not sure about liveness and safety, actually, stupid question: is not liveness in ltl-formulae getting safety in a never claim?

another question, c,d,e, just the sequence, independent of a,b,f,g: how would the perfect ltl-formulae be with nested UNTIL? (without a,b,f,g)

bit val_a, val_b,val_f,val_g
never  {
    do
    ::!c
    ::e||d -> goto no_accept
    ::atomic { c -> val_a = a; val_b = b; val_f = f; val_g = g; break }
    od
    #define INV (val_a!=a)||(val_b!=b)||(val_f!=f)||(val_g!=g)
    do
    ::e||INV -> goto no_accept
    ::d-> break
    od
    do
    ::INV -> goto no_accept
    ::e-> break
    od
    do
    ::skip
    od
    /* is it a safety property? if yes, acceptance cycle is not needed?*/
    no_accept: skip
}

Offline

#9 2019-04-11 22:06:16

spinroot
forum
Registered: 2010-11-18
Posts: 636
Website

Re: sequences in ltl

for a liveness property the (generated or handwritten) never claim will have accept-state labels and the matching executions contain a cycle.  for a safety property that's not the case (it's a state property, not a cycle of states).
so a liveness property expressed in ltl will still be a liveness property when formalized as a never claim.
LTL defines a subset of all omega regular properties -- a never claim (i.e., a Buchi automaton) can express all omega-regular properties -- not just what's expressable in LTL.
In ltl you cannot do the assignments that I showed in the example, so that would be a non-starter.
So, I don't know how you could express the same property in LTL -- perhaps you cannot....

Offline

#10 2019-04-12 09:59:26

marc15
Member
Registered: 2019-02-07
Posts: 17

Re: sequences in ltl

thank you very much!!

#define p (<>x) (Liveness)
M |= p
!p <=> Never claim

so !p is still a liveness property, because !p would be a cycle in absence of x, or in other words, must be a cycle to show there is no x

"The negation of a liveness property is a safety property." == false

I think I got it now :-)

//////////////////////
ltl, yes, of course, assignments in ltl are not possible,
but I wanted to ask, additionally, how do you express a sequence of x,y,z in ltl?
(!y U x) && (!z U y) && (true U z)
you wrote there is a nested solution, but how does it look in detail?

Offline

#11 2019-04-12 16:48:43

spinroot
forum
Registered: 2010-11-18
Posts: 636
Website

Re: sequences in ltl

the negation of a liveness property *can* be a safety property -- but that's not always the case.

for the sequence properties probably this website can be helpful: http://patterns.projects.cs.ksu.edu/documentation/patterns/ltl.shtml

Offline

Board footer

Powered by FluxBB