LoTREC Support for Model-Checking
Introduction
LoTREC 2.0 has the ability to
perform model checking for normal modal logics. It checks the satisfiability of
a given logical formula in a given Kripke model. This is exactly what we
do with most recent model checkers, except that LoTREC don't cover all problem
types for the moment. Even though, the fact of implementing model-checking under
LoTREC still interesting for two reasons:
- LoTREC is a generic theorem prover and it is not designed to perform such
tests.
- The model-checking is implemented using the high level meta language of LoTREC
without the addition of any line of code. This demonstrates the power and the
extensibility of this simple and expressive language.
Rules and strategy for model-checking
The strategy of model-checking
consists of four main stages:
1- Model construction.
2- Formula analysis by the propagation of the question "is it sat this
formula?".
3- Response formation.
4- Response synthesis until the original formula.
The first rule to applicate is buildModel. It constructs the user's Kripke model. As it is known, a kripke model is a set of nodes (i.e. worlds) linked by arrows (i.e. relations) and such that each node contains a finite set of literals [p, q, r...] (indicating the truth value of literals in each world).
To build a model you will need
to use just three actions:
- createNewNode <node>
- link <node1>
<node2> <relation>
- add <node>
<expression>
The buildModel rule will have the following schema:
rule buildModel
if isNewNode node0
//world creation
do createNewNode node1
do link node0 node1 (R)
do createNewNode node2
do link node0 node2 (R)
do createNewNode node3
do link node1 node3 (R)
do createNewNode node4
do link node1 node4 (R)
//literal evaluation in each world
do add node0 (constant p)
do add node1 (constant p)
do add node2 (not (constant p))
do add node3 (not (constant p))
do add node4 (not (constant p))
end
The constructed model will be like this:
Fig.1 Building a model with LoTREC
The second stage of the strategy consists of the analysis of the given formula, by the propagation of the question "is it sat this formula?", departing from the root node and until the leaf nodes or the nodes where we get no more complex formulae (i.e. where we get atomic formulae or literals).
Next we begin to generate the response in order to propagate it finally to the root node and then we will have the response for the original formula.
We give here the list of connectors and rules and the strategy defining model-checking under LoTREC.
Example
We give here a short example. We want to check the satisfiability of the formula "not(nec(not(nec(not((not(p) and p))))))" in the above model (Fig.1).
The checking operation will pass through the three stages of the model-checking strategy as it is shown in the following diagrams:
Fig.2 Formula analysis
Fig.3 Response formation
Fig.4 Response propagation