We study the problem of simultaneously performing reachability analysis and simulation reduction of transition systems, called online minimization by Lee and Yannakakis [1992] who settled the question for bisimulation. We call this problem online simulation reduction to reflect some significant dissimilarities w.r.t. Lee and Yannakakis' online bisimulation minimization. Indeed, by means of a reduction to an undecidable problem and of its relationship with graph st-connectivity, we show that by moving from bisimilarity to similarity this online reduction problem becomes fundamentally different. Then, we put forward a symbolic (i.e., processing state partitions) algorithm that performs online reduction in a complete way for the simulation quasiorder while yielding a sound over-approximation for simulation equivalence, and a second symbolic algorithm which is complete for simulation equivalence but, due to the undecidability result, reveals unavoidable limitations on its termination.
翻译：我们研究了同时对过渡系统进行可及性分析和模拟减少模拟的问题,由Lee和Yannakakis(1992年)在网上进行最小化处理,他们解决了减肥问题。我们称这个问题在网上模拟减少时反映了一些显著的异差,而Lee和Yannakakis的在线减肥最小化则反映了一些显著的异差。 事实上,我们通过将问题减到一个不可减轻的问题及其与图形连接性的关系,我们表明,通过从两个相似性转向相似性,这一网上减少问题变得根本不同。 然后,我们提出了一个象征性的(即处理状态分区)算法,在模拟准顺序上完全进行在线减肥,同时产生模拟等同的超近似性,以及第二个完全用于模拟等同的符号算法,但由于不衰减的结果,揭示了在终止时不可避免的限制。
相关内容
微信扫码咨询专知VIP会员