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

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'.

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.

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 φ.

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> formulaExample : $((p\to \u25caq)\wedge \u25fbq)$ should be written in InToHyLo :

`begin ((p1 -> <r1>p2) & [r1]p2 ) end`

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 w2The 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.

./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.begin ((p1 | p2) & <r1>~ p1 & ~ p1) end

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`

OK 2We 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 w1Then, 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 UNSATISFIABLEThen

`mdk-verifier`

will answer: ERROR: UNSATISFIABLE formulae are not checkable yet.

Patch

Patch

Patch

Patch

`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 montmirail@cril.fr.

Valentin Montmirail Universite d'Artois CRIL - CNRS UMR 8188 Rue Jean Souvraz SP 18 62307 Lens FRANCE http://www.cril.fr/~montmirail