Uso de Abordagens de Verificação Formal na Síntese de Controladores para Sistemas de Eventos Discretos com especificações Lógicas e Temporais

Descrição

Este projeto de pesquisa investiga o uso de técnicas de verificação formal, em particular a verificação de propriedades expressas em lógicas temporais quantitativas (TCTL e fragmentos relacionados), como etapa central na síntese de controladores (supervisores) para Sistemas a Eventos Discretos temporizados (TDES). Partindo das limitações conhecidas da Teoria de Controle Supervisório clássica quando aplicada a sistemas com restrições de tempo — especialmente a dificuldade de construir a linguagem supremamente controlável a partir de restrições modeladas apenas por autômatos —, propõe-se uma abordagem híbrida. Nela, o comportamento desejado é obtido por meio da verificação formal local de especificações lógicas e temporais sobre o grafo de classes de estados de Redes de Petri Temporizadas (utilizando a partição Stable State Zone Graph – SSZG). A partir do autômato temporizado resultante (Timed Transition Graph), são então associados intervalos de tempo mínimos e máximos às transições controláveis, permitindo a obtenção da linguagem supremamente controlável. O trabalho fundamenta-se na Teoria de TDES de Brandin e Wonham (1994), nas abordagens de supervisão baseadas em Redes de Petri de Basile, Cordone e Piroddi (2022) e nos resultados recentes de síntese por classes de estados de Leclercq, Lime e Roux (2023), integrando-os com técnicas avançadas de abstração de espaço de estados (SSZG) desenvolvidas pelo proponente. Espera-se como resultado uma metodologia completa, algoritmos implementáveis e suporte computacional (extensão da ferramenta Corona) para a síntese de controladores em sistemas a tempo real com especificações mistas lógicas e quantitativas.