• Redes de Petri
    • Modelação de sistemas concorrentes com redes de Petri.
    • Cálculo de matrizes de incidência.
    • 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.
    • Redes coloridas.
    • Ferramentas para especificação e animação de redes de Petri (DaNAMiCS, PEP).

  • Verificação de modelos
    • Especificação de propriedades de segurança e animação usando lógica temporal.
    • Lógicas CTL*, CTL e LTL.
    • 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).