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

Resumo Técnico: Definibilidade de Propriedades Funcionais na Linguagem Modal-Temporal Básica sobre Quadros Ordenados

Enunciado do Problema
Este artigo investiga o poder expressivo da linguagem modal-temporal básica $LT \times W$, formada pela adição dos operadores temporais de Prior $G$ (sempre no futuro) e $H$ (sempre no passado) à linguagem modal básica com $\Box$ (em todas as imagens funcionais). O estudo foca na definibilidade de nove propriedades funcionais específicas — totalidade, não-totalidade, injetividade, sobrejetividade, monotonicidade, monotonicidade estrita, antitonicidade, antitonicidade estrita e constância — através de cinco tipos de ordem distintos: pré-ordens (PRE), pré-ordens estritas (sPRE), ordens parciais (PO), ordens lineares (LO) e ordens lineares estritas (sLO).

Um desafio central abordado é o cenário de "multifluxo" (multiflow), onde múltiplas funções de acessibilidade coexistem e os operadores modais quantificam indiscriminadamente sobre suas imagens combinadas. Trabalhos anteriores (ex: [1, 3]) haviam restringido a análise a ordens lineares estritas e propriedades de Domínio Uniforme (U-Dom). Este artigo visa determinar se essas propriedades são definíveis isoladamente e como sua definibilidade varia através de um espectro mais amplo de estruturas de ordem, examinando especificamente o impacto de duas leituras semânticas: a interpretação padrão (incluindo o instante atual) e a interpretação estrita (excluindo o instante atual).

Metodologia
Os autores empregam uma abordagem analítica de dois estágios para mapear os limites expressivos de $LT \times W$:

1. Cenário de Multifluxo Ordenado Arbitrário: O estudo estabelece primeiro os limites de definibilidade no cenário geral onde os quadros consistem em famílias arbitrárias de funções. Aqui, os operadores modais atuam como quantificadores de segunda ordem sobre a união de todas as imagens funcionais. Os autores utilizam p-morfismos sobrejetivos (que induzem bisimulações funcionais) para provar a undefinibilidade. Se um p-morfismo mapeia um quadro que satisfaz uma propriedade para um que não a satisfaz, a propriedade é undefinível.
2. Refinamento Estrutural (Quadros Mínimos): Para isolar a fonte das limitações expressivas, os autores introduzem "quadros funcionais mínimos" (a família $O_2$), restringindo os quadros a no máximo dois fluxos e uma única função de acessibilidade. Esta redução colapsa a complexidade de segunda ordem do cenário de multifluxo em uma leitura relacional de primeira ordem.
3. Análise Comparativa: O estudo compara os resultados de quadros mínimos contra outros dois frameworks:
   • Linguagens Indexadas: Onde os operadores são explicitamente rotulados para distinguir funções específicas.
   • Quadros de Domínio Uniforme (U-Dom): Onde todas as funções em um quadro compartilam um domínio comum.
4. Variações Semânticas: A análise é conduzida sob ambas as interpretações padrão ($G, H$) e estrita ($G^*, H^*$) para determinar se a exclusão do instante atual altera o panorama de definibilidade.

Contribuições Principais e Resultados

• Limites Expressivos no Cenário de Multifluxo:
  No cenário geral de multifluxo, a linguagem é significativamente fraca. O estudo prova que apenas a totalidade e a sobrejetividade são definíveis, e apenas dentro de ordens lineares (LO e sLO). Todas as outras propriedades (injetividade, monotonicidade, constância, etc.) são undefiníveis em qualquer tipo de ordem, incluindo as lineares. Isso é atribuído à "quantificação indiscriminada" sobre múltiplas funções, que obscurece comportamentos funcionais individuais.

• O Impacto de Quadros Mínimos:
  Ao restringir a semântica para quadros mínimos (função única), o panorama de definibilidade expande-se dramaticamente:

  • Monotonicidade e Antitonicidade: Tornam-se definíveis em todos os tipos de ordem (PRE, sPRE, PO, LO, sLO).
  • Injetividade: Torna-se definível em ordens lineares estritas (sLO) sob a interpretação padrão.
  • Monotonicidade/Antitonicidade Estrita: Tornam-se definíveis em pré-ordens estritas e ordens lineares estritas.
  • Constância: Permanece undefinível em ordens não lineares (PRE, sPRE, PO) mesmo em quadros mínimos, exigendo um argumento de equivalência semântica distinto (pois é preservada por p-morfismos).

• O Papel da Interpretação Estrita:
  No cenário geral de multifluxo, a escolha entre interpretações padrão e estrita produz resultados idênticos. No entanto, em quadros mínimos, a interpretação estrita ($G^*, H^*$) proporciona ganhos cruciais:

  • Ela permite a definição de injetividade em ordens lineares (LO) onde a interpretação padrão falha.
  • Ela permite a definição de monotonicidade estrita e antitonicidade estrita em todos os tipos de ordem, incluindo as não estritas (PRE, PO), ao tratar efetivamente elas como seus equivalentes estritos.

• Equivalência de Frameworks:
  O artigo demonstra que os padrões de definibilidade obtidos em quadros mínimos são idênticos aos de linguagens indexadas (onde as funções são sintaticamente distinguidas) e quadros de Domínio Uniforme (U-Dom). Isso indica que as limitações expressivas do framework original derivam não da fraqueza dos próprios operadores, mas da multiplicidade descontrolada de funções com domínios divergentes. Uma vez que a multiplicidade funcional é controlada (via simplificação estrutural, uniformidade de domínio ou indexação sintática), os operadores básicos recuperam sua capacidade total.

• Obstáculos Fundamentais:
  Mesmo após controlar a multiplicidade funcional, um "núcleo duro" de propriedades — totalidade, não-totalidade, injetividade, sobrejetividade e constância — permanece undefinível em todas as ordens não lineares (PRE, sPRE, PO). Os autores concluem que a falta de conectividade (incomparabilidade de pontos) é um obstáculo fundamental que as modalidades temporais não conseguem superar, independentemente da interpretação ou refinamento estrutural.

Significância
O artigo fornece uma classificação sistemática dos limites expressivos da linguagem modal-temporal básica sobre quadros ordenados. Sua principal significância reside em identificar que a incapacidade de definir propriedades funcionais fundamentais no cenário de multifluxo original é um artefato estrutural da multiplicidade funcional descontrolada, não uma falha inerente aos operadores temporais.

Ao mostrar que quadros mínimos, linguagens indexadas e quadros U-Dom produzem padrões de definibilidade idênticos, o trabalho esclarece as condições precisas sob as quais as propriedades funcionais tornam-se definíveis. Estabelece que, embora a simplificação estrutural possa recuperar a definibilidade de monotonicidade e antitonicidade em todas as ordens, a falta de conectividade linear permanece uma barreira persistente para propriedades que exigem comparações globais de domínio (como totalidade e injetividade) em estruturas não lineares. O estudo também destaca o status especial da constância, que resiste aos padrões de undefinibilidade via p-morfismos em quadros mínimos, exigindo um argumento de equivalência semântica único.