A Linear Temporal Logic of Frequencies on Series of Events

1. Problema e Motivação

O artigo aborda a necessidade crítica de monitorar e controlar sistemas complexos em tempo de execução, especialmente em contextos onde as saídas devem alinhar-se a requisitos específicos de distribuição de frequência. Um exemplo central é a avaliação de classificadores de aprendizado de máquina sob a ótica da justiça algorítmica, onde é necessário verificar se as decisões probabilísticas do modelo correspondem a distribuições ideais ou desejadas.

O problema central identificado é a falta de uma lógica temporal existente que formalize explicitamente a relação entre uma frequência observada (dados empíricos de uma série de eventos) e uma distribuição teórica alvo (frequência ideal) dentro de uma única estrutura de avaliação. Embora existam extensões de lógicas temporais com contagem ou probabilidades (como LTL de contagem, CTL ou PCTL), elas geralmente focam em contagens absolutas ou probabilidades de caminhos, sem integrar a comparação dinâmica entre o observado e o ideal em séries finitas de eventos de forma "olhando para trás" (backward-looking).

2. Metodologia: A Lógica LTLF

Os autores propõem a LTLF (Linear Temporal Logic of Frequencies), uma nova lógica proposicional temporal projetada para expressar propriedades de frequência de séries de eventos de maneira natural e rigorosa.

Estrutura Semântica

A semântica da LTLF é baseada em estruturas de Kripke adaptadas para séries temporais finitas:

• Mundos ($W$): Representam instantes de tempo discretos em uma série finita de eventos ($w_1, \dots, w_n$).
• Relação de Acessibilidade ($R_e$): Uma relação linear, reflexiva, transitiva e fortemente conectada, representando a ordem temporal.
• Atribuições ($a$): Mapeamentos que associam proposições atômicas (resultados de experimentos) a mundos, representando a "observação real".
• Distribuição de Frequência ($F_\Omega$): Um conjunto de atribuições compatíveis com uma medida de probabilidade empírica definida sobre um espaço de amostra $\Omega$.

Operadores Chave

A inovação central reside na introdução de cinco operadores modais sensíveis a medidas, que permitem contar ocorrências e prever futuras ocorrências baseadas em distribuições esperadas:

1. $\Box_q \phi$ (Caixa Branca): Operador dependente da observação e do tempo. Expressa que, até o momento atual, a fórmula $\phi$ foi observada em uma frequência relativa de pelo menos $q$. Reflete a frequência empírica acumulada.
2. $\blacksquare_q \phi$ (Caixa Preta): Operador dependente do tempo, mas independente da observação atual. Expressa que, de acordo com a distribuição alvo $F_\Omega$, é possível que $\phi$ tenha ocorrido com frequência $q$ até o momento atual. Verifica a compatibilidade da observação parcial com a distribuição ideal.
3. $\circ_q \phi$ (Círculo): Dependente de tempo e observação. Expressa que, até o momento atual, $\phi$ ocorreu em pelo menos $q \times n$ vezes (onde $n$ é o total de experimentos planejados). Relaciona o observado com o total global.
4. $\triangleright_q \phi$ (Seta): Operador de "próximo". Calcula a probabilidade condicional de que $\phi$ ocorra no próximo passo, assumindo que a observação atual é compatível com a distribuição alvo $F_\Omega$.
5. $\star_q \phi$ (Estrela): Operador global e independente do tempo/observação. Expressa que, segundo a distribuição $F_\Omega$, existe um momento onde a frequência de $\phi$ é pelo menos $q$. Reflete a propriedade intrínseca da distribuição teórica.

3. Contribuições Principais

• Formalização Unificada: A LTLF é a primeira lógica temporal a integrar explicitamente a verificação de compatibilidade entre frequências observadas e distribuições teóricas alvo em uma única estrutura semântica.
• Abordagem "Backward-Looking": Diferente da maioria das lógicas temporais que projetam para o futuro, a LTLF interpreta operadores olhando para o passado (histórico da série), permitindo a avaliação dinâmica em qualquer ponto da série.
• Novos Operadores Modais: A definição de operadores que combinam contagem, probabilidade e comparação com um ideal, permitindo expressar conceitos como "compatibilidade com uma distribuição" e "probabilidade de realização futura".
• Solução de Problemas de Decisão: O artigo demonstra como a lógica resolve formalmente cinco classes de problemas:
  1. Medir a frequência de um resultado em uma série.
  2. Verificar a compatibilidade entre uma frequência parcial observada e uma frequência global esperada.
  3. Verificar se uma observação é compatível com uma frequência desejada.
  4. Expressar a probabilidade de realizar uma frequência desejada.
  5. Prever a probabilidade de um resultado futuro dado o histórico e a distribuição alvo.

4. Resultados e Propriedades

Os autores estabelecem a semântica formal e provam várias propriedades teóricas:

• Definibilidade e Interdefinibilidade: Demonstram que os operadores podem ser definidos uns em termos dos outros ou através de restrições de desigualdade estrita ($<q$) e igualdade ($=q$).
• Monotonicidade e Independência: Estabelecem propriedades de monotonicidade dos operadores e sua independência de atribuições específicas em certos contextos.
• Teoremas de Compatibilidade:
  • O Teorema 5.5 fornece condições para detectar inconsistência: se a frequência observada ($\Box$) difere da compatibilidade com o alvo ($\blacksquare$), a observação atual não pertence à distribuição alvo.
  • O Teorema 5.8 e 5.9 fornecem fórmulas para calcular a probabilidade de uma observação parcial ser compatível com a distribuição alvo, considerando casos de resultados equiprováveis e não equiprováveis (independentes).
  • O Teorema 5.10 e 5.12 formalizam o cálculo da probabilidade de um evento futuro ($\triangleright$) baseado no histórico observado e na restrição da distribuição global.
• Exemplos Aplicados: O artigo utiliza o exemplo clássico de lançamentos de moedas para ilustrar como a lógica pode detectar viés (bias) em tempo real. Por exemplo, se uma moeda deve ser justa (50% cara, 50% coroa), a lógica pode determinar em qual ponto da série uma sequência de resultados (ex: 3 coros seguidos) torna impossível atingir a frequência ideal, ou qual é a probabilidade de recuperar o equilíbrio nos lançamentos restantes.

5. Significado e Impacto

A LTLF preenche uma lacuna significativa entre o raciocínio lógico formal e a observação empírica em sistemas dinâmicos.

• Aplicação em IA e Justiça Algorítmica: A lógica oferece uma ferramenta formal para monitorar classificadores de aprendizado de máquina, permitindo verificar se as decisões do modelo estão desviando de distribuições justas ou esperadas durante a execução, facilitando a mitigação de viés.
• Sistemas de Controle: É aplicável a qualquer sistema onde o controle de qualidade depende de manter uma distribuição estatística de saídas ao longo do tempo.
• Fundação Teórica: O trabalho abre caminho para o desenvolvimento de sistemas de prova e resultados meta-teóricos para lógicas temporais baseadas em frequência, além de extensões para tempos ramificados (tree structures), que estão em desenvolvimento pelos autores.

Em resumo, o artigo apresenta uma ferramenta lógica robusta e intuitiva para modelar, monitorar e prever o comportamento de sistemas estocásticos finitos, conectando a teoria das probabilidades com a lógica temporal de uma maneira inédita.