Problema da alcançabilidade

Alcançabilidade é um problema fundamental que aparece em diferentes contextos: sistemas concorrentes de variável de estado finito e infinito modelos computacionais como autómato celular e rede de Petri, análise de programas, sistemas discretos e contínuos, sistemas de tempo crítico, sistemas híbridos, sistema de redução, probabilístico e sistemas paramétricos, e sistemas abertos modelados como jogos.

Em geral o problema da alcançabilidade pode ser formulado da seguinte forma:

Dado um sistema computacional (potencialmente de estado infinito) com um conjunto de regras ou transformações permitidas, decida se um dado estado de um sistema é alcançável a partir de um dado estado inicial do sistema.

Variantes do problema da alcançabilidade podem resultar de restrições adicionais em seus estados inicial ou final, requerimentos específicos de caminhos de alcançabilidade assim como de alcançabilidade iterativa ou mudando as questões analisadas de estratégias para vencer jogos infinitos ou inevitabilidade de algumas dinâmicas.

Tipicamente, para um sistema fixo descritivo dado em alguma forma (regras de redução, sistemas de equações, fórmulas lógicas, etc.) um problema de alcançabilidade consiste em checar se um dado conjunto de estados alvos conseguem ser atingidos a partir de um conjunto fixo de estados iniciais. O conjunto de estados alvos podem ser representados explicitamente ou através de alguma representação implícita (e.g., um sistema de equações, um conjunto de elementos mínimos com respeito a uma ordem de estados). Propriedades quantitativas e qualitativas sofisticadas podem ser reduzidas a questões de alcançabilidade básicas. Decidibilidade e fronteiras complexas, soluções algorítmicas, e heurísticas eficientes são todos aspectos importantes para serem considerados neste contexto. Soluções algorítmicas são freqüentemente baseadas em uma combinação diferente de estratégias explorarias, manipulações simbólicas de conjuntos de estados, propriedades de decomposição, ou redução à problemas de programação linear, e freqüentemente se beneficiam de aproximações, abstrações, acelerações e heurísticas de extrapolação. Soluções ad hoc assim como soluções baseadas no uso geral de soluções com restrições e motores dedutíveis são muitas vezes combinados a fim de balancear eficiência e flexibilidade.

Oficina em Problemas da Alcançabilidade

A série Oficina em Problemas da Alcançabilidade é uma conferência acadêmica anual que agrupa pesquisadores de diversas disciplinas e áreas de conhecimento interessados em problemas de alcançabilidade que aparecem em estruturas algébricas, modelos computacionais, sistemas híbridos, jogos infinitos, lógica e verificação. A oficina tenta preencher o gap de resultados obtidos em diferentes áreas que compartilham estruturas matemáticas e dificuldades conceituais.