# 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:

#### 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

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

• W is a non-empty set of possible worlds;
• R is a binary relation on W (called accessibility relation).
• l is a function which associates, to each propositional variable p ∈ P, the set of possible worlds from W where p is true.

#### 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 : $\left(\left(p\to ◊q\right)\wedge ◻q\right)$ 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.

problem.intohylo:
```begin
((p1 | p2) & <r1>~ p1 & ~ p1)
end
```
solution.kripke:
```s SATISFIABLE
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:
```s SATISFIABLE
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.
`s UNSATISFIABLE`
Then `mdk-verifier` will answer:
`ERROR: UNSATISFIABLE formulae are not checkable yet.`

#### Spartacus

http://www.ps.uni-saarland.de/spartacus/
Patch

#### InKreSAT

http://www.ps.uni-saarland.de/~kaminski/inkresat/
Patch

#### Km2SAT

http://disi.unitn.it/~rseba/sat06/
Patch

#### StarSAT

http://www.mrg.dist.unige.it/~tac/StarSAT.html
Patch
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`.

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

```    Valentin Montmirail