跟踪语言包含的多缓冲区模拟
Multi-Buffer Simulations for Trace Language Inclusion
摘要：
我们认为模拟游戏之间的破坏者和复制两个Büchi自动机，其中的选择由破坏者可以缓冲复制在几个缓冲区之前，她执行他们对她的结构。我们表明，模拟游戏是有用的，以近似包含跟踪封闭的语言接受有限状态自动机，这是已知的不可判定的。我们研究的可判定性和复杂性，并表明，有界缓冲区的游戏可以决定在多项式时间，而一个无界和一个有界缓冲区的游戏是高度不可判定的。我们还显示了一些充分条件的自动机复制器赢得比赛（无界缓冲区）。
英文摘要：
We consider simulation games played between Spoiler and Duplicator on two Büchi automata in which the choices made by Spoiler can be buffered by Duplicator in several buffers before she executes them on her structure. We show that the simulation games are useful to approximate the inclusion of trace closures of languages accepted by finite-state automata, which is known to be undecidable. We study the decidability and complexity and show that the game with bounded buffers can be decided in polynomial time, whereas the game with one unbounded and one bounded buffer is highly undecidable. We also show some sufficient conditions on the automata for Duplicator to win the game (with unbounded buffers).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
