Buffered Simulation Games for B\"uchi Automata
Milka Hutagalung (University of Kassel), Martin Lange (University of, Kassel), Etienne Lozes (University of Kassel)

TL;DR
This paper introduces buffered simulation games for Büchi automata, revealing their computational complexity and limitations in approximating language inclusion, with continuous and look-ahead variants exhibiting high complexity.
Contribution
It extends multi-letter simulations to buffered simulations, analyzing their computational hardness and providing bounds for solving these complex games.
Findings
Look-ahead simulation is PSPACE-hard.
Continuous simulation is EXPTIME-hard.
Matching upper bounds are provided for infinite state spaces.
Abstract
Simulation relations are an important tool in automata theory because they provide efficiently computable approximations to language inclusion. In recent years, extensions of ordinary simulations have been studied, for instance multi-pebble and multi-letter simulations which yield better approximations and are still polynomial-time computable. In this paper we study the limitations of approximating language inclusion in this way: we introduce a natural extension of multi-letter simulations called buffered simulations. They are based on a simulation game in which the two players share a FIFO buffer of unbounded size. We consider two variants of these buffered games called continuous and look-ahead simulation which differ in how elements can be removed from the FIFO buffer. We show that look-ahead simulation, the simpler one, is already PSPACE-hard, i.e. computationally as hard as…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
