model checking on finite trace

[MFaisalZaki]

Hi, I want to implement an LTL path constraint solver, as mentioned in Heuristic Search: Theory and Applications, chapter 13.

The algorithm's idea is to use LTL model checking during a search to generate solutions that satisfy a given formula. I have a problem expressing a sequence of predicates that should become true for a generated trace.

To represent a trace, I created a Kripke structure as follows:

from pyModelChecking import *
from pyModelChecking.CTL import *
from pyModelChecking.LTL import *

K = Kripke(R=[(0,0),(0,1),(1,2),(2,3),(3,3)], L={0: set([]), 1:set(['p']),3:set(['p', 'q'])})

Now, I want to check if this trace satisfies a formula that says 'q' had to occur at some point before 'p' and that both have to hold at the end.

I am new to LTL and am trying to figure out how to express such a sentence into an LTL formula and encode it using 'pyModelChecking'.

[albertocasagrande]

The LTL formula modelling your property is A((~p & ~q) U (~p & q & F(G(p & q)))).

To identify the states satisfying this formula, use the following code after updating the pyModelChecking package (the LTL model checking implementation had an issue).

from pyModelChecking import *
from pyModelChecking.LTL import *

K = Kripke(R=[(0,0),(0,1),(1,2),(2,3),(3,3)],
           L={0: {}, 1:{'p'}, 3:{'p', 'q'}})

phi = 'A((~p & ~q) U ((~p & q) & F(G(p & q))))'

print(modelcheck(K, phi))

As you can see, no state satisfies the above formula. This is because no state satisfies ~p & q.