Resumo Técnico: Raciocínio de Pré-expectativa Multiobjetivo para Programas Probabilísticos

Declaração do Problema

Programas probabilísticos com não determinismo modelam problemas de planejamento e controle onde uma estratégia (ou controlador) deve resolver escolhas não determinísticas para otimizar resultados esperados. Enquanto as abordagens clássicas focam na otimização de uma única quantidade (ex: nível de combustível esperado ou probabilidade de terminação), muitos cenários do mundo real exigem a otimização de múltiplos objetivos, frequentemente conflitantes, simultaneamente (ex: maximizar a probabilidade de sucesso enquanto se minimiza o consumo de recursos).

No cenário multiobjetivo, melhorar um objetivo frequentemente degrada outro. O conjunto de trocas (trade-offs) ideais é capturado pela fronteira de Pareto. Métodos existentes para otimização multiobjetivo em Processos de Decisão de Markov (MDPs) são amplamente restritos a modelos de estados finitos. No entanto, programas probabilísticos frequentemente induzem MDPs de estados infinitos. Além disso, há uma carência de um cálculo dedutivo de nível de programa capaz de raciocinar sobre múltiplas expectativas simultaneamente, sintetizar estratégias e lidar com espaços de estados infinitos sem recorrer à enumeração explícita de estados.

Este artigo aborda três questões centrais:

1. Q1: Qual é o conjunto de tuplas de valores simultaneamente alcançáveis (a pré-expectativa multiobjetivo) para um determinado programa, e pode ele ser computado via um cálculo mecanizável de nível de programa?
2. Q2: Dada uma troca alvo alcançável, como podemos sintetizar um refinamento de programa (estratégia) que a realize?
3. Q3: Como esses construtos de nível de programa se relacionam com e estendem a teoria de MDPs multiobjetivos (possivelmente de estados infinitos)?

Metodologia

Os autores desenvolvem um transformador de pré-expectativa multiobjetivo (denotado por mop) que opera no nível do programa. Esta abordagem estende o cálculo clássico de pré-expectativa fraca (wp) para lidar com vetores de expectativas.

1. O Transformador de Pré-expectativa Multiobjetivo (mop)

A inovação central é o mapeamento de uma tupla de pós-expectativas $(f_1, \dots, f_n)$ para um conjunto de valores simultaneamente alcançáveis.

• Domínio: O transformador opera no powerset de Hoare convexo de $\mathbb{R}_{\ge 0}^n$. Elementos deste domínio são subconjuntos de $\mathbb{R}_{\ge 0}^n$ que são:
  • Não vazios: Sempre contendo o vetor zero.
  • Descendentes (Downward closed): Se um vetor de valores é alcançável, qualquer vetor dominado por ele também é alcançável.
  • Convexos fechados (Convex closed): Misturar estratégias (randomizar sobre determinizações) permite alcançar qualquer combinação convexa de seus resultados.
  • Scott-fechados (Scott closed): Captura pontos "quase alcançáveis" (limites de sequências de pontos alcançáveis), garantindo completude para sistemas de estados infinitos onde os supremos podem não ser atingidos por uma única estratégia.
• Semântica: O transformador é definido indutivamente sobre a estrutura do programa (skip, atribuição, composição sequencial, escolha probabilística, escolha não determinística guardada e laços/loops).
  • Para escolha não determinística guardada, o mop aplica o supremo pontual no powerset, o que corresponde à união Scott-fechada e convexa-fechada dos ramos.
  • Para laços (loops), o mop é definido como o ponto fixo inferior (lfp) de uma função característica, cuja existência é garantida devido à $\omega$-continuidade do transformador.

2. Síntese de Estratégia via Escalarização

Para sintetizar uma estratégia (uma determinização) que alcance um ponto específico na fronteira de Pareto, os autores empregam escalarização:

• Somas Ponderadas: Um vetor de pesos $w$ combina múltiplos objetivos em uma única expectativa escalar $w \cdot f$.
• Redução: O problema de encontrar uma estratégia para uma troca específica é reduzido ao problema de encontrar uma estratégia ótima para uma soma ponderada. Técnicas existentes de síntese de estratégia programática de objetivo único (ex: [Batz et al. 2024a]) podem ser usadas para encontrar uma determinização pura $C_w$ que maximize $w \cdot f$.
• Determinizacões Mistas: Como uma única estratégia determinística pode não alcançar todos os pontos na fronteira de Pareto (especialmente pontos não expostos), os autores introduzem determinizacões mistas. Estas são programas que realizam um lançamento de moeda inicial para selecionar entre diferentes determinizações puras. Mostra-se que o conjunto de pontos alcançáveis é o fecho convexo do envelope dos resultados dessas determinizações puras.

3. Raciocínio de Laços e Terminação

O artigo fornece regras para raciocinar sobre laços usando invariantes:

• Limites Superiores: Derivados via indução de Park usando superinvariantes.
• Limites Inferiores: Derivados usando subinvariantes sob condições específicas de terminação:
  • Terminação Quase-Certa Demônica (dAST - Demonic Almost-Sure Termination): Toda resolução de não determinismo termina com probabilidade 1.
  • Terminação Certa Demônica (dCT - Demonic Certain Termination): Todas as execuções terminam dentro de um número limitado de passos.
  • $\omega$-invariantes: Uma sequência de invariantes que rastreia a profundidade de desdobramento (unrolling), aplicável sem suposições de terminação, mas que requer infinitas obrigações de prova.

4. Correspondência Operacional

Os autores estabelecem uma conexão rigorosa entre o transformador de nível de programa mop e a semântica operacional de programas probabilísticos como MDPs de ação finita e estados enumeráveis.

• Eles definem um operador de Bellman generalizado no powerset de Hoare convexo para MDPs.
• Provam que o transformador mop coincide exatamente com o ponto fixo inferior deste operador de Bellman, caracterizando o conjunto de vetores de recompensa esperada quase alcançáveis. Esta correspondência ocorre sem assumir um espaço de estados finito.

Principais Contribuições

1. Transformador de Pré-expectativa Multiobjetivo: Introdução do mop, um transformador bem definido, monótono e $\omega$-contínuo no powerset de Hoare convexo que estende conservativamente as pré-expectativas fracas para o cenário multiobjetivo.
2. Raciocínio Baseado em Invariantes: Elevação do raciocínio de invariantes para laços ao cenário multiobjetivo, fornecendo regras para limites superiores e inferiores, incluindo condições de exatidão (dAST/dCT).
3. Síntese de Estratégia: Desenvolvimento de regras para sintetizar estratégias testemunhas. O artigo demonstra que, embora as determinizações puras possam não ser suficientes para todos os pontos ótimos de Pareto, as determinizacões mistas (randomizando sobre determinizações puras) podem alcançar qualquer ponto no fecho convexo Scott-fechado do conjunto alcançável.
4. Correspondência Operacional: Prova de uma correspondência exata entre o transformador mop e um operador de Bellman generalizado sobre semânticas operacionais de MDP, válida para MDPs de estados contáveis (infinitos). Isso generaliza resultados seminais de verificação de MDP multiobjetivo que anteriormente eram restritos a estados finitos.
5. Estudos de Caso: Aplicação da maquinaria a três estudos de caso:
   • Robô: Um trade-off entre risco e velocidade, demonstrando o cálculo de fronteiras de Pareto e a síntese de estratégias mistas.
   • Cassino: Um cenário de jogo com recompensas ilimitadas, ilustrando o raciocínio com $\omega$-invariantes e dAST.
   • Fila (Queue): Um sistema de servidor adaptativo, mostrando como o framework pode caracterizar simbolicamente as trocas sob varições de parâmetros ambientais.

Resultados e Significância

O artigo afirma que o mop fornece uma abordagem simbólica de nível de programa para otimização multiobjetivo sobre MDPs infinitos.

• Completude: O transformador captura exatamente o conjunto de pontos quase alcançáveis. A fronteira de Pareto é identificada como o limite deste conjunto.
• Capacidade de Síntese: O framework permite a construção mecânica de estratégias (determinizacões) que alcançam trocas específicas, desde que o ponto alvo seja "exposto" (otimizável por uma soma ponderada) ou possa ser aproximado por tais pontos. Para pontos não expostos, o artigo observa que, embora a síntese exata via uma única soma ponderada possa falhar, o ponto pode ser aproximado arbitrariamente perto de pontos expostos (Teorema de Straszewicz).
• Limitações: Os autores notam modestamente que as condições suficientes para a existência de determinizações ótimas exatas (Scott-fechamento dos conjuntos alcançáveis) nem sempre são fáceis de verificar. Além disso, o framework atual é limitado a uma linguagem imperativa simples (pGCL) e ainda não suporta procedimentos, recursão, manipulação de heap ou distribuições contínuas. Objetivos como recompensas descontadas ou médias de longo prazo também estão fora do escopo atual.

Em resumo, este trabalho une a lacuna entre a verificação dedutiva de programas e a teoria de MDP multiobjetivo, oferecendo um cálculo unificado para raciocinar sobre trocas em programas probabilísticos com não determinismo, mesmo em configurações de estados infinitos.