Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata
Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata
复制标题
DOI：
10.1007/3-540-48224-5_57
复制
发表时间：
2001-07
期刊：
影响因子：
--
通讯作者：
K. Etessami;T. Wilke;Rebecca A. Schuller
中科院分区：
文献类型：
--
作者：
K. Etessami;T. Wilke;Rebecca A. Schuller
我们给出了有效的算法，击败或匹配的最佳已知的界限，用于计算各种模拟的状态空间上的Büchi自动机的关系。我们的算法是通过一个统一的和简单的奇偶博弈框架。这个框架结合了以前研究的概念，如fairanddirectsimulation，但我们的主要动机是状态空间减少，并为此目的，我们引入了一个新的自然概念的模拟，称为delayedsimulation。我们表明，不像公平的模拟，延迟模拟保留自动机语言后，receiventing，它允许更好的状态比直接simulation.We使用的奇偶博弈的方法，最近的算法Jurdzinski的基础上，有效地计算所有上述模拟关系。特别地，我们得到了一个O（mn ~ 3）-时间和O（mn）-空间的算法来计算延迟和公平的模拟关系。公平互模拟的最佳先验算法需要时间O（n6）（[HKR 97]）.我们的框架还允许有效地计算互模拟：我们在O（mn 3）时间和O（mn）空间中计算公平互模拟关系，而公平互模拟的最佳先验算法需要时间O（n10）（[HR 00]）.
We give efficient algorithms, beating or matching optimal known bounds, for computing a variety of simulation relations on the state space of a Büchi automaton. Our algorithms are derived via a unified and simple parity-game framework. This framework incorporates previously studied notions likefairanddirectsimulation, but our main motivation is state space reduction, and for this purpose we introduce a new natural notion of simulation, calleddelayedsimulation. We show that, unlike fair simulation, delayed simulation preserves the automaton language upon quotienting, and that it allows substantially better state reduction than direct simulation.We use the parity-game approach, based on a recent algorithm by Jurdzinski, to efficiently compute all the above simulation relations. In particular, we obtain anO(mn3)-time andO(mn)-space algorithm for computing both the delayed and fair simulation relations. The best prior algorithm for fair simulation requires timeO(n6) ([HKR97]).Our framework also allows one to compute bisimulations efficiently: we compute the fair bisimulation relation inO(mn3) time andO(mn) space, whereas the best prior algorithm for fair bisimulation requires timeO(n10) ([HR00]).