Alex Dixon ; Andrzej S. Murawski - Saturating automata for game semantics

entics:12277 - Electronic Notes in Theoretical Informatics and Computer Science, November 23, 2023, Volume 3 - Proceedings of MFPS XXXIX - https://doi.org/10.46298/entics.12277
Saturating automata for game semanticsArticle

Authors: Alex Dixon ; Andrzej S. Murawski

    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.


    Volume: Volume 3 - Proceedings of MFPS XXXIX
    Published on: November 23, 2023
    Accepted on: October 16, 2023
    Submitted on: September 15, 2023
    Keywords: Computer Science - Programming Languages,Computer Science - Formal Languages and Automata Theory

    Consultation statistics

    This page has been seen 62 times.
    This article's PDF has been downloaded 59 times.