[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Model-Checking



Hi, 
I've been playing  with the PVS model-checker for some days,
and now I've encountered a problem I cannot understand.

I have defined a state type STATE, and a next-state relation N. I want
to check the property AG AF p under the fairness constraint f.

This is formalized as
	 f(s: STATE) = (definition of f, not temporal)
	 p(s: STATE) = (definition of p, not temporal)
	 N(s1,s2: STATE) = (.....)

	 lem: LEMMA FORALL s: AG(N, fairAF(N, p)(f))(s)

I start the model-checker, which does not complete the proof
(unfortunalty, the PVS modelchecker does not compute a
counterexample). 

Now we change the fairness constraint to f':=AG AF f; this should not
change anything (at least in my understeanding of fairness and
temporal operators).

	f'(s: STATE) = AG(N, AF(N, f))

	lem2: LEMMA FORALL s: AG(N, fairAF(N, p)(f'))(s)

Surprisingly, lem2 can be proved by invoking the model-checker. 

Is this a bug in the model-checker, or is my understanding of fairness
and temporal operators wrong?

Thanks, Chris

PS: if you need the actual files, just give me a note.

-- 
----------------------------------------------------------------
                                       FB 14 - Informatik
 Christian Jacobi                      Im Stadtwald
 Computer Science Department           D-66041 Saarbruecken
 Saarland University        			 
 Germany                               Phone: (+49) 681 3024490
                                       Fax:   (+49) 681 3024290
----------------------------------------------------------------