Verification of confliction and unreachability in rule-based expert
  systems with model checking
  It is important to find optimal solutions for structural errors in rule-based
expert systems .Solutions to discovering such errors by using model checking
techniques have already been proposed, but these solutions have problems such
as state space explosion. In this paper, to overcome these problems, we model
the rule-based systems as finite state transition systems and express
confliction and unreachability as Computation Tree Logic (CTL) logic formula
and then use the technique of model checking to detect confliction and
unreachability in rule-based systems with the model checker UPPAAL.
