Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Saturating automata for game semantics

Alex Dixon, Andrzej S. Murawski

TL;DR

Saturating automata provide an automata-theoretic model over infinite alphabets that enforces a saturation-like closure on accepted languages, aligning with the concurrent, higher-order game-semantic view of programs. The authors show how to translate the finitary Idealized Concurrent Algol ($ abla extsf{FICA}$) into SATA, ensuring that SATA captures complete plays with pointers via a forest-structured data domain and WAIT-respecting transitions. For terms in $eta$-normal $ ext{η}$-long form, the resulting automata have linear size and can be constructed in quadratic time, avoiding the exponential blow-ups of prior translations. This work thus offers a principled, scalable automata-theoretic bridge to higher-order concurrency and game semantics, with potential implications for verification and program-analysis tooling that exploit saturation properties.

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.

Saturating automata for game semantics

TL;DR

Saturating automata provide an automata-theoretic model over infinite alphabets that enforces a saturation-like closure on accepted languages, aligning with the concurrent, higher-order game-semantic view of programs. The authors show how to translate the finitary Idealized Concurrent Algol () into SATA, ensuring that SATA captures complete plays with pointers via a forest-structured data domain and WAIT-respecting transitions. For terms in -normal -long form, the resulting automata have linear size and can be constructed in quadratic time, avoiding the exponential blow-ups of prior translations. This work thus offers a principled, scalable automata-theoretic bridge to higher-order concurrency and game semantics, with potential implications for verification and program-analysis tooling that exploit saturation properties.

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.
Paper Structure (18 sections, 6 theorems, 26 equations, 5 figures)

This paper contains 18 sections, 6 theorems, 26 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Finitary Idealised Concurrent Algol ($\mathsf{FICA}$)
  3. Game semantics
  4. Saturating automata ($\mathsf{SATA}$)
  5. DEL
  6. EPS
  7. Saturation
  8. From $\mathsf{FICA}$ to $\mathsf{SATA}$
  9. $\mathbf{M\equiv{\bf skip}}$:
  10. $\mathbf{M\equiv i}$:
  11. $\mathbf{M\equiv {\bf div}_\theta}$:
  12. $\mathbf{M\equiv \mathbf{op}(M_1)}$:
  13. $\mathbf{M \equiv M_1 || M_2}$:
  14. $\mathbf{M\equiv M_1;M_2:{\bf com}}$:
  15. $\mathbf{M\equiv f(M_1)}$:
  16. ...and 3 more sections

Key Result

theorem 1

We have $\Gamma\vdash M_1\cong M_2$ if and only if $\textsf{comp}({\llbracket}{\Gamma\vdash M_1}{\rrbracket})=\textsf{comp}({\llbracket}{\Gamma\vdash M_2}{\rrbracket})$.

Figures (5)

  • Figure 1: $\mathsf{FICA}$ typing rules
  • Figure 2: Reduction rules for $\mathsf{FICA}$
  • Figure 3: Arena constructions ($+$ and $[\cdots]$ stand for the disjoint union of sets and functions respectively; $\langle \cdots \rangle$ denotes pairing).
  • Figure 4: Arenas and justified sequences
  • Figure 5: A transition sequence corresponding to $s_2$ (Figure \ref{['fig:gs2c']}).

Theorems & Definitions (30)

  • definition 1
  • definition 2
  • remark 1
  • definition 3
  • theorem 1: GM08
  • definition 4
  • remark 2
  • theorem 2: GM08
  • definition 5
  • definition 6
  • ...and 20 more