Foundation for a Series of Efficient Simulation Algorithms

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, ->) be a given transition system and R-init be an initial preorder over Q. Until now, algorithms to compute R-sim, the coarsest simulation included in R-init, 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(|P-sim|.| -> |), and a bit space complexity in O(|P-sim|(2). log(|P-sim|)+|Q|. log(|Q|)), with P-sim the partition induced by R-sim.