1

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.

Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
Ranjana N
  • 59
  • 5

1 Answers1

0

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.

Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
  • @RanjanaN You are welcome. I apologize for not including a hands-on example in my answer, I don't have `nuXmv` on this system. – Patrick Trentin Jan 12 '19 at 07:21
  • I have been searching for some documentation on examples of msat (infinite domain cases) based property checking on NuXMV. Will share if I can build some concrete examples. I may need to ask some more questions till I get the hang of it. – Ranjana N Jan 12 '19 at 07:35
  • Glad to find the quick explanation. Helps in continuing. – Ranjana N Jan 12 '19 at 07:36
  • 1
    @RanjanaN There might a couple of (toy) examples using `msat_...` functionality among the exercises solutions [here](http://www.patricktrentin.com/pages/fm2018.html). – Patrick Trentin Jan 12 '19 at 08:44
  • Just went through the web page. It is informative. Tried dining philosphers example. All properties are true with check property as well as msat_check.... I tried one of my own example. The check_property gives a counter example of 13 states, whereas msat_check.... gives only one state as counterexample. What could be explanation to this? – Ranjana N Jan 12 '19 at 09:04
  • 1
    @RanjanaN being unable to run `nuXmv`, I can only guess. It would help if you created a new question with the model and both output traces, so I can see the same data you see now. – Patrick Trentin Jan 12 '19 at 09:13
  • Sure would do that. – Ranjana N Jan 12 '19 at 09:19