Quantitative fair simulation games
Quantitative fair simulation games
复制标题
DOI：
10.1016/j.ic.2016.10.006
复制
发表时间：
2017-06-01
影响因子：
1
通讯作者：
Velner, Yaron
中科院分区：
文献类型：
--
作者：
Chatterjee, Krishnendu;Henzinger, Thomas A.;Velner, Yaron
模拟是自动机语言包含的一个有吸引力的替代方案，因为它是语言包含的下近似，但通常具有低得多的复杂性。模拟还在两个正交方向上进行了扩展，即（1）公平模拟，用于在指定的无限运行集上进行模拟;（2）定量模拟，用于加权自动机之间的模拟。虽然公平跟踪包含是PSPACE完全的，但公平模拟可以在多项式时间内计算。对于加权自动机，（定量）语言包含问题一般是不可判定的，而（定量）模拟则归结为定量博弈，允许伪多项式时间算法.本文研究了具有Bfichi接受条件的加权自动机的（定量）模拟问题，即，我们将公平模拟从非加权自动机推广到加权自动机。我们表明，施加Bfichi接受条件的加权自动机改变了许多基本性质的模拟游戏，但他们仍然承认伪多项式时间算法。(C)2016 Elsevier Inc. All rights reserved.
Simulation is an attractive alternative to language inclusion for automata as it is an under approximation of language inclusion, but usually has much lower complexity. Simulation has also been extended in two orthogonal directions, namely, (1) fair simulation, for simulation over specified set of infinite runs; and (2) quantitative simulation, for simulation between weighted automata. While fair trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial time. For weighted automata, the (quantitative) language inclusion problem is undecidable in general, whereas the (quantitative) simulation reduces to quantitative games, which admit pseudo-polynomial time algorithms.In this work, we study (quantitative) simulation for weighted automata with Bfichi acceptance conditions, i.e., we generalize fair simulation from non-weighted automata to weighted automata. We show that imposing Bfichi acceptance conditions on weighted automata changes many fundamental properties of the simulation games, yet they still admit pseudo-polynomial time algorithms. (C) 2016 Elsevier Inc. All rights reserved.