Using Model Checking for Verification of Redundancy and Inconsistency in Maritime Laws
Date
2010-06-08T13:08:39Z
Authors
Sagheer, Muzammil
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
A computer-aided solution for the task performed by a Maritime Lawyer is presented in this thesis. It facilitates the process of searching a set of rules from across different Maritime Laws that are applicable in a certain given situation and provides analytical capabilities that include verification of the selected rules against inconsistency as well as reasoning with them. The analyses are meant to decide the applicability of actions from the selected rule set after a careful consideration of possible inconsistencies that may appear in the applicable rules. The analytical techniques require that Maritime Laws be represented as Production Systems. The production rules are first normalized and transformed into an equivalent Petri Net representation. The structural and behavioral analysis of the Petri Net is then performed to look for properties of the net corresponding to useless, incomplete, cyclic, redundant and inconsistent cases. The structural analysis is done by an already existing approach to identify the cases of useless, incomplete and circular rules. The behavioral analysis is done by using a formal methodology of model x checking that explores the state space of the Petri Net to verify the properties corresponding to redundant and inconsistent rules. A reasoning mechanism is also proposed, which uses the Petri Net representation, to answer queries about the applicability of actions from the selected set of rules. The combined use of the verification results and the reasoning mechanism will help a Maritime Lawyer in identifying a course of action for a given situation of interest that is supported by the applicable Maritime Laws.
Description
Keywords
Rule-based systems, Maritime laws, redundancy, Maritime laws, inconsistency, V&v of rule bases, Model checking