Buffered Simulation Games for B\"uchi Automata

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 language inclusion itself. Continuous simulation is even EXPTIME-hard. We also provide matching upper bounds for solving these games with infinite state spaces.