Model Checking a Rule-based Parser

In the field of natural language processing, one key difficulty for rule-based systems is the debugging and tuning of rules. In this paper we suggest a novel method that use model checking tools to theoretically verify the rule system of a feature-based parser. We discuss the modeling of the system: the establishment of Kripke structures, and most importantly, the method to compress the state space of the model. We use partial Kripke structures as a main tool for space compression. We show that the state space can be reduced considerably while the compressed model still keeps similar behavior as the non-compressed one. Initial examples of specifications are presented and certain restrictions on them are discussed.