论文标题
计算可及的模拟
Computing Reachable Simulations
论文作者
论文摘要
我们研究了计算模拟预订的可及主和模拟等效块的问题。经过对该问题的可决定性和复杂性方面进行理论研究，这特别突出了与已经结束的仿真案例形成鲜明对比的情况，我们设计了算法来解决此问题，通过利用相互交织的可及性和仿真计算的想法，而可能避免了所有可触及状态或整个仿真的计算。特别是，我们提出了一种符号算法处理状态分区，进而提出了它们的块之间的关系，该分区适用于处理无限状态系统。
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.
