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

Problema
A Lógica de Equilíbrio Temporal Métrico (MEL) estende a Lógica de Equilíbrio Temporal (TEL) ao incorporar restrições temporais quantitativas, permitindo a especificação de prazos e durações em sistemas dinâmicos, como sistemas embarcados e ciber-físicos. Embora a MEL permita expressões precisas como "um evento deve ocorrer dentro de 5 milissegundos", as implementações existentes enfrentam desafios. Reduções anteriores de MEL para Programação de Conjuntos de Respostas (ASP) proposicional (por exemplo, por Becker et al.) frequentemente resultam em programas lógicos contendo átomos de futuro puro em cabeçalhos de regras, criando dependências de futuro. Essas dependências dificultam a eficiência de resolvedores incrementais e de múltiplas etapas (multi-shot), que operam melhor quando as derivações de estados atuais dependem apenas de informações de estados computados anteriormente, em vez de estados futuros não computados. Além disso, as traduções existentes não lidam totalmente com operadores temporais métricos binários, como o até métrico ou o liberação métrico.

Metodologia
Os autores propõem uma tradução do tipo Tseitin que mapeia fórmulas temporais métricas arbitrárias para um fragmento específico de programas de lógica temporal métrica. A metodologia central envolve:

1. Restrição a Traços Estritos: A abordagem assume traços estritos onde os pontos temporais aumentam estritamente ($\tau(i) < \tau(i+1)$). Isso permite que operadores métricos binários com intervalos $[0..n]$ sejam desdobrados recursivamente usando equivalências que colapsam os operadores em seus argumentos à direita ou constantes de verdade quando o intervalo é $[0..0]$.
2. Definição de Fechamento: Inspirados pelo fechamento Fisher-Ladner em lógicas dinâmicas, os autores definem um conjunto de fechamento $cl(\phi)$ para uma fórmula $\phi$. Este conjunto inclui não apenas subfórmulas, mas também as expansões recursivas de operadores métricos binários (por exemplo, $\phi U_{\le n} \psi$ gera $\bigcirc^i(\phi U_{\le n-i} \psi)$).
3. Semântica de Três Valores: Para provar a correção da tradução, o artigo utiliza uma caracterização de três valores da lógica de Metric Here-and-There (MHT). Esta semântica, equivalente a MHT, simplifica a verificação das equivalências lógicas necessárias para a redução.
4. Regras de Tradução: A tradução introduz átomos auxiliares (rótulos) para cada fórmula no fechamento. Ela gera regras onde operadores de futuro afetam apenas implicações, enquanto os corpos e cabeçalhos dessas implicações contêm apenas referências de passado e presente. A tradução distingue entre regras dinâmicas (envolvendo operadores de próximo/anterior) e regras iniciais/finais.
5. Ordem Bem-Fundada: Para lidar com a natureza não estrutural do fechamento (onde fórmulas desdobradas não são subfórmulas propriamente ditas), os autores definem uma medida de complexidade $u(\phi)$ baseada no desdobramento de operadores, estabelecendo uma ordem parcial estrita bem-fundada para suportar provas indutivas.

Principais Contribuições

• Redução do tipo Tseitin: Uma redução formal de fórmulas temporais métricas arbitrárias para programas de lógica temporal métrica restritos a operadores de passado nos corpos das regras.
• Tratamento de Operadores Binários: A tradução lida explicitamente com operadores métricos binários ($U_{\le n}, R_{\le n}, S_{\le n}, T_{\le n}$) com intervalos da forma $[0..n]$, uma limitação em codificações ASP proposicionais anteriores.
• Eliminação de Dependências de Futuro: Ao garantir que os corpos das regras dependam apenas de informações de passado e presente, os programas lógicos resultantes são compatíveis com técnicas de resolução incremental usadas em resolvedores como o telingo.
• Correção Formal: O artigo prova que a tradução preserva o conjunto de Modelos de Equilíbrio Métrico (equivalência forte módulo átomos auxiliares) e estabelece um limite polinomial sobre o tamanho do programa gerado em relação ao tamanho da fórmula de entrada e ao intervalo máximo $n$.

Resultos
O artigo demonstra que, para qualquer fórmula temporal métrica $\phi$, existe um programa de lógica temporal métrica $\Gamma$ tal que os modelos de equilíbrio métrico de $\phi$ correspondem exatamente à projeção dos modelos de equilíbrio métrico de $\Gamma$ sobre o alfabeto original. O tamanho do programa gerado é limitado por uma função polinomial do tamanho da fórmula e do valor do intervalo máximo $n$. A tradução mostra-se correta sob a suposição de traços estritos e intervalos da forma $[0..n]$.

Significância
O artigo afirma fornecer uma "forma normal" para interpretar teorias temporais métricas sob semântica de conjuntos de respostas. Ao conectar fórmulas temporais métricas com programas de lógica restritos a operadores de passado, o trabalho permite o aproveitamento de resolvedores ASP existentes e eficientes (especificamente aqueles que suportam resolução de múltiplas etapas e incremental) para o raciocínio sobre restrições temporais métricas. Isso facilita a implementação prática de MEL em domínios que exigem tempo preciso, como software de tempo real e sistemas embarcados, sem as ineficiências associadas às dependências de futuro. Os autores observam que, embora o trabalho atual seja limitado a intervalos $[0..n]$, ele estabelece as bases para estender essas reduções para intervalos arbitrários e integrá-las ao resolvedor telingo.