Enhancing simulation for checking language containment

Abstract

Many verification approaches based on automata theory are related to the language containment problem, which is PSPACE-complete for nondeterministic automata. To avoid such a complexity, one may use simulation as an approximation to language containment, since simulation implies language containment and computing simulation is a polynomial time problem. As it is an approximation, there exists a gap between simulation and language containment, therefore there has been an effort to develop methods to narrow the gap while keeping the computation in polynomial time. In this paper, we present such an approach by building a Büchi automaton based on partial marked subset construction to be used in the computation of simulation relation, such that the automaton preserves the original language and has a structure that helps identify more pairs of automata that are in language containment relation. This approach is an improvement to the fair-k-simulation method [3]. © Springer-Verlag Berlin Heidelberg 2007.