Parameterized refinement is a refinement technique for preserving specific Linear Time Temporal Logic properties during formal program development. In this paper, we describe a proof method for verifying that one program is a parameterized refinement of another program.

Our method combines transduction, due to Jonsson, Pnueli, and Rump, for showing that one system simulates another system, with techniques used in implementations of model checkers. The method is argued to be attractive in a development environment, where tools such as model checkers are applied. It enables rigorous verification that one system is a parameterized refinement of another system.