Elementos Lógicos da Programação III
Licenciatura de Matemática e Ciências da Computação
3º Ano - 2º Semestre
Ano lectivo 2003/2004
Ùltima alteração: 12/07/2004
Avisos
- 29/07: Já disponíveis as notas da época de recurso (Notas).
- 12/07: Já disponíveis as notas da 1ª e 2ª chamadas (Notas).
- 07/05: Já disponível o enunciado dos projectos práticos.
- 22/03: Disponíveis duas novas secções nesta página: Elementos de Estudo e Apontadores WEB.
- 25/02: Nos dias 2 e 3 de Março (segunda e terça) não haverá aulas Teórico-Práticas de ElementosLogicosProgramacaoIII0304.
- 25/02: Este ano a página da disciplina é alojada no WIKI. Contacte um docente se pretender colaborar na manutenção da página.
Programa
Programa Resumido
- Redes de Petri
- Introdução aos modelos da concorrência
- Sistemas de transição de estados: bissimulação.
- Estruturas de eventos/redes de ocorrências.
- Redes de Petri coloridas
- Verificação de Modelos
- Lógicas temporais: CTL e CTL+
- Verificação simbólica
Programa Detalhado
Bibliografia
Bibliografia Recomendada:
- Elements of Distributed Algorithms: modeling and analysis with petri nets; Wolfgang Reisig. Springer-Verlag 1998.
- Model Checking; Edmund M. Clarke Jr., Orna Grumberg, and Doron A. Peled. MIT Press 2001.
Elementos de Estudo
- 16/04 Uma nova versão do Animador que já suporta redes coloridas (Net2.tgz)
- 05/04 Nova verão dos módulos do Animador que fazem uso de multi-parameter type classes para permitir um maior nível de abstracção. (Net.tgz) --- Obs.: Para executar estes módulos devem-se passar as seguintes opções ao GHC:
"-fglasgow-exts -fallow-undecidable-instances"
.
- 05/04 Versões simplificadas do animador de redes de Petri apresentado na teórica:
- Versão I - Não define novas classes; utiliza o transformador de estados da biblioteca. (RPetri.hs)
- Versão II - Evita a utilização do monad de estado. (RPetri2.hs)
- 05/04 Várias resoluções para os exercícios da aula sobre o Monad de Estado:
- Versão I - Monad definido explicitamente (como foi apresentado na aula prática). (StateEx1.hs)
- Versão II - Usando a biblioteca standard. (StateEx2.hs)
- Versão III - Usando State threads. (StateEx3.hs)
- 22/03 Programa em Haskell para animação de Redes de Petri demonstrado nas aulas teóricas: (rp-jmv.tgz)
Apontadores WEB
Projectos Práticos
Horário e Equipa docente
Horário Lectivo:
Teóricas | Práticas |
2ª, das 10:00 às 11:00 (sala CP1.A2) | TP1 , 2ª, das 14:00 às 16:00 (sala DI 0.11) |
5ª, das 9:00 às 10:00 (sala CP2.103) | TP2 , 3ª, das 9:00 às 11:00 (sala DI 0.11) |
Horário de Atendimento:
JMV | JBA |
| 2ª, das 11:00 às 13:00 |
| 2ª, das 16:00 às 19:00 |
Critério de Avaliação
Nota final é calculada com base nas seguintes componentes:
Componente Teórica (Exame) - OBRIGATÓRIA - peso nunca inferior a 60% (nota mínima de 8 valores).
Componente Prática - FACULTATIVA - com peso máximo de 30%.
A componente prática consiste na realização de um projecto.
Notas
- Notas das épocas normais e de recurso (PDF)