Model Checking is Refinement -- Relating Buechi Testing and Linear-Time Temporal Logic

摘要

This paper develops a semantic foundation for reasoning about reactive systems specifications featuring combinations of labeled transition systems and formulas in linear time temporal logic (LTL). Using Buechi automata as a semantic basis, the paper introduces two refinement preorders based on DeNicola and Hennessy's notion of may- and must-testing. Alternative characterizations for these relations are provided and used to show that the new preorders are conservative extensions of the traditional DeNicola and Hennessy preorders. The paper then establishes a tight connection between LTL formula satisfaction and the Buechi must-preorder. More precisely, it is shown that a labeled transition system satisfies an LTL formula if and only if it refines an appropriately defined Buechi automaton that can be constructed from the formula. Consequently, the Buechi must-preorder allows for a uniform treatment of traditional notions of process refinement and model checking. The implications of the novel theory are illustrated by means of a simple example system, in which some components are specified as transition systems and others as LTL formulas.