Using truth-preserving reductions to improve the clarity of kripke-models

Abstract

We present an approach by means of which temporal logic models may be replaced by smaller ones without affecting the truth values of any formulas of a fairly standard linear-time temporal logic without a nexttime-operator. The main advantage of the approach is the increased readability of a model, as we can concentrate on some features of the model and hide irrelevant details. Two other advantages are the potential for increased model-checking speed, and the inherent compositionality of the method.

Our method is based on the observation that instead of recording the truth values of atomic propositions in the states of a model, it is enough to record the truth values in the initial state of the model and attach to each transition a label telling how the truth values of the atomic propositions change when that transition is taken. This allows us to handle a temporal logic model as a labelled transition system and apply process-algebraic reduction methods to it. Specifically, it is noted that the process-algebraic equivalence class defined by initial stability, stable failures and divergences, is truth-preserving w.r.t the logic applied in this paper.