A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications
by
Antonín Kučera,
Philippe Schnoebelen,
A full version of the paper presented at CONCUR`04. June 2004, 32 pages.
FIMU-RS-2004-05.
Available as Postscript,
PDF.
Abstract:
We introduce a generic family of behavioral relations for which the
problem of comparing an arbitrary transition system to some
finite-state specification can be reduced to a model checking problem
against simple modal formulae. As an application, we derive
decidability of several regular equivalence problems for well-known
families of infinite-state systems.