A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications

Abstract. We introduce a generic family of behavioral relations for which the problem of comparing an arbitrary transition system to some finite-state speci-fication can be reduced to a model checking problem against simple modal for-mulae. As an application, we derive decidability of several regular equivalence problems for well-known families of infinite-state systems.