Reducing Arbitrary Metric Temporal Formulas into Logic Programs under Answer Set Semantics

Problème
La logique de l'équilibre temporel métrique (MEL - Metric Temporal Equilibrium Logic) étend la logique de l'équilibre temporel (TEL) en incorporant des contraintes temporelles quantitatives, permettant la spécification de délais et de durées dans les systèmes dynamiques tels que les systèmes embarqués et cyber-physiques. Bien que la MEL permette des expressions précises comme « un événement doit se produire dans un délai de 5 millisecondes », les implémentations existantes font face à des défis. Les réductions précédentes de la MEL vers la programmation par ensembles de réponses (ASP) propositionnelle (par exemple, par Becker et al.) aboutissent souvent à des programmes logiques contenant des atomes du futur pur dans les têtes de règles, créant ainsi des dépendances futures. Ces dépendances entravent l'efficacité des solveurs incrémentiels et multi-shots, qui sont plus performants lorsque les dérivations de l'état actuel reposent uniquement sur des informations provenant d'états précédemment calculés plutôt que sur des états futurs non calculés. De plus, les traductions existantes ne gèrent pas pleinement les opérateurs temporels métriques binaires tels que l'« jusqu'à » métrique ou le « relâchement » métrique.

Méthodologie
Les auteurs proposent une traduction de type Tseitin qui associe des formules temporelles métriques arbitraires à un fragment spécifique de programmes de logique temporelle métrique. La méthodologie centrale implique :

1. Restriction aux traces strictes : L'approche suppose des traces strictes où les points temporels augmentent strictement ($\tau(i) < \tau(i+1)$). Cela permet aux opérateurs métriques binaires avec des intervalles $[0..n]$ d'être déroulés de manière récursive à l'aide d'équivalences qui réduisent les opérateurs en leurs arguments de droite ou en constantes de vérité lorsque l'intervalle est $[0..0]$.
2. Définition de la clôture : Inspirée par la clôture de Fisher-Ladner dans les logiques dynamiques, les auteurs définissent un ensemble de clôture $cl(\phi)$ pour une formule $\phi$. Cet ensemble inclut non seulement les sous-formules, mais aussi les expansions récursives des opérateurs métriques binaires (par exemple, $\phi U_{\le n} \psi$ génère $\bigcirc^i(\phi U_{\le n-i} \psi)$).
3. Sémantique à trois valeurs : Pour prouver la correction de la traduction, l'article utilise une caractérisation à trois valeurs de la logique Metric Here-and-There (MHT). Cette sémantique, équivalente à MHT, simplifie la vérification des équivalences logiques requises pour la réduction.
4. Règles de traduction : La traduction introduit des atomes auxiliaires (étiquettes) pour chaque formule de la clôture. Elle génère des règles où les opérateurs du futur n'affectent que les implications, tandis que les corps et les têtes de ces implications ne contiennent que des références passées et présentes. La traduction distingue les règles dynamiques (impliquant des opérateurs de type « suivant/précédent ») des règles initiales et finales.
5. Ordre bien fondé : Pour gérer la nature non structurelle de la clôture (où les formules déroulées ne sont pas des sous-formules propres), les auteurs définissent une mesure de complexité $u(\phi)$ basée sur le déroulement des opérateurs, établissant un ordre partiel strict bien fondé pour soutenir les preuves inductives.

Contributions clés

• Réduction de type Tseitin : Une réduction formelle de formules temporelles métriques arbitraires vers des programmes de logique temporelle métrique restreints aux opérateurs passés dans les corps de règles.
• Gestion des opérateurs binaires : La traduction gère explicitement les opérateurs métriques binaires ($U_{\le n}, R_{\le n}, S_{\le n}, T_{\le n}$) avec des intervalles de la forme $[0..n]$, une limitation présente dans les encodages ASP propositionnels précédents.
• Élimination des dépendances futures : En garantissant que les corps de règles ne reposent que sur des informations passées et présentes, les programmes logiques résultants sont compatibles avec les techniques de résolution incrémentielle utilisées dans des solveurs comme telingo.
• Correction formelle : L'article prouve que la traduction préserve l'ensemble des modèles d'équilibre métrique (équivalence forte modulo les atomes auxiliaires) et établit une borne polynomiale sur la taille du programme généré par rapport à la taille de la formule d'entrée et à la valeur d'intervalle maximale $n$.

Résultats
L'article démontre que pour toute formule temporelle métrique $\phi$, il existe un programme de logique temporelle métrique $\Gamma$ tel que les modèles d'équilibre métrique de $\phi$ correspondent exactement à la projection des modèles d'équilibre métrique de $\Gamma$ sur l'alphabet d'origine. La taille du programme généré est bornée par une fonction polynomiale de la taille de la formule et de la valeur maximale de l'intervalle $n$. La traduction est montrée comme étant correcte sous l'hypothèse de traces strictes et d'intervalles de la forme $[0..n]$.

Signification
L'article affirme fournir une « forme normale » pour interpréter les théories temporelles métriques sous la sémantique des ensembles de réponses. En jetant un pont entre les formules temporelles métriques et les programmes logiques restreints aux opérateurs passés, ce travail permet de tirer parti des solveurs ASP existants et efficaces (spécifiquement ceux supportant la résolution multi-shot et incrémentielle) pour le raisonnement sur les contraintes temporelles métriques. Cela facilite la mise en œuvre pratique de la MEL dans des domaines exigeant une précision temporelle, tels que les logiciels temps réel et les systèmes embarqués, sans les inefficacités associées aux dépendances futures. Les auteurs notent que bien que le présent travail soit limité aux intervalles $[0..n]$, il pose les bases pour étendre ces réductions à des intervalles arbitraires et les intégrer dans le solveur telingo.