We study the problem of computing the reachable blocks of simulation equivalence and design algorithms for this problem by interleaving reachability and simulation computation while possibly avoiding the computation of all the reachable states or the whole simulation preorder. Following an investigation of the decidability and complexity aspects of this problem, we put forward several sound algorithms with varying completeness guarantees as well as a symbolic procedure manipulating state partitions and relations between their blocks, suited for processing infinite state systems. We show that the symbolic algorithm comes with better termination guarantees and, through empirical evidence, runs faster in general.

翻译：我们研究了模拟等价的可达块计算问题，并设计了通过交错进行可达性计算与模拟计算来求解该问题的算法，该方法可能避免计算所有可达状态或整个模拟预序。在探讨该问题的可判定性与复杂性后，我们提出了若干具有不同完备性保证的可靠算法，以及一种操作状态划分及其块间关系的符号化程序，该程序适用于处理无限状态系统。我们证明该符号化算法具有更强的终止保证，并通过实证证据表明其运行速度总体更快。