MAS: Using Priest Modal Tableaux to Visualise Kripke Models


Chapter 3: Implementation

M. Koonstra S2399385 / G. Schoenmacker s1550748 / Rijksuniversiteit Groningen

Overview

The basis of our implementation is defined to be a four stage process. This chapter mainly focusses on step two, which has been designed for this project.

  1. Parsing the formula string
  2. Using tableau rules to expand the formula
  3. Transforming the tableau into a collapsed model
  4. Rendering the generated model

Step 1: Parsing the formula string

For this project we used the grammar used by OOPS for parsing a formula string. By using SableCC, we can parse the formula string by using a stack based depth first parser into a tree of formula. Classes are defined for each of the operators used in propositional logic: Conjunction, Disjunction, Implication, BiImplication and Negation. These are extended with the model operators: Box, EBox, CBox, Diamond, WorldInstance and WorldRelation. All operators can be defined in the formula string except the WorldInstance and WorldRelation formula, these are used internally during the expansion of the formula. After the formula tree has been generated, it can be added to the tableau.

The language for OOPS has been modified to allow for the C and E operators to be used. These operators use the normal alphanumeric characters, which has the implication that the naming of agents is not possible. Agents can only be named by number. This means that the grammar is not completely compatible with OOPS.

A depth first parser is used to generate the formula tree from the

Step 2: Using tableau rules to expand the formula

A tableau is basically a sheet that holds the formula that are expanded from the initial formula(e). A tableau can contain multiple branches that are to be expanded using the rules used by the model. These branches contains a list of nodes that are on that branch. A node contains a formula and a world in which it holds.

The Expander class is the workhorse for expanding tableaux. The expander class loops through all branches to apply rules to the formulae on that branch. Each branch is expanded until either false can be concluded by having both p and ~p in the branch (where p is any formula). Or if there are no more formula to be expanded and all rules have been applied. Each branch that concludes false is considered a closed branch. Branches that cannot be expanded further are considered open branches. If all branches in the tableau are closed, we can conclude that there is no situation in which the initial formula(e) can be satisfied. The open branches are candidates to visualise, as they are models demonstrating how the (counter-)model can be constructed.

Propositional Rules

For the propositional operators, a rule is defined for each operator defining how to handle the formula. These rules either add new nodes to the branch or they start a new branch (like the Disjunction operator). When a branch is created, the current branch is copied and separated from the current branch. The new branch will be processed later. Consider the following branch:

  1. a > b | c, i

This tree is then branched and on each node either the left or right side of the formula is added:

  1. a > b | c, i
  2. a > b, i : 1
  1. a > b | c, i
  2. c, i : 1

Each branch can now be processed separately. The rules for the propositional operators are explained in Chapter two.

Epistemic Rules

The Box formula rule poses a problem for processing in the serial manner used by the expander. Because it uses two formulae as it's precondition, the Box formula and the WorldRelation formula, it cannot be triggered on the Box operator alone, as a new world relation might be introduced after the Box operator has been processed (or vice versa). To overcome this shortcoming, we must apply the rule to both the Box formula and the WorldRelation formula. To correctly apply the rule we must backtrack on the branch to find matching formula so that they can be applied together (if they have the same agent).

  1. Rn j, i (looked up via backtracking)
  2. Kn a, i
  3. a, j : 1,2
  1. Kn a, i (looked up via backtracking)
  2. Rn j, i
  3. a, j : 1,2

The Diamond formula is the only rule that introduces a new world to be satisfied. It adds a WorldRelation onto the branch and also adds the possible formula here. Here is an example:

  1. Mn a, i
  2. Rn j, i : 1
  3. a, j : 1

S5

For S5, a few more rules are added to this rule system. These rules are applied in the same manner. The reflexivity rule is applied as following. The notation RA i, j is used so denote that an accessibility relation R i, j from world i to world j exists for all agents.

  1. inst, i
  2. RA i, i : 1

Transitivity poses the same problem as the Box formula does. It also has to backtrack to find relations between worlds, so when it it applied to a WorldRelation instance it looks up other worldrelation instances (for the same agent):

  1. Rn j, i (looked up via backtracking)
  2. Rn k, j
  3. Rn k, i : 1,2

Symmetry is just like a normal rule in that it just reverses the relation between the worlds

  1. Rn j, i
  2. Rn i, j : 1

The E and C operator

In the same way we have the rules for K and S5 defined, we can do the same for the E (everybody knows) and C (common knowledge) can be added to our rules. E p (as defined in Chapter 2) practically implies that K1 p & ... & Km p. The rule for this is simplified so that it has the same effect as the Box operator but without checking if the agents are the same.

For ~E p we cannot do the same because it implies that ~(K1 p & ... & Km p), which is equivalent to M1 ~p | ... | Mm ~p). The end effect is that there is a branch created for every agent in the system.

  1. RA j, i (looked up via backtracking, any agent)
  2. E a, i
  3. a, j : 1,2
  1. ~E a, i
  2. M ~a, i : 1 (for each agent a new branch)

Common knowledge is the last operator that has a rule defined. These are expanded like explained in Chapter 2. Examples:

  1. C a, i
  2. E (a & C a), i : 1
  1. ~C a, i
  2. ~E (a & C a), i : 1

Step 3: Transforming the tableau into a collapsed model

When an open tree is in the tableau, it can be used as a model that can be drawn from it. However, before we can draw a model from it, we must first condense the tree into a format that can be used to draw a tree. A lot of nodes can be ignored when generating a model.

First the worlds are determined that are in the tree. By listing all the unique worlds that are in the tree, we can generate the nodes that are going to be in the graph. Next the relations between worlds are added. Some relations might be defined for multiple agents and so these relations can be joined into one relation. When all the worlds and relations have been parsed from the tree, we can conclude with determining the logical truths that are in the worlds.

Step 4: Rendering the generated model

After the model has been rendered, we hand over our condensed model to the JUNG library which draws our model. We have chosen to use the JUNG library as it allows us to easily draw the vertices and edges onto a Java form.

The JUNG library takes care of drawing the vertices (nodes/worlds) and edges (relations) and making a nice layout for them.

Optimisations

The implementation mentioned in the previous chapters leaves things to be improved to enhance the performance of the model generation. During this project, the following optimisations have been implemented:

  1. Stop processing a tree as soon as false can be concluded. As we don't have to process the complete tree and apply all rules on the nodes on it any further. We save execution time and memory with all possible new nodes and branches that could be created.
  2. Insert new nodes right after the current node being processed and before all other nodes awaiting to be processed. This makes sure that we expand the current formula before we work with another one. Possibly leading to an earlier contradiction.
  3. Instead of completely copying the tree when creating a new branch, a shallow copy is created. The formula types are all immutable to make sure no modification can be done once it is added to a tree.

Further improvements could be the following:

  1. Sort the newly added nodes in an improved order. By placing epistemic formulae before propositional formulae and non-branching formulae before branching formulae, the performance of the tableau generation could improve.

Encountered problems

The common knowledge operator might pose problems as it has the potential to infinitely add new worlds to the model if there is some diamond operator expanded from the inner formula. To overcome this problem, the diamond operators first checks if it is already satisfied by looking up the tree for relations to other worlds and checking if the inner formula holds there. This saves creating new worlds when it is not needed. This approach works when the system is S5EC (the rule is satisfied either through reflexivity or symmetry) but not when the system is KEC.


Previous Chapter: Chapter 2 - Theory

Next Chapter: Chapter 4 - Demonstration



Table of Contents  -   Top Of Page

Valid XHTML 1.1! Valid CSS!