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:
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 : 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.
./starsat ./problem.intohylo > solution.kripke ./mdk-verifier problem.intohylo < solution.kripke
mdk-verifier
and which output we should expect.begin ((p1 | p2) & <r1>~ p1 & ~ p1) endsolution.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 2We can see that there is a possible world accessible from w0 where ~p1 is true, which implies (<r1>~ p1).
mdk-verifier
concludes that this Kripke model is a solution, and that this solution has 2 worlds (OK 2).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 !
s UNSATISFIABLEThen
mdk-verifier
will answer: ERROR: UNSATISFIABLE formulae are not checkable yet.
mdk-verifier
on your own, here are 2 archives of problems and Kripke models, ready to be checked.mdk-verifier
.
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