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 :

((p \to ◊ q) \land ◻ 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:

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.

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

MoDal logic K : Checker of Modal-SAT solutions

Preliminaries

Modal Logic K

Kripke Model

Modal-SAT problems

I/O Format

Input Format

Output Format

How to use

MDK-verifier call

Supported solvers

Spartacus

InKreSAT

Km2SAT

StarSAT

Examples

Contact