Interacção e Concorrência - Edição 2013-14
Objectivos
Este curso tem por objectivo o estudo de
sistemas reactivos, com ênfase na sua composição
concorrente e no controlo da
interacção continuada com o ambiente.
Serão introduzidas técnicas de especificação de propriedades, modelação, análise e verificação deste tipo de sistemas, assim como lógicas apropriadas.
O curso aborda, essencialmente, sistemas reactivos clássicos; serão brevemente mencionados sistemas com requisitos de mobilidade.
Programa Resumido
- Introdução aos sistemas reactivos: estado, comportamento, interacção e concorrência.
- Sistemas reactivos
- Automatos e sistemas de transição.
- Processo e comportamento.
- Similaridade e bisimilaridade.
- Álgebras de Processos
- Introdução às álgebras de processos.
- Modelação e cálculo de sistemas reactivos em CCS e mCRL2.
- Mobilidade e o Pi-calculus.
- Lógicas para sistemas reactivos
- Lógica de Hennessy-Milner e suas extensões.
- Lógicas modais e híbridas.
- Lógicas temporais.
- Especificação de propriedades e sua verificação.
- Introdução às técnicas de model-checking.
- Laboratório: modelação e análise de sistemas reactivos em mCRL2
Bibliografia base
Bibliografia complementar
Software
Material de Apoio
Acetatos
Sistemas de transição etiquetados
Simulação e bissimulação
Álgebra de processos
Introdução à modelação de processos em mCRL2
Lógica modal sobre processos
Exercícios
Folha de Exercícios 1
Folha de Exercícios 2
Folha de Exercícios 3
Folha de Exercícios 4
Folha de Exercícios 5
Folha de Exercícios 6
Projectos
Projectos em mCRL2 (Parte 1)
Docente
Avaliação
- Prova individual escrita sem consulta (80%)
- Trabalho prático de síntese de conhecimentos para realização em grupos de 3 elementos e discussão nas aulas (20%)
- As notas finais superiores ou iguais a 19 valores poderão necessitar de ser defendidas em prova oral.
Provas
Aviso (Provas orais)
As orais realizam-se no dia 18 de Julho, sexta-feira, entre as 10 e as 13h no gabinete do docente.
A não comparência determina automaticamente a reprovação na UC
Horário
Atendimento
--
Luís Soares Barbosa - 18 Julho 2014, 21.45h