Saturating automata for game semantics

TL;DR

This paper introduces saturating automata, a new automata model over infinite alphabets, to effectively model higher-order concurrent programs with saturation properties, enabling polynomial-time translation from a fragment of FICA.

Contribution

The paper proposes saturating automata that guarantee saturation properties, and demonstrates their efficient translation from FICA, improving over previous models with exponential complexity.

Findings

Automata accept languages satisfying saturation closure.

Translation from FICA is polynomial time for normal forms.

Automata have linearly many states and transitions for normal form terms.

Abstract

Saturation is a fundamental game-semantic property satisfied by strategies that interpret higher-order concurrent programs. It states that the strategy must be closed under certain rearrangements of moves, and corresponds to the intuition that program moves (P-moves) may depend only on moves made by the environment (O-moves). We propose an automata model over an infinite alphabet, called saturating automata, for which all accepted languages are guaranteed to satisfy a closure property mimicking saturation. We show how to translate the finitary fragment of Idealized Concurrent Algol (FICA) into saturating automata, confirming their suitability for modelling higher-order concurrency. Moreover, we find that, for terms in normal form, the resultant automaton has linearly many transitions and states with respect to term size, and can be constructed in polynomial time. This is in contrast to earlier attempts at finding automata-theoretic models of FICA, which did not guarantee saturation and involved an exponential blow-up during translation, even for normal forms.