Résumé Technique : Une Sémantique de Collecte de Stone–Čech pour le Comportement des Processus Résiduels

1. Énoncé du Problème

Une computation infinie n'est pas entièrement caractérisée par la séquence d'actions qu'elle effectue ; elle laisse également derrière elle une séquence de processus résiduels (les processus restant à exécuter après chaque transition). Si les computations finies ou celles se stabilisant dans des cycles simples sont bien comprises, les exécutions infinies peuvent présenter des comportements à long terme complexes :

• Divergence stable : Stabilisation vers un processus unique ou un cycle fini.
• Récurrence mixte : Retour infini à certains états tout en visitant une séquence non bornée de nouveaux états.
• Évasion (Escape) : Quitter toute partie finie de l'espace d'observation (par exemple, une croissance non bornée du nombre de composants parallèles) sans qu'aucun processus résiduel unique ne réapparaisse.

Le défi consiste à fournir une forme sémantique commune pour ces diverses queues résiduelles. Les ensembles limites standards échouent pour les espaces non compacts (où une séquence peut n'avoir aucun limite), et les comptes de récurrence simples ne parviennent pas à capturer le comportement d'« évasion ». De plus, la sémantique doit être robuste sous l'observation : puisque l'objet sémantique complet est trop grand pour être inspecté directement, il doit se comporter correctement sous des observations continues (telles que des compteurs de ressources ou des prédicats modaux).

2. Méthodologie

L'article construit une sémantique de collecte filtrée de Stone–Čech. La méthodologie centrale consiste à traiter une exécution infinie comme un flux d'observations et à projeter son comportement asymptotique dans la compactification de Stone–Čech de l'espace d'observation.

2.1 La Construction

• Temps filtré : Une exécution est définie comme une application $a: T \to X$, où $T$ est un ensemble d'indices temporels équipé d'un filtre propre $\mathcal{F}$ (spécifiant les ensembles de temps « grands »), et $X$ est un espace d'observation de Tychonoff.
• Signification de Stone–Čech : La signification de l'exécution est le compact suivant :
  $$M^F_X(a) = \beta a[\text{Ext}(\mathcal{F})] = \bigcap_{F \in \mathcal{F}} \text{cl}_{\beta X} a[F] \subseteq \beta X$$
  Ici, $\text{Ext}(\mathcal{F})$ est l'ensemble des ultrafiltres sur $T$ étendant $\mathcal{F}$, et $\beta a$ est l'extension continue de $a$ vers les compactifications.
• Interprétation :
  • Pour le temps séquentiel ($T=\mathbb{N}$) avec le filtre cofini, cela produit l'ensemble de grappes de queue (tail-cluster set) dans $\beta X$.
  • Si $X$ est discret et fini, $M^F_X(a)$ est l'ensemble des états visités infiniment souvent.
  • Si $X$ est discret et infini (par exemple, $\mathbb{N}$), la signification peut inclure des points dans le reste $X^* = \beta X \setminus X$, représentant une « évasion » vers l'infini.

2.2 Lecture Observationnelle

La sémantique est conçue pour être lue via des observations continues $f: X \to Y$. Par functorialité, la signification d'une exécution observée est l'image de la signification originale :
$$M^F_Y(f \circ a) = \beta f[M^F_X(a)]$$

• Observations Clopen : Pour un ensemble ouvert et fermé (clopen) $C \subseteq X$, l'inclusion $M^F_X(a) \subseteq \text{cl}_{\beta X} C$ correspond à la vérité éventuelle (l'exécution est éventuellement dans $C$), tandis qu'une intersection non vide correspond à la récurrence (l'exécution visite $C$ infiniment souvent).
• Observations de Ressources : Les cartes de ressources à valeurs entières (par exemple, compter les composants parallèles) peuvent détecter une évasion non bornée en projetant la signification compacte dans le reste des entiers naturels ($\mathbb{N}^*$).

2.3 Gestion de l'Indéterminisme et de la Loyauté (Fairness)

• Indéterminisme : La sémantique distingue entre les significations sensibles à l'exécution (un ensemble de ensembles compacts, un par exécution) et les significations aplaties (l'union de tous les points asymptotiques).
• Loyauté (Fairness) : La loyauté et les hypothèses de progrès sont gérées en renforçant le filtre temporel. Une signification loyale est calculée en restreignant les ultrafiltres admissibles à ceux contenant des ensembles de progrès spécifiques.
• Propriétés Relationnelles : Pour préserver les corrélations entre observations simultanées (par exemple, deux processus tournant en parallèle), la construction compactifie l'espace produit $\beta(X_1 \times \dots \times X_k)$ plutôt que de prendre le produit des significations individuelles.

3. Contributions Clés et Résultats

3.1 Théorie Générale

1. Invariance de Queue : La signification est invariante par rapport aux changements de l'exécution sur tout ensemble de temps qui n'est pas dans le filtre (par exemple, changer un nombre fini de termes dans un flux).
2. Functorialité : Les observations continues commutent avec la construction, permettant de dériver des quotients finis, de la logique modale et des cartes de ressources à partir d'un objet compact unique.
3. Logique Temporelle : La construction fournit une lecture topologique directe pour les modalités temporelles : $\Box_\infty A$ (vérité éventuelle) et $\Diamond_\infty A$ (récurrence) correspondent respectivement à l'inclusion d'ensembles et à l'intersection dans la compactification.

3.2 Application au CCS (Calculus of Communicating Systems)

L'article applique ce cadre au CCS, où les exécutions infinies sont vues comme des flux de classes de congruence structurelle de processus.

• Classification des Comportements : La sémantique distingue :
  • Divergence stable : Ensembles singulets (ex: $A \xrightarrow{a} A$).
  • Divergence récurrente finie : Ensembles finis (ex: alterner entre $P$ et $Q$).
  • Croissance résiduelle non bornée : Ensembles contenus entièrement dans le reste $\beta \text{CCS} \setminus \text{CCS}$ (ex: $G \xrightarrow{a} G|G \xrightarrow{a} G|G|G \dots$).
  • Comportement mixte : Combinaisons de points principaux (récurrents) et non principaux (évasifs).
• Lois de la Queue Résiduelle : L'article prouve que pour les enveloppes de choix de préfixes finis (processus de la forme $\alpha_1.P_1 + \dots + \alpha_k.P_k$), la signification asymptotique résiduelle est l'union des significations des feuilles. Les préfixes finis et les déploiements gardés n'affectent pas la signification de queue.
• Limite des Lois : L'article démontre que ces lois ne sont pas des congruences pour des contextes CCS arbitraires. Spécifiquement, la composition parallèle et la synchronisation peuvent rendre un préfixe fini pertinent avant qu'il ne soit consommé (par exemple, un préfixe $a.0$ peut se synchroniser avec l'environnement pour permettre une boucle, alors que $0$ ne le peut pas). Ainsi, la sémantique est une sémantique de « queue résiduelle », et non une équivalence contextuelle complète.

3.3 Interface Computationnelle

Puisque $\beta X$ est indénombrable et non dénombrable de manière effective, l'article fournit une interface computationnelle via des quotients d'observation finis :

• Une algèbre de Boole finie de prédicats de processus induit un espace quotient fini.
• L'image de la signification compacte dans cet espace est exactement l'ensemble des états abstraits récurrents.
• Pour les graphes de transition finis, cela se réduit à l'analyse des composantes fortement connexes (SCC). Sous une convention de « loyauté d'arête » (edge-fair), les significations loyales correspondent aux SCC terminales atteignables.
• Observables de Ressources : L'évasion non bornée est détectée par calcul en observant qu'une carte de ressource (par exemple, la taille du processus) tend vers l'infini, ce qui correspond au fait que la signification compacte atterrit dans le reste de Stone–Čech de $\mathbb{N}$.

4. Signification et Revendications

L'article revendique de fournir une sémantique de collecte unifiée et compacte pour le comportement des processus résiduels qui :

1. Généralise la Récurrence : Elle subsume la récurrence ordinaire (espaces finis) et les ensembles limites (espaces compacts) tout en s'étendant aux espaces non compacts où l'« évasion » se produit.
2. Unifie les Observations : Elle traite les quotients finis, la logique modale et les mesures de ressources comme des images continues d'un seul objet sémantique, assurant la cohérence à travers différents niveaux d'abstraction.
3. Clarifie l'Équivalence de Queue : Elle établit des lois précises pour savoir quand les préfixes finis peuvent être effacés (dans la queue) et identifie explicitement la limite où la composition parallèle brise cette équivalence.
4. Permet le Calcul : Elle comble le fossé entre les objets compacts abstraits et non calculables et les techniques de vérification concrètes et finies (analyse SCC) ainsi que la surveillance des ressources.

La construction est présentée comme un support sémantique : l'objet compact lui-même n'est pas inspecté directement, mais ses projections (via les observations) fournissent l'interface effective pour l'analyse, la vérification de la loyauté et la vérification des comportements infinis.