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.
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-verifierand 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
OK 2We can see that there is a possible world accessible from w0 where ~p1 is true, which implies (<r1>~ p1).
mdk-verifierconcludes 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
ERROR: model is incorrect ~p1 is not in w_0 but its negation is !
ERROR: UNSATISFIABLE formulae are not checkable yet.
mdk-verifieron your own, here are 2 archives of problems and Kripke models, ready to be checked.