Esta disciplina tem por objectivo introduzir a modelação, especificação e verificação de sistemas concorrentes.
Após uma breve introdução aos sistemas de transição de estados, a primeira parte da disciplina foca-se nas redes de Petri: um modelo gráfico muito poderoso para representar sistemas concorrentes de média e alta complexidade. Ainda nesta primeira parte, serão introduzidas técnicas para verificar propriedades de sistemas concorrentes através da análise directa das redes.
A segunda parte da disciplina tem por ênfase a especificação e verificação de propriedades de sistemas concorrentes usando lógica temporal. Em particular, será utilizada a lógica de tempo ramificado CTL, para a qual serão apresentadas diferentes técnicas de verificação de modelos.
Na componente prática laboratorial serão utilizadas ferramentas para edição gráfica de redes de Petri e para verificação simbólica de modelos.