Model Refinement Using Bisimulation Quotients

erschienen 2010 in M. Johnson, D. Pavlovic (eds.): Algebraic Methodology and Software Technology (AMAST 2010), LNCS 6486, pp. 76-91, 2010.

Abstract: The paper shows how to refine large-scale or even infinite transition systems so as to ensure certain desired properties. First, a given system is reduced into a smallish, finite bisimulation quotient. Second, the reduced system is refined in order to ensure a given property, using any known finite-state method. Third, the refined reduced system is expanded back into an adequate refinement of the system given initially. The proposed method is based on a Galois connection between systems and their quotients. It is applicable to various models and bisimulations and is illustrated with a few qualitative and quantitative properties.