Title: Foundation for a series of efficient simulation algorithms,
Abstract: Compute the coarsest simulation preorder included in an initial preorder is
used to reduce the resources needed to analyze a given transition system. This
technique is applied on many models like Kripke structures, labeled graphs,
labeled transition systems or even word and tree automata. Let (Q,
$\rightarrow$) be a given transition system and Rinit be an initial preorder
over Q. Until now, algorithms to compute Rsim , the coarsest simulation
included in Rinit , are either memory efficient or time efficient but not both.
In this paper we propose the foundation for a series of efficient simulation
algorithms with the introduction of the notion of maximal transitions and the
notion of stability of a preorder with respect to a coarser one. As an
illustration we solve an open problem by providing the first algorithm with the
best published time complexity, O(|Psim |.|$\rightarrow$|), and a bit space
complexity in O(|Psim |^2. log(|Psim |) + |Q|. log(|Q|)), with Psim the
partition induced by Rsim.