Sumários
Objectivos da disciplina e tópicos do programa: parte I e parte II. Métodos de avaliação. Bibliografia recomendada.
Breve introdução à programação concorrente: processos e interação. Paralelismo e Concorrência
Sylabus and objectives: part I and part II. Assessment methods. Bibliography. Short introduction to concurrent programming: processes and interaction. Paralelism and concurrency
Modelo abstracto de processos: sistemas de transição. Estados e Ações. Sucessores de um estado. Estados atingíveis. Determinismo e Não determinismo. Tipos de Sistemas de transição. Processos Concorrentes.
Labeled transition Systems. States and actions. Successors of State. Reachable states.Determinism and nondeterminism. Types of transition systems. Concurrent
processes.
Breve introdução à programação concorrente: processos e interação. Paralelismo e Concorrência
Sylabus and objectives: part I and part II. Assessment methods. Bibliography. Short introduction to concurrent programming: processes and interaction. Paralelism and concurrency
Modelo abstracto de processos: sistemas de transição. Estados e Ações. Sucessores de um estado. Estados atingíveis. Determinismo e Não determinismo. Tipos de Sistemas de transição. Processos Concorrentes.
Labeled transition Systems. States and actions. Successors of State. Reachable states.Determinism and nondeterminism. Types of transition systems. Concurrent
processes.
Bibliografia
CPAPF: Cap 1., 3.1.1, 3.2.1 3 3.3.1. Ler ainda 3.2.2 e 3.3.2
ITC: 2.1 e 2.2
CPAPF: Cap 1., 3.1.1, 3.2.1 3 3.3.1. Ler ainda 3.2.2 e 3.3.2
ITC: 2.1 e 2.2
CCS sequencial: operadores prefixo e escolha.Semântica das expressões por sistemas de transições. Regras de inferência.
CCS sequential: prefix and choice. Semantics of expressions as transition systems. Inference rules.
Nomes de processos e definições recursivas. Expressões guardadas. Regra de inferência para a recursão.
Process names and recursive definitions. Guarded expressions. Inference rule for recursion
CCS sequential: prefix and choice. Semantics of expressions as transition systems. Inference rules.
Nomes de processos e definições recursivas. Expressões guardadas. Regra de inferência para a recursão.
Process names and recursive definitions. Guarded expressions. Inference rule for recursion
Bibliografia
O operador composição paralela. Acções de entrada e de saída. Ações complementares. Sincronização. O operador de restrição (para forçar a sincronização). Regras de inferência.
Parallel composition. Input and output actions. Complementary actions. Synchronisation. Restriction (forcing synchronisation). Inference rules.
Exemplos com composição paralela e restrição. Operadores dinâmicos e estáticos. O CCS regular. Exemplos de buffers e protocolos.
Examples of parallel composition, synchronisation and restriction. Dynamic and static operators. CCS regular. Examples of buffers and protocolos (Sender/receiver).
Parallel composition. Input and output actions. Complementary actions. Synchronisation. Restriction (forcing synchronisation). Inference rules.
Exemplos com composição paralela e restrição. Operadores dinâmicos e estáticos. O CCS regular. Exemplos de buffers e protocolos.
Examples of parallel composition, synchronisation and restriction. Dynamic and static operators. CCS regular. Examples of buffers and protocolos (Sender/receiver).
Bibliografia
Equivalência de comportamentos de Processos. Traços. Critérios para a equivalência: relações de equivalência, de congruência e sensíveis a deadlocks. Isomorfismo e equivalência de traços. Bissimulação (forte). Bissimilaridade. Prova da bissimilaridade de dois processos. Jogo de bissimulação.
Equivalence of process behaviours. Traces. Equivalence criteria: equivalence, congruence, termination sensitivity. Isomorphism and trace equivalence. Bisimulation (strong). Bisimilarity. Proving and disproving bisimilarity. Bisimulation games.
Equivalence of process behaviours. Traces. Equivalence criteria: equivalence, congruence, termination sensitivity. Isomorphism and trace equivalence. Bisimulation (strong). Bisimilarity. Proving and disproving bisimilarity. Bisimulation games.
Bibliografia
RS: 3.1, 3.2; PB (Equality) ITC 2.3.1-2
Aula 9/10 14/3/2024
Propriedades da Bissimularidade. Ignorar ações internas. Bissimilaridade fraca. Prova da bissimilaridade fraca de dois processos. Exemplos de bissimulação fraca. Propriedades da bissimilaridade fraca.
Jogos de bissimilaridade fraca. Bisimilaridade fraca não é uma congruência. Congruência para a escolha. Congruência Observável. Igualdade observável. Minimização de Sistemas de Transição.
Properties of bisimilarity. Weak bisimulations. Weak bisimilarity. Examples and properties. Games of weak bisimilarity. Bisi,imarity is not a congruence. Observable congruence. Equality of Processes. Minimization of LTSs.
Jogos de bissimilaridade fraca. Bisimilaridade fraca não é uma congruência. Congruência para a escolha. Congruência Observável. Igualdade observável. Minimização de Sistemas de Transição.
Properties of bisimilarity. Weak bisimulations. Weak bisimilarity. Examples and properties. Games of weak bisimilarity. Bisi,imarity is not a congruence. Observable congruence. Equality of Processes. Minimization of LTSs.
Bibliografia
RS: 3.3, 3.5 Pseuco Book (Equality)
Para jogos de bissimulação: CAAL (sintaxe do CCS diferente do pseuco.com)
Para quem quiser saber mais sobre bissimulações (facultativo): "Introduction to Bisimulation and Coinduction", D. Sangiori 2012, CUP
Expressividade do CCS. Escrita de programas imperativos em CCS: Algoritmo de Peterson para a exclusão mútua.
CCS com passagem de valores (CCS_vp). Regras para substituir variáveis por valores e calculo de valores. Parâmetros em nomes de processos e regra da recursão. Representação de escrita e leitura em células de memória, Programas funcionais e imperativos em CSS_vp. CCS_vp embebido em CCS.
Expressivity of CCS. Mutex algorithms. Value- passing CCS. Rules for substituting variables by values: CCS_vp. Memory cells.
CCS com passagem de valores (CCS_vp). Regras para substituir variáveis por valores e calculo de valores. Parâmetros em nomes de processos e regra da recursão. Representação de escrita e leitura em células de memória, Programas funcionais e imperativos em CSS_vp. CCS_vp embebido em CCS.
Expressivity of CCS. Mutex algorithms. Value- passing CCS. Rules for substituting variables by values: CCS_vp. Memory cells.