We study the problem of computing the reachable principals of simulation preorder and the reachable blocks of simulation equivalence. Following a theoretical investigation of the decidability and complexity aspects of this problem, which in particular highlights a stark contrast with the already settled case of bisimulation, we design algorithms to solve this problem by leveraging the idea of interleaving reachability and simulation computation while possibly avoiding the computation of all the reachable states or the whole simulation preorder. In particular, we put forward a symbolic algorithm processing state partitions and, in turn, relations between their blocks, which is suited for processing infinite state systems.

翻译：本文研究了仿真预序的可达主元以及仿真等价的可达块的计算问题。在对该问题的可判定性和复杂性进行理论探讨后——这一研究特别揭示了与已解决的双仿真问题之间的显著差异——我们设计了通过交织可达性与仿真计算来求解该问题的算法，同时尽可能避免计算所有可达状态或整个仿真预序。具体而言，我们提出了一种基于状态划分及其块间关系处理的符号化算法，该算法适用于处理无限状态系统。