Implementation of Explanatory Algorithm for Logical Models

Sammanfattning

In this project, we introduce how to implement the explanatory algorithm for logical models that can help us to better understand the properties of a given system. The explanatory algorithm is designed in a way to produce some explanations for the user’s questions about the given behaviours of the given system. By using the explanatory algorithm on the system, we will be able to answer the following questions: why must the system satisfy this specification? Or why does this specification not hold in the system? Then, the algorithm should give some explanations for such questions about the system in the form of mathematical formulas. Our implementation showed that the algorithm provides useful and accurate explanations on small systems. However, for very large systems the results are still correct, but they do not point to the given questions directly. Consequently, we have to follow a certain method to get more relevant explanations.