Explosão do Espaço de Estados e Model Checking Simbólico

• Explicar por que o espaço de estados alcançável de um sistema modelado cresce de forma multiplicativa, e não aditiva, a cada variável ou componente acrescentado.
• Calcular o número de estados alcançáveis no pior caso para um sistema descrito por N flags booleanas independentes e explicar por que esse limite é estrutural, e não uma falha de implementação.
• Explicar como uma representação simbólica, como um diagrama de decisão binária, consegue descrever de forma compacta um conjunto exponencialmente grande de estados.
• Descrever a redução por ordem parcial e explicar, de forma concreta, que redundância ela elimina.
• Explicar o que é um contraexemplo espúrio, por que a abstração pode introduzir um e como o refinamento responde a ele.

model-checking-exhaustive-state-space-exploration estabeleceu que a exaustividade (visitar todo estado alcançável) é exatamente o que torna o model checking uma técnica de prova genuína, e não de amostragem. Essa mesma exaustividade é também a fonte do maior obstáculo de engenharia da disciplina, e vale ser direto sobre por que o obstáculo é inevitável em princípio, e não um sintoma de ferramentas pouco espertas: o número de estados alcançáveis em um modelo realista cresce por multiplicação, e não por adição, toda vez que uma nova variável, um novo componente concorrente ou um novo entrelaçamento possível é acrescentado ao modelo. Um model checker a que só se pede para checar sistemas pequenos de brinquedo, escolhidos a dedo, nunca esbarra nisso; um model checker a que se pede para verificar qualquer coisa parecida com um protocolo real ou com um software concorrente real esbarra nisso quase de imediato.

Este conceito existe para tornar esse crescimento concreto e numericamente palpável, em vez de deixá-lo como um alerta vago, e depois para apresentar a família de técnicas (abstração, redução e representação simbólica) que o model checking usa para manter intacta a ideia subjacente de busca exaustiva, mudando, às vezes de forma dramática, como os conjuntos de estados envolvidos são de fato representados e manipulados. Nenhuma dessas técnicas muda o que está sendo provado; elas mudam como a prova é calculada, trocando uma representação que lista os estados um por um por representações que conseguem descrever conjuntos enormes de estados de uma vez.

Fontes da explosão

Várias fontes independentes de crescimento se compõem umas com as outras em um modelo realista, e vale nomeá-las individualmente porque cada uma pede uma mitigação um pouco diferente mais adiante neste conceito. O produto dos estados dos componentes é a fonte mais básica: se um sistema é modelado como várias peças que interagem, cada uma com seus estados locais, o espaço de estados do sistema combinado é (no pior caso) o produto do número de estados de cada peça, e não a soma. Os entrelaçamentos de ações concorrentes multiplicam ainda mais o espaço: com vários processos, cada um capaz de dar um passo, o número de ordens possíveis em que seus passos podem ocorrer cresce de forma combinatória com o número de processos e de passos envolvidos, e um model checker ingênuo trata cada entrelaçamento distinto como um caminho distinto a explorar. Domínios de dados como contadores e arrays acrescentam mais um fator multiplicativo, já que cada valor possível que um contador ou uma célula de array pode ter é, em princípio, mais um eixo ao longo do qual o espaço de estados cresce. Buffers de mensagens e escolhas irrestritas do ambiente compõem ainda mais tudo isso, já que cada conteúdo possível de buffer ou cada entrada possível do ambiente é mais uma dimensão de variação que o modelo precisa levar em conta.

Contando estados concretamente

Para tornar o crescimento numericamente concreto, e não abstrato: um sistema descrito por N variáveis de estado booleanas independentes tem, no pior caso, exatamente 2^N combinações possíveis dos seus valores e, portanto, até 2^N estados alcançáveis. Dez flags booleanas independentes já produzem até 2^10 = 1.024 combinações possíveis, um número pequeno o bastante para enumerar confortavelmente em uma máquina. Vinte flags produzem até 2^20 = 1.048.576 combinações possíveis, mais de um milhão, só por dobrar o número de flags uma vez. É crescimento exponencial no sentido mais literal: cada variável booleana adicional dobra o tamanho do espaço de estados no pior caso, em vez de somar algum incremento fixo, e é exatamente por isso que acrescentar "só mais uma" flag a um modelo pode levá-lo de confortavelmente checável a intratável de forma muito mais repentina do que a intuição linear sugeriria. Acrescentar estrutura concorrente compõe isso ainda mais, em vez de apenas somar: dois processos adicionais, cada um com cinco localizações de controle distintas, multiplicam a contagem de estados por 5 × 5 = 25 por cima do que a contagem de variáveis de dados já contribuía; uma instância direta da fonte de explosão do produto dos estados dos componentes recém-descrita, agora ligada a um número concreto. Nada desse crescimento é um bug na implementação de alguma ferramenta específica; é um fato estrutural sobre quantas combinações distintas um sistema com essa quantidade de variabilidade genuína de fato tem, e todo model checker, por mais bem projetado que seja, precisa lidar com isso de um jeito ou de outro.

Técnicas de redução

Várias técnicas atacam a explosão reconhecendo que nem todos esses estados combinatoriamente numerosos, nem todos esses entrelaçamentos combinatoriamente numerosos, precisam de fato ser visitados separadamente para que uma dada propriedade seja checada corretamente. A abstração junta estados que são indistinguíveis do ponto de vista da propriedade específica sendo checada, substituindo muitos estados concretos por um estado abstrato que representa todos eles de uma vez, sempre que a propriedade não depende de fato dos detalhes que os distinguem. A redução por ordem parcial mira especificamente a fonte de explosão dos entrelaçamentos: quando duas ações executadas por processos diferentes e independentes não afetam o resultado uma da outra nem a propriedade sendo checada (um processo incrementando seu contador privado enquanto outro processo sem relação envia uma mensagem por outro canal, digamos), explorar toda ordem possível em que essas duas ações podem se entrelaçar é redundante, já que a verdade da propriedade não depende de qual ordem foi escolhida; a redução por ordem parcial identifica essas ações independentes e explora só uma ordem representativa entre elas, em vez de toda permutação, sem deixar de lado nenhum comportamento que possa de fato afetar a propriedade. A redução por simetria explora uma redundância relacionada, mas distinta: quando vários processos de um modelo são estruturalmente intercambiáveis (vários processos trabalhadores idênticos rodando o mesmo código, digamos), muitos estados combinados diferem só em qual processo calha de estar em qual estado local, e a redução por simetria explora só um padrão representativo para cada classe de equivalência desses estados intercambiáveis, em vez de cada rotulagem distinta. O raciocínio composicional ataca o problema por um ângulo completamente diferente, verificando um componente isoladamente sob uma premissa explícita sobre como seu ambiente (o resto do sistema) se comporta, em vez de jamais construir o espaço de estados combinado completo de todos os componentes juntos.

Representação simbólica

Uma estratégia genuinamente diferente, em vez de reduzir quais estados são visitados, muda como os conjuntos de estados são representados, para começo de conversa. Em vez de listar os estados alcançáveis um por um (a abordagem que model-checking-exhaustive-state-space-exploration descreveu, e a que esbarra diretamente no argumento de contagem exponencial acima), o model checking simbólico representa um conjunto inteiro de estados usando uma fórmula, ou uma estrutura de dados especializada como um diagrama de decisão binária (BDD), que consegue descrever exponencialmente muitos estados com uma representação cujo tamanho não precisa crescer exponencialmente. Concretamente, em vez de listar separadamente os quatro estados de três bits 001, 011, 101 e 111, a única fórmula bit0 = 1 descreve exatamente esse mesmo conjunto de quatro estados de uma vez, porque são precisamente os estados cujo bit menos significativo é 1; uma fórmula curta valendo por todo estado que a satisfaz, não importa quantos sejam. Um BDD consegue representar conjuntos definidos por fórmulas assim de forma compacta, especialmente quando a estrutura subjacente do conjunto tem uma regularidade que o compartilhamento interno de um BDD consegue explorar, e a própria relação de transição vira uma relação simbólica entre um conjunto de variáveis de "estado atual" e um conjunto correspondente de variáveis de "próximo estado", de modo que calcular quais estados são alcançáveis vira uma computação de imagem simbólica repetida: aplicar a relação de transição a um conjunto representado inteiro de estados de uma vez, algebricamente, em vez de explorar os sucessores de um estado concreto por vez.

Trade-offs

Os métodos simbólicos conseguem, quando a estrutura subjacente colabora, lidar com espaços de estados enormemente maiores do que qualquer enumeração com estados explícitos poderia esperar visitar diretamente; esse é todo o seu atrativo. Mas o custo dessa compactação é que ela depende muito de detalhes invisíveis à propriedade sendo checada: para um BDD especificamente, a ordem em que as variáveis são arranjadas internamente pode fazer uma diferença enorme, às vezes transformando uma representação que seria exponencialmente grande em uma pequena e administrável, ou o contrário, e encontrar uma boa ordem de variáveis é em si um problema genuinamente difícil, sem solução automática universalmente confiável. A abstração, por sua vez, compra sua própria redução do espaço de estados com o risco de outro tipo de custo: como ela junta deliberadamente estados que uma propriedade não parece precisar distinguir, ela pode de vez em quando juntar estados que na verdade deveriam ter sido mantidos separados, produzindo um contraexemplo espúrio: um rastro que existe no modelo abstraído, mas que não corresponde a nenhuma execução concreta real do sistema de verdade.

Contando estados

Dez flags booleanas independentes produzem até 2^10 = 1.024 estados alcançáveis no pior caso, confortavelmente enumeráveis. Dobrar para vinte flags produz até 2^20 = 1.048.576 estados alcançáveis, mais de um milhão, ilustrando de forma concreta como cada flag adicional dobra a contagem no pior caso em vez de só somar a ela. Agora suponha que dois processos adicionais sejam acrescentados a esse modelo de vinte flags, cada um com cinco localizações de controle distintas: a contagem de estados é multiplicada de novo por 5 × 5 = 25, levando o total no pior caso a cerca de 1.048.576 × 25 ≈ 26,2 milhões de estados alcançáveis; um número alcançado a partir de uma descrição de sistema que, lida informalmente, soa inteiramente modesta ("vinte flags e dois processos com cinco localizações"). Esse crescimento é exatamente o fenômeno estrutural e inevitável que o argumento de contagem exponencial acima prevê, e não um artefato de algum model checker mal projetado; é o motivo concreto de abstração, redução e representação simbólica existirem como técnicas, em vez de serem refinamentos opcionais só para sistemas excepcionalmente grandes.

Conjunto simbólico

Continuando a ilustração anterior: em vez de listar separadamente os estados 001, 011, 101 e 111 como quatro entradas distintas no conjunto de visitados de uma busca com estados explícitos, a fórmula bit0 = 1 nomeia exatamente esse mesmo conjunto de quatro estados com uma única expressão curta, porque essas são precisamente as combinações de três bits cujo bit menos significativo é igual a 1. Um BDD consegue, para muitos conjuntos que surgem na prática, guardar um conjunto definido por fórmula assim de forma muito mais compacta do que uma lista explícita dos seus membros exigiria e (esse é o ganho operacional, e não só uma economia de armazenamento) operações como "calcular os sucessores de todo estado deste conjunto" ou "fazer a interseção deste conjunto com aquele" podem ser feitas diretamente sobre a própria representação simbólica, de uma vez, para o conjunto inteiro (possivelmente enorme), em vez de exigir uma passada separada por cada estado membro, um por vez.

Contraexemplo espúrio

Suponha que uma abstração, no interesse de reduzir o espaço de estados, esqueça a relação precisa entre uma variável lock_owner (que registra qual processo, se algum, detém um lock no momento) e uma variável in_critical (que registra se algum processo está dentro da sua seção crítica no momento), talvez porque a abstração foi construída para checar outra propriedade e essa relação específica parecia, na época, irrelevante para ela. O model checker, explorando esse modelo abstraído, encontra um caminho em que nenhum processo é registrado como dono do lock e, mesmo assim, algum processo é registrado como estando in_critical; uma combinação que a abstração tecnicamente permite, já que a relação entre as duas variáveis foi descartada, mas que o sistema real e concreto pode de fato proibir totalmente (uma implementação de lock bem formada deveria fazer "estar na seção crítica" implicar "deter o lock", sempre). Esse caminho é um contraexemplo espúrio: um rastro genuíno pelo modelo abstraído que não corresponde a nenhuma execução concreta real do sistema de verdade, precisamente porque a abstração descartou exatamente a relação que o teria excluído. O refinamento é a resposta padrão: reintroduzir a relação faltante entre lock_owner e in_critical na abstração, tornando-a precisa o bastante para que esse caminho espúrio específico deixe de ser representável, mantendo ainda (se o refinamento for feito com cuidado) a abstração mais grosseira, e portanto menor, que o modelo totalmente concreto.

• Culpar a explosão do espaço de estados por hardware lento ou por uma ferramenta pouco otimizada. Como o argumento de contagem exponencial deixa explícito, o crescimento é um fato estrutural sobre quantas combinações genuinamente distintas um sistema com essa variabilidade de fato tem; hardware mais rápido compra alguma folga adicional, mas não consegue transformar uma curva de crescimento exponencial em uma administrável para modelos de tamanho realista, e é exatamente por isso que abstração, redução e representação simbólica existem como estratégias genuinamente diferentes, e não como mero ajuste de desempenho.
• Acrescentar detalhes a um modelo antes de perguntar se a propriedade sendo checada de fato precisa deles. Cada variável adicional, cada estado local distinguível adicional, multiplica diretamente o espaço de estados alcançável, como o exemplo de contagem mostra de forma concreta; o trabalho de um modelo é capturar exatamente o detalhe de que uma dada propriedade precisa, e a fidelidade desnecessária a cada detalhe de implementação do sistema real é um contribuinte direto e evitável exatamente da explosão de que este conceito trata.
• Presumir que a representação simbólica sempre supera a busca com estados explícitos. A compactação dos métodos simbólicos depende muito de uma regularidade estrutural que um BDD (ou uma representação parecida) consiga de fato explorar, e de encontrar uma boa ordem de variáveis; para alguns sistemas, a busca com estados explícitos com técnicas de redução como a redução por ordem parcial genuinamente supera uma abordagem simbólica, e nenhuma das estratégias é um padrão universalmente superior.
• Tratar um contraexemplo abstrato como definitivamente real sem concretização. Como o exemplo do contraexemplo espúrio mostra diretamente, um rastro que existe em um modelo abstraído não é automaticamente um rastro do sistema real; checar se um contraexemplo relatado de fato corresponde a uma execução concreta genuína (concretização) é um passo necessário antes de confiar nele, e não uma formalidade opcional, e pulá-lo arrisca perseguir um bug que a abstração fabricou, e não um que o sistema real de fato tem.

A explosão do espaço de estados não é uma deficiência de implementação, mas um fato estrutural e exponencial sobre como o número de estados alcançáveis de um modelo cresce a cada variável ou componente adicional: N flags booleanas independentes sozinhas já produzem até 2^N estados alcançáveis, e modelos realistas compõem isso com entrelaçamentos concorrentes, domínios de dados e escolhas do ambiente por cima. O model checking responde com duas famílias complementares de técnicas: reduções como a redução por ordem parcial e por simetria, que reconhecem e pulam a exploração redundante de entrelaçamentos e de estrutura intercambiável, e representações simbólicas como os BDDs, que descrevem conjuntos exponencialmente grandes de estados de forma compacta o bastante para manipulá-los diretamente, ao custo de depender de regularidade estrutural e de uma ordem cuidadosa de variáveis. A abstração, a mais agressiva dessas técnicas, compra as maiores reduções, mas arrisca introduzir contraexemplos espúrios que só existem no modelo simplificado, exigindo refinamento para restaurar exatamente as distinções de que uma propriedade de fato precisa; a mesma tensão fundamental entre correção, completude e escala a que theorem-proving-and-proof-assistants e the-limits-of-verification voltam, por ângulos diferentes, mais adiante nesta disciplina.