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

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.

• Type: Conference
• Year: 2004
• Where: CONCUR
• Authors: Antonín Kucera, Ph. Schnoebelen
• Keywords: CONCUR 2004, Distributed And Parallel Computing, Model Checking Problem, Regular Equivalence Problems, Simple Modal Formulae