Resumo Técnico: Quocientes Mínimos e Canônicos para Equivalências de Simulação

Declaração do Problema

Os Sistemas de Transição Rotulados (LTSs) servem como o modelo semântico fundamental para várias linguagens de especificação de alto nível. Uma técnica comum para gerenciar o problema da explosão do espaço de estados é o quotientamento (quotienting), que funde estados equivalentes para produzir um sistema menor e semanticamente equivalente. Embora as funções de quotientamento e suas propriedades (canonicidade e minimalidade) sejam bem estabelecidas para bisimilaridade forte, bisimilaridade de ramificação e equivalência de traço, seu comportamento para a equivalência de simulação fraca e similaridade acoplada permanece pouco explorado.

Resultados existentes para outras equivalências mostram graus variados de sucesso:

• Para bisimilaridade, os quocientes são canônicos (únicos até isomorfismo) e mínimos.
• Para equivalência de traço, quocientes mínimos podem não ser únicos, e computá-los é PSPACE-completo.
• Para simulação fraca e similaridade acoplada, desconhece-se se existem quocientes canônicos ou mínimos, nem a complexidade de computá-los foi estabelecida.

Este artigo investiga a existência de quocientes canônicos e mínimos para a equivalência de simulação fraca ($\equiv_S$) e similaridade acoplada ($\equiv_{CS}$), e analisa a complexidade computacional de encontrá-los.

Metodologia

Os autores desenvolvem procedimentos abstratos para transformar um LTS arbitrário em um representante de sua classe de equivalência. A metodologia baseia-se em uma sequência de transformações baseadas nas propriedades de pré-ordens de simulação e em $\tau$-leis específicas (axiomas que regem ações inobserváveis).

1. Quociente Universal e Remoção de Redundância

O processo começa com o quociente-$\forall$, que funde todos os estados equivalentes. No entanto, isso por si só é insuficiente, pois pode introduzir transições "inertes" (transições entre estados equivalentes) e transições "duplicadas".

• Transições Cobertas: Os autores generalizam a noção de transições duplicadas para transições cobertas. Uma transição $p \xrightarrow{\alpha} q$ é coberta se existir outra transição $p' \xrightarrow{\alpha} q'$ tal que $p$ possa alcançar $p'$ via passos-$\tau$ e $q$ seja simulado por $q'$ ($q \sqsubseteq_x q'$).
• A remoção de transições cobertas preserva a equivalência e reduz o espaço de estados, mas o LTS resultante não é necessariamente canônico nem mínimo.

2. $\tau$-dessaturação (Para Canonicidade)

Para alcançar a canonicidade, o artigo introduz a $\tau$-dessaturação, baseada nos axiomas $\tau.x = x$ e $\tau.(\tau.x + y) = \tau.x + y$.

• Operação: Se um estado $p$ possui uma transição-$\tau$ para $q$ ($p \xrightarrow{\tau} q$), a transição é removida e $p$ é "saturado" com todas as transições de saída de $q$. Para similaridade acoplada, isso exige que $q$ possua uma transição-$\tau$ de saída.
• Efeito: Esta transformação elimina transições-$\tau$ consecutivas e reduz as transições de entrada para os estados. A aplicação repetida termina, resultando em um LTS dessaturado.
• Resultado: Ao combinar o quociente-$\forall$, a $\tau$-dessaturação, a remoção de transições cobertas e a remoção de estados inalcançáveis, os autores definem um LTS reduzido. Eles provam que quaisquer dois LTSs reduzidos que sejam equivalentes são isomorfos, estabelecendo assim a existência de um quociente canônico.

3. $\tau$-saturação (Para Minimalidade)

Para alcançar a minimalidade, os autores introduzem a operação inversa: $\tau$-saturação.

• Operação: Se $q \sqsubseteq_x p$, uma transição-$\tau$ $p \xrightarrow{\tau} q$ pode ser adicionada. Isso pode tornar as transições existentes "cobertas", permitindo que sejam removidas.
• Desafio de Otimização: A escolha de quais transições-$\tau$ adicionar é não-determinística. Diferentes escolhas levam a diferentes reduções. O problema de selecionar o conjunto ótimo de passos de $\tau$-saturação para maximizar a redução é mostrado como equivalente ao Problema de Cobertura de Conjuntos (Set Cover Problem).
• Algoritmo: O procedimento de quociente mínimo computa primeiro o quociente canônico e, em seguida, identifica transições "cobertas" para cada estado. Ele resolve uma instância de Cobertura de Conjuntos para cada estado para determinar o conjunto mínimo de transições-$\tau$ a serem adicionadas, o que subsequentemente permite a remoção do número máximo de outras transições.

Contribuições e Resultados Principais

1. Existência de Quocientes Canônicos

O artigo prova que, tanto para a equivalência de simulação fraca quanto para a similaridade acoplada, um quociente canônico existe.

• Teorema 4.4: Dois LTSs reduzidos (dessaturados, sem transições cobertas, sem estados inalcançáveis, sem transições inertes, sem estados equivalentes) são equivalentes se, e somente se, forem isomorfos.
• Algoritmo 1: Um procedimento de tempo polinomial é fornecido para computar este quociente canônico.

2. Complexidade de Quocientes Mínimos

O artigo estabelece que computar um quociente mínimo (um com o menor número lexicográfico de estados e transições) é NP-completo.

• Teorema 5.5: A minimização com respeito a $\equiv_x$ é NP-difícil. Isso é provado via uma redução do Problema de Cobertura de Conjuntos.
• Implicação: Diferente da minimização de bisimilaridade (que é polinomial), encontrar o menor LTS equivalente para equivalências de simulação é computacionalmente intratável no caso geral.
• Algoritmo 2: Um procedimento é descrito que computa um quociente mínimo aproveitando um oráculo para o Problema de Cobertura de Conjuntos. Embora o algoritmo em si não seja de tempo polinomial (devido ao subproblema NP-difícil), ele permite o uso de solvers de Cobertura de Conjuntos de última geração. As instâncias geradas para esses solvers são tipicamente pequenas (limitadas pelo grau de saída dos estados).

3. Distinção da Bisimilaridade

Os resultados destacam uma divergência fundamental da bisimilaridade:

• Para a bisimilaridade, o quociente mínimo é único e computável em tempo polinomial.
• Para as equivalências de simulação, os quocientes mínimos podem não ser únicos (múltiplos LTSs mínimos não isomorfos podem existir para a mesma classe de equivalência) e encontrá-los é NP-completo.

Significância e Alegações

O artigo afirma estender a compreensão teórica do quotientamento além das equivalências de bisimulação e traço bem estudadas.

• Generalização: A abordagem generaliza o conceito de "transições duplicadas" e utiliza $\tau$-leis específicas de pré-ordens de simulação para derivar formas canônicas.
• Praticidade: Embora encontrar o quociente absolutamente mínimo seja NP-completo, o método proposto permite que praticantes utilizem solvers de Cobertura de Conjuntos eficientes para alcançar reduções significativas no espaço de estados, visto que as instâncias específicas que surgem da minimização de LTS são frequentemente pequenas.
• Modéstia: Os autores observam explicitamente que seus resultados dependem das $\tau$-leis específicas da simulação fraca e da similaridade acoplada. Eles não alegam que esses resultados se generalizam para todo o espectro de tempo linear-tempo (LTL-branching time), sugerindo que diferentes equivalências podem exigir distintas $\tau$-leis e estratégias de transformação.

Em conclusão, o artigo fornece os primeiros procedimentos abstratos para obter tanto quocientes canônicos quanto mínimos para simulação fraca e similaridade acoplada, caracterizando o primeiro como computável em tempo polinomial e o segundo como NP-completo.