MoDal logic K : Checker of Modal-SAT solutions

This page is presenting the tool called mdk-verfier which is, with some specifications in the I/O, able to tell if a Kripke model satisfies a formula.

Binaries: Linux Mac OS X View source

Modal Logic K

The language of Modal Logic K is the language of classical propositional logic + 2 unary operators : Diamond (◊) and Box (◻).

A formula of the form ◻φ (box phi) means 'φ is necessarily true', while a formula of the form ◊φ (diamond phi) means 'φ is possibly true'.

Kripke Model

Fig1. - Example of a Kripke model.

Let a non-empty countable set of propositional variables P be given.
A Kripke model is a triplet M = <W,R,l>, where:

Modal-SAT problems

A formula φ is satisfiable in K if and only if there exists a Kripke model M = <W,R,l> (with w_0 ∈ W) that satisfies φ.

As one might expect, a software trying to solve this problem may try to find a Kripke model that satisfies the formula given as input.
If such model is found, the software can answer YES (or SAT) and provide the model to justify its answer.

The goal of mdk-verifier is to check, for a formula φ and a model M, if M satisfies φ.

Input Format

For the input format, we choose to use the already existing format InToHyLo.

file         := begin formulas end
formulas     := formula | formula ; formulas
formula      := true | false | proposition | negation | conjunction | disjunction | implication | dimplication | box | diamond | ( formula )
proposition  := p number
relation     := r number
negation     := ~ formula
conjunction  := formula & formula 
disjunction  := formula | formula 
implication  := formula -> formula
dimplication := formula <-> formula
box          := [relation] formula
diamond      :=  <relation> formula
Example : ( ( p q ) q ) should be written in InToHyLo : begin ((p1 -> <r1>p2) & [r1]p2 ) end

Output Format

For the output, we decide to create a representation of a Kripke model in order to be able to check solvers answers. Here is an example:

2 3 1 2
-1 2 0
1 2 0
1 -2 0
r1 w0 w1
r1 w1 w2
The first line contains exactly four integers separated by spaces. They provide respectively the number of propositional variables, the number of possible worlds, the number of relations, (which will be useful in the future for multi-modal problems), and the number of edges in the model.
In the subsequent lines, each propositional variable is represented by a positive integer. For example, if there exists 3 propositional variables in the model, then they are named 1, 2 and 3.
The second line corresponds to the valuation of the first possible world (i.e. w_0). The third line corresponds to the valuation of the second possible world (w_1), and so on.

Each of these lines follows the DIMACS format: the integer i means that the propositional variable i is true in that world and −i means that the propositional variable i is false in that world.
There must be exactly one valuation line for each possible world in the model. Each of these lines must end with a 0.
After that, the connections between worlds are indicated. Each line has the format: rI wJ wK, where I, J and K are integers.

The first one represents the I-th relation of the model, the second one is the J-th possible world and the third one is the K-th world. Each one of these lines means that there is an arrow from w_J to w_K labelled by I in the model.
There must be exactly one such line for each edge of the model.

MDK-verifier call

Example with *SAT:
./starsat ./problem.intohylo > solution.kripke
./mdk-verifier problem.intohylo < solution.kripke 

Let's now see a full example of a call of mdk-verifier and which output we should expect.

((p1 | p2) & <r1>~ p1 & ~ p1)
c #var #worlds #relations #edges
v 2 2 1 1
v -1 2 0 
v -1 0 
v r1 w0 w1
mdk-verifier answer:
OK 2
We can see that there is a possible world accessible from w0 where ~p1 is true, which implies (<r1>~ p1).
We also see that ((p1 | p2) & ~p1)) is true in w0. Then, mdk-verifier concludes that this Kripke model is a solution, and that this solution has 2 worlds (OK 2).

Let's assume that the solver gives an incorrect answer. For example:
c #var #worlds #relations #edges
v 2 2 1 1
v 1 2 0
v -1 0
v r1 w0 w1
Then, we don't have -1 in the world w0 and mdk-verifier answers:
ERROR: model is incorrect
~p1 is not in w_0 but its negation is !

If the solver answers UNSAT.
Then mdk-verifier will answer:
ERROR: UNSATISFIABLE formulae are not checkable yet.




If you want to try mdk-verifier on your own, here are 2 archives of problems and Kripke models, ready to be checked.
Some of this Kripke models are not solutions of their corresponding problem (which has the same filename) and can miss some information.
We provide them on purpose to show the output of mdk-verifier.

InToHyLo problems Kripke-CNF solutions

If you want to see how some of these Kripke models look like, here is an archive of images:

Kripke models (png)

For any additional information about this tool, please feel free to contact

    Valentin Montmirail                               
    Universite d'Artois                           
    CRIL - CNRS UMR 8188
    Rue Jean Souvraz SP 18 62307 Lens FRANCE