I am using NuXMV for checking LTL properties using msat_check_ltlspec_bmc command on a fairly large model. The result shows no counterexample found within the given bounds. Do I interpret it as that property is True. Or it can alternatively mean that analysis is not complete.
This is because, by changing the property proposition to true or false, the result is always no counterexample. Most of The results are counterintuitive.
Started with real variables based properties but since unable to understand the result, shifted to Boolean based properties on the same model, using the same command.
Bounded Model Checking is a bug-oriented technique which checks the validity of a property on execution traces up to a given lenght k.
When an execution trace violates a property, great: a bug was found.
Otherwise, (in the general case) the model checking result provides no useful information and it should be treated as such.
In some cases, knowing additional information about the model can help. In particular, if one knows that every execution trace of length k must loop-back to one of the k-1 states, then it is possible to draw stronger conclusions from the lack of counter-examples of length smaller or equal k.