Definability of Functional Properties in the Basic Modal-Temporal Language over Ordered Frames

Résumé technique : Définissabilité des propriétés fonctionnelles dans le langage modal-temporel de base sur les cadres ordonnés

Énoncé du problème
Cet article étudie la puissance expressive du langage modal-temporel de base $LT \times W$, formé par l'ajout des opérateurs temporels de Prior $G$ (toujours dans le futur) et $H$ (toujours dans le passé) au langage modal de base avec $\Box$ (dans toutes les images fonctionnelles). L'étude se concentre sur la définissabilité de neuf propriétés fonctionnelles spécifiques — totalité, non-totalité, injectivité, surjectivité, monotonie, monotonie stricte, antitonicité, antitonicité stricte et constance — à travers cinq types d'ordres distincts : préordres (PRE), préordres stricts (sPRE), ordres partiels (PO), ordres linéaires (LO) et ordres linéaires stricts (sLO).

Un défi central abordé est le cadre de « multiflux » (multiflow), où plusieurs fonctions d'accessibilité coexistent et où les opérateurs modaux quantifient de manière indistincte sur leurs images combinées. Des travaux antérieurs (ex. [1, 3]) avaient limité l'analyse aux ordres linéaires stricts et aux contraintes globales comme la propriété de Domaine Uniforme (U-Dom). Cet article vise à déterminer si ces propriétés sont définissables de manière isolée et comment leur définissabilité varie à travers un spectre plus large de structures d'ordre, en examinant spécifiquement l'impact de deux lectures sémantiques : l'interprétation standard (incluant l'instant actuel) et l'interprétation stricte (excluant l'instant actuel).

Méthodologie
Les auteurs emploient une approche analytique en deux étapes pour cartographier les limites expressives de $LT \times W$ :

1. Cadre de multiflux ordonné arbitraire : L'étude établit d'abord les limites de définissabilité dans le cadre général où les cadres consistent en des familles de fonctions arbitraires. Ici, les opérateurs modaux agissent comme des quantificateurs du second ordre sur l'union de toutes les images de fonctions. Les auteurs utilisent des p-morphismes surjectifs (qui induisent des bisimulations fonctionnelles) pour prouver l'indéfinissabilité. Si un p-morphisme associe un cadre satisfaisant une propriété à un autre qui ne la satisfait pas, la propriété est indéfinissable.
2. Raffinement structurel (Cadres minimaux) : Pour isoler la source des limitations expressives, les auteurs introduisent des « cadres fonctionnels minimaux » (la famille $O_2$), restreignant les cadres à au plus deux flux et une seule fonction d'accessibilité. Cette réduction réduit la complexité du second ordre du cadre de multiflux en une lecture relationnelle du premier ordre.
3. Analyse comparative : L'étude compare les cadres minimaux à deux autres cadres :
   • Langages indexés : Où les opérateurs sont explicitement étiquetés pour distinguer les fonctions spécifiques.
   • Cadres à Domaine Uniforme (U-Dom) : Où toutes les fonctions d'un cadre partagent un domaine commun.
4. Variations sémantiques : L'analyse est menée sous les deux interprétations, standard ($G, H$) et stricte ($G^*, H^*$), pour déterminer si l'exclusion de l'instant actuel modifie le paysage de la définissabilité.

Contributions clés et résultats

• Limites expressives dans le cadre de multiflux :
  Dans le cadre général de multiflux, le langage est significativement faible. L'étude prouve que seules la totalité et la surjectivité sont définissables, et uniquement au sein des ordres linéaires (LO et sLO). Toutes les autres propriétés (injectivité, monotonie, constance, etc.) sont indéfinissables dans n'importe quel type d'ordre, y compris les ordres linéaires. Cela est attribué à la « quantification indistincte » sur plusieurs fonctions, qui occulte les comportements fonctionnels individuels.

• L'impact des cadres minimaux :
  En restreignant la sémantique aux cadres minimaux (fonction unique), le paysage de la définissabilité s'élargit considérablement :

  • Monotonie et Antitonicité : Elles deviennent définissables dans tous les types d'ordres (PRE, sPRE, PO, LO, sLO).
  • Injectivité : Devient définissable dans les ordres linéaires stricts (sLO) sous l'interprétation standard.
  • Monotonie/Antitonicité strictes : Deviennent définissables dans les préordres stricts et les ordres linéaires stricts.
  • Constance : Reste indéfinissable dans les ordres non linéaires (PRE, sPRE, PO) même dans les cadres minimaux, nécessitant un argument d'équivalence sémantique distinct (car elle est préservée par les p-morphismes).

• Le rôle de l'interprétation stricte :
  Dans le cadre général de multiflux, le choix entre les interprétations standard et stricte produit des résultats identiques. Cependant, dans les cadres minimaux, l'interprétation stricte ($G^*, H^*$) apporte des gains cruciaux :

  • Elle permet la définition de l'injectivité dans les ordres linéaires (LO) là où l'interprétation standard échoue.
  • Elle permet la définition de la monotonie stricte et de l'antitonicité stricte dans tous les types d'ordres, y compris les non-stricts (PRE, PO), en les traitant effectivement comme leurs homologues stricts.

• Équivalence des cadres :
  L'article démontre que les modèles de définissabilité obtenus dans les cadres minimaux sont identiques à ceux des langages indexés (où les fonctions sont syntaxiquement distinguées) et des cadres U-Dom (où les fonctions partagent un domaine uniforme). Cela indique que les limitations expressives du cadre original ne proviennent pas de la faiblesse des opérateurs eux-mêmes, mais de la multiplicité incontrôlée de fonctions aux domaines divergents. Une fois la multiplicité fonctionnelle contrôlée (via une simplification structurelle, l'uniformité du domaine ou l'indexation syntaxique), les opérateurs de base recouvrent leur pleine capacité.

• Obstacles fondamentaux :
  Même après avoir contrôlé la multiplicité fonctionnelle, un « noyau dur » de propriétés — totalité, non-totalité, injectivité, surjectivité et constance — reste indéfinissable dans tous les ordres non linéaires (PRE, sPRE, PO). Les auteurs concluent que l'absence de connectivité (l'incomparabilité des points) est un obstacle fondamental que les modalités temporelles ne peuvent surmonter, quelle que soit l'interprétation ou le raffinement structurel.

Signification
L'article fournit une classification systématique des limites expressives du langage modal-temporel de base sur les cadres ordonnés. Sa signification principale réside dans l'identification du fait que l'incapacité à définir des propriétés fonctionnelles fondamentales dans le cadre de multiflux original est un artefact structurel de la multiplicité fonctionnelle incontrôlée, et non un défaut inhérent aux opérateurs temporels.

En montrant que les cadres minimaux, les langages indexés et les cadres U-Dom produisent des modèles de définissabilité identiques, ce travail clarifie les conditions précises sous lesquelles les propriétés fonctionnelles deviennent définissables. Il établit que si la simplification structurelle peut restaurer la définissabilité de la monotonie et de l'antitonicité à travers tous les ordres, l'absence de connectivité linéaire demeure une barrière persistante pour les propriétés exigeant des comparaisons globales de domaines (comme la totalité et l'injectivité) dans les structures non linéaires. L'étude souligne également le statut spécial de la constance, qui résiste aux preuves classiques d'indéfinissabilité par p-morphismes dans les cadres minimaux, nécessitant un argument d'équivalence sémantique unique.