Redes de Petri

• Modelação de sistemas concorrentes com redes de Petri.
• Semântica operacional baseada em sistemas de transição de estados.
• Propriedades fundamentais de redes: finitude, animação e invertibilidade.
• Cálculo de invariantes de estado.
• Extensões às redes não coloridas: lugares com capacidade explicita e arcos inibidores.
• Ferramentas para especificação e animação de redes de Petri (DaNAMiCS, PEP).

Lógica Temporal

• Especificação de propriedades de segurança e animação usando lógica temporal CTL.
• Representação mínima de fórmulas CTL.
• Verificação directa de modelos para a lógica CTL.
• Representação da relação de acessibilidade usando lógica proposicional.
• Verificação simbólica de modelos para a lógica CTL baseada em OBDDs.
• Ferramentas para verificação simbólica de modelos (SMV).

Álgebra de Processos

• Autómatos e sistemas de transição. Interacção e comportamento.
• Modelação de sistemas reactivos em CCS. Semântica operacional. Análise e verificação de transições.
• Cálculo de sistemas reactivos. Equivalência estrita e observacional em CCS. Teorema da expansão. Resolução de equações.
• Cálculo de sistemas móveis. Motivação, sintaxe, semânticas e equivalências entre processos móveis.
• Animação e análise de processos no CWB e no MWB.