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 from 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 an 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 algorithm which is complete for simulation equivalence but, due to the undecidability result, reveals unavoidable limitations on its termination. Finally, we report on a prototype implementation.
翻译：我们研究了同时对过渡系统进行可实现性分析和模拟减少转换系统的问题,Lee和Yannakakis(1992年)在网上进行了最小化分析并同时进行模拟处理,他们解决了减肥问题。我们称这个问题的在线模拟减少反映了一些显著的异差(w.r.t. Lee和Yannakakis的在线减肥最小化 ) 。 事实上,我们通过减少一个不可减轻的问题及其与图示连接性的关系,我们表明,通过从两个相似性转向相似性,这一网上减少问题就变得根本不同。 然后,我们提出了一个算法,在模拟准顺序上完全进行网上减少,同时产生模拟等同的超近似性,以及第二个算法完全用于模拟等同,但由于不衰减的结果,揭示了其终止的不可避免的限制。最后,我们报告一个原型的完成情况。
相关内容
微信扫码咨询专知VIP会员