From hidden to visible: A unified framework for transforming behavioral theories into rewrite theories

Algebraic formalization and verification are effective and practical ways of modeling and verifying software systems by both model checking and theorem proving techniques. In algebraic approaches, a system can be modeled either in a hidden way as a behavioral theory or in a visible way as a rewrite theory. Several approaches have been proposed to transform behavioral theories into rewrite theories for integrating model checking and theorem proving in verification. In this paper, we propose a framework for transforming behavioral theories into rewrite theories, which unifies four existing related transformation approaches. In this framework, each existing transformation approach can be viewed as a process of transforming behavioral theories first into a special class of behavioral theories and finally into rewrite theories. From this perspective, these transformation approaches differ from each other only in the transformation from ordinary behavioral theories into the classified ones, and their transformations from the classified ones into rewrite theories are essentially the same. We prove that the transformation framework preserves linear-time properties. The preservation of linear-time properties guarantees that a counterexample found by model checking a linear-time property with a generated rewrite theory is also a counterexample in the original behavioral theory, as required by integrated verification.