Resumo Técnico: dtControl2+ε: Otimização de Negociação para Explicabilidade em MDPs via Árvores de Decisão

Declaração do Problema

A síntese de controladores para Processos de Decisão de Markov (MDPs) frequentemente resulta em controladores ótimos representados por tabelas estado-ação grandes e não estruturadas. Embora essas tabelas sejam matematicamente precisas, elas são impraticáveis para implementação em dispositivos com recursos limitados e carecem de explicabilidade, dificultando a validação e a certificação. Ferramentas existentes, como o dtControl2, tentam representar esses controladores como Árvores de Decisão (DTs) para melhorar a interpretabilidade. No entanto, mesmo essas DTs podem se tornar complexas demais para a compreensão humana para sistemas grandes ou com muitos casos de borda.

Um desafio crítico é que a redução do tamanho da DT não é trivial; remover uma única decisão crucial pode tornar um controlador incorreto. Além disso, muitos métodos de síntese escaláveis fornecem apenas controladores $\epsilon$-ótimos (desempenho dentro de $\epsilon$ do valor ótimo), mas as ferramentas de construção de DT existentes tipicamente visam a representação exata ($\epsilon=0$), falhando em aproveitar a imprecisão permitida para simplificar a explicação.

Metodologia

O artigo apresenta o dtControl2+ε, uma ferramenta que estende o estado da arte dtControl2 introduzindo uma funcionalidade "$\epsilon$". O fluxo de trabalho central integra-se estreitamente com o verificador de modelos probabilísticos Storm para construir DTs menores e explicáveis, garantindo que o controlador resultante permaneça $\epsilon$-ótimo.

A metodologia procede em três etapas principais:

1. Resolução de Modelo e Construção de Conjunto de Dados

Em vez de começar com um controlador ótimo determinístico, a ferramenta gera um conjunto de dados inicial que é permissivo (mapeando estados para conjuntos de ações permitidas) ou combinado (restringindo ações permissivas a estados alcançáveis).

• Estratégias Permissivas: A ferramenta identifica ações que são ótimas ou que geram o mesmo valor, permitindo que a DT "unifique" estados.
• Heurísticas de Redução: Antes de aprender a DT, a ferramenta identifica e remove estados onde a escolha específica de uma ação não impacta o resultado ou onde o erro introduzido é limitado por $\epsilon$. Principais técnicas de redução incluem:
  • AllOpt: Remoção de estados onde todas as ações disponíveis são ótimas.
  • Agency (Agência): Remoção de estados onde a diferença entre o melhor e o pior resultado possível é menor que $\epsilon$.
  • Dominância: Remoção de estados que são quase certamente alcançados de outros estados, independentemente da escolha feita.
  • Unreach (Inalcançável): Remoção de estados inalcançáveis a partir do estado inicial sob qualquer controlador consistente.

2. Aprendizado de Árvore de Decisão

A ferramenta emprega uma versão modificada do algoritmo de construção de DT baseado em heurísticas padrão (Algoritmo 1) com diversas melhorias:

• Extração de Predicados: Extrai automaticamente predicados relevantes da descrição de alto nível do modelo (ex: guardas de transição da linguagem PRISM), superando a abordagem de template semiautomática de ferramentas anteriores.
• Medidas de Impureza: Introduz ponderação específica do modelo para cálculos de impureza. Em vez de ponderação uniforme, utiliza:
  • Imp_Simulation: Pondera estados pela frequência de visita (com um piso de segurança para garantir a $\epsilon$-otimalidade).
  • Imp_Agency: Pondera estados pela sua agência (erro potencial).
  • Imp_CoE (Custo do Erro): Pondera estados pelo impacto de escolher a pior ação naquele estado específico.
• Heurísticas Agressivas com Verificação: A ferramenta emprega Interrupção Precoce (terminando divisões quando a impureza está abaixo de um limite) e Poda Gananciosa (colapsando subárvores). Diferente de abordagens "agressivas" anteriores que arriscavam a consistência, o dtControl2+ε usa o Storm para verificar a $\epsilon$-otimalidade da DT resultante. Se a restrição de precisão for violada, a ferramenta relaxa as heurísticas e tenta novamente.

3. Loop de Verificação

Uma característica única é o acoplamento estreito com o Storm para verificação pós-construção. A ferramenta verifica a precisão da DT gerada. Se o desvio do valor ótimo exceder $\epsilon$, ela retrocede e reduz a agressividade das heurísticas (por exemplo, aumentando o limite de interrupção ou desabilitando a poda), garantindo que a saída final seja garantidamente $\epsilon$-ótima.

Contribuições Principais

1. A Ferramenta dtControl2+ε: Uma ferramenta autossuficiente que estende o dtControl2 para construir DTs menores ao explorar a imprecisão permitida $\epsilon$.
2. Heurísticas Seguras vs. Agressivas: Um framework que separa claramente reduções "seguras" (que preservam a $\epsilon$-otimalidade por definição) de heurísticas "agressivas" (que são validadas via verificação de modelos).
3. Extração Automática de Predicados: Um método para derivar predicados de decisão diretamente das guardas de transição do modelo, removendo a necessidade de expertise manual na seleção de predicados.
4. Suporte para Diversos Objetivos: A abordagem cobre objetivos padrão (alcancabilidade, segurança, alcance-evitação, baseados em recompensa) e, unicamente, suporta propriedades de Lógica Temporal Linear (LTL) ao lidar com controladores baseados em memória.

Resultados

Os autores avaliaram o dtControl2+ε contra o dtControl2, dtPaynt, dtNESt e uma reimplementação da abordagem CAV15 em 38 benchmarks (incluindo modelos PRISM com até 500.000 estados).

• Redução de Tamanho: Mesmo para representação exata ($\epsilon=0$), o dtControl2+ε produz DTs ordens de magnitude menores que o dtControl2 devido ao conjunto de dados inicial melhorado e heurísticas seguras.
• Impacto de $\epsilon$: Ao permitir $\epsilon = 10^{-2}$, a ferramenta produziu DTs de nó único para quase metade dos benchmarks, revelando que uma única ação (com fallback aleatório uniforme) é frequentemente suficiente para a $\epsilon$-otimalidade.
• Comparação:
  • vs. dtControl2: O dtControl2+ε produz consistentemente árvores menores.
  • vs. dtPaynt: O dtPaynt esgotou o tempo (timeout) na maioria dos benchmarks e produziu árvores maiores onde teve sucesso.
  • vs. dtNESt: O dtNESt é um forte competidor para $\epsilon=0$, mas o dtControl2+ε produz árvores no máximo metade do tamanho em 23 de 38 benchmarks e ordens de magnitude menores em 10. Notavelmente, o dtNESt frequentemente falha ou produz árvores maiores quando $\epsilon > 0$, enquanto o dtControl2+ε se destaca ao explorar a imprecisão.
• Escalabilidade: A ferramenta resolveu todos os benchmarks, exceto um, dentro de um limite de 20 minutos, demonstrando viabilidade em modelos grandes e complexos.

Significância

O artigo afirma que o dtControl2+ε representa um avanço significativo no estado da arte para a síntese de controladores explicáveis. Ao trocar uma quantidade controlável de otimalidade por compacidade, a ferramenta permite a geração de controladores compreensíveis por humanos que anteriormente eram complexos demais para interpretar. A capacidade de derivar insights estruturais automaticamente (ex: identificar que uma única regra é suficiente para a $\epsilon$-otimalidade) e de suportar propriedades LTL distingue-a das ferramentas existentes. Os autores enfatizam que sua abordagem fornece garantias de $\epsilon$-otimalidade, ao contrário de métodos de poda baseados em heurísticas anteriores que poderiam comprometer a correção.