Verificação e síntese de controladores de realimentação de estados estática com garantias formais de desempenho não frágil - Cavalcante, Thiago Rodrigo Félix (2019)
Neste trabalho, uma abordagem para a realização de verificação e síntese de sistemas de controle discreto com realimentação de estados foi descrita, levando-se em consideração requisitos de desempenho da resposta ao degrau em sistemas de controle, a qual é baseada em técnicas de síntese indutiva guiada por contraexemplo (counter-example guided inductive synthesis - CEGIS). Nesse esquema, requisitos de desempenho (e.g., tempo de assentamento e máximo sobressinal) são avaliados, em um determinado sistema de controle, com o objetivo de verificar se os valores desejados são atendidos. Caso isso não aconteça, torna-se necessário encontrar um sistema que possibilite isso e, nesse caso, um controlador é novamente projetado. Para a geração de controladores, uma técnica de aprendizagem que se baseia em algoritmo genético foi utilizada, onde, a cada iteração em que um requisito não seja satisfeito, sabe-se que o controlador associado não é adequado. Na verificação desses requisitos de desempenho, em sistemas de controle discreto, considerou-se fragilidade (erros de quantização numérica, arredondamentos, efeitos de palavra de máquina finita, etc) nos controladores utilizados. A abordagem desenvolvida é útil para auxiliar engenheiros em seus projetos de sistemas de controle discretos, visto que fragilidades normalmente ocorrem durante implementações em plataformas digitais e, nesse caso, um sistema que atenda os requisitos desejados pode ser gerado. A sua implementação ocorreu dentro da ferramenta DSVerifier, que é baseada em verificação limitada (e ilimitada) de modelos e teorias de módulo de satisfabilidade. A metodologia proposta foi avaliada em um conjunto de padrões de teste clássicos (benchmarks) de sistemas de controle, extraídos da literatura, bem como em casos específicos e considerando diferentes autovalores e configurações de controladores. Os resultados experimentais mostram a sua eficácia em síntese de sistemas de controle discreto com realimentação de estados, levando-se em consideração requisitos de desempenho, visto que considera problemas práticos de implementação, o que não ocorre com outros métodos existentes.