CODEWITHSUNDEEP
logicmodel-checkingnusmv
Nicola Gigante
Nicola Gigante

Reputation: 3266

How to check LTL satisfiability using NuSMV?

I'm trying to use NuSMV as a satisfiability checker for LTL formulae, i.e. I want to know if there exist a model for a given formula. I know that NuSMV can be used for this purpose as well, both because it is theoretically possible and because I see it cited in a lot of papers that deal with satisfiability (one of them claims also that NuSMV is one of the fastest satisfiability checkers out there).

I see that with NuSMV comes a tool called ltl2smv that apparently translates an LTL formula into an SMV module, but then I don't know how to use the output. Giving it directly to NuSMV gives back an error message about "main" being undefined, so I suppose I have to define a main module and use the other in some way. Since I've never used NuSMV as a model checker I have no idea how its language works and the User Guide is overwhelming given that I only need this specific use case, which, by the way, is not mentioned anywhere in said guide.

So how can I use NuSMV to check the satisfiability of an LTL formula? Is there a place where this use case is documented?

Upvotes: 3

Views: 1505

Answers (2)

gmatht
gmatht

Reputation: 835

One way is to use PolSAT. This takes as input an LTL formula, and feeds it to a number of different LTL solvers. This is usually faster than just using NuSMV alone. If you replace the NuSMV binary with /bin/false and run ./polsat 'Gp & F X ~ p' it will abort and leave behind a file ../NuSMV/tmpin.smv containing something like:

MODULE main
VAR
Gp:boolean;
p:boolean;
LTLSPEC
!(((Gp)&(F (X (!(p))))))

(Note that PolSAT interpreted Gp as a single variable). You can then run NuSMV directly with the command ../NuSMV/nusmv/NuSMV < ../NuSMV/tmpin.smv.

If you want to install PolSAT, it can presently be downloaded from https://lab301.cn/home/pages/lijianwen/. v0.1 has a bit of difficulty on modern machines, you may need to downgrade bison to version 2.7 (See e.g. https://askubuntu.com/questions/444982/install-bison-2-7-in-ubuntu-14-04).

Upvotes: 0

danielp
danielp

Reputation: 1187

Have a look at the chapter about LTL model checking in NuSMV's user manual. It comes with an example how LTL specifications can be expressed in a module and checked:

MODULE main
  VAR
    ...
  ASSIGN
    ...
  LTLSPEC <LTL specification 1>
  LTLSPEC <LTL specification 2>
...

NuSMV checks if the specifications hold for all possible paths. To check if there exists a model (i.e. path) for your formula, you can enter the negation and the model checker will give you a counter-example for it if it exists. The counter-example would then be an example for your original formula.

Upvotes: 4

Related Questions