Dissertação

Supervisory Control of Petri Nets using Linear Temporal Logic EVALUATED

Atendendo à necessidade de métodos autómaticos de síntese e análise de tarefas robóticas complexas, propõe-se uma metodologia que permite a um projectista de tarefas robóticas usando redes de Petri garantir propriedades relacionados com eventos, partindo de redes de Petri mais simples. Utilizam-se conceitos de trabalhos anteriores de Supervisory Control de sistemas de eventos discretos. As especificações são dadas em QPLTL, uma lógica temporal linear com quantificadores estritamente mais expressiva que LTL. Esta abordagem formal é suficientemente próxima aos nossos raciocínios internos, permitindo poupar tempo gasto ao projectar uma tarefa robótica em forma de rede de Petri. Devido à necessidade de investigar linguagens omega reconhecidas por redes de Petri para o foco principal do trabalho, sugere-se ainda uma extensão do conceito de autómato de Büchi generalizado, incluindo ainda um teorema que permite caracterizar as linguagens omega reconhecidas por redes de Petri.
Redes de Petri, Supervisory Control, Lógica Temporal Linear

Janeiro 25, 2010, 14:30

Publicação

Obra sujeita a Direitos de Autor

Orientação

CO-ORIENTADOR

Paulo Alexandre Carreira Mateus

Departamento de Matemática (DM)

Professor Associado

ORIENTADOR

Pedro Manuel Urbano de Almeida Lima

Departamento de Engenharia Electrotécnica e de Computadores (DEEC)

Professor Associado