Sumários
Applications of Model Checking
10 dezembro 2015, 15:00 • Paulo Alexandre Carreira Mateus
Applications of Model Checking to the verification of concurrent and distributed systems. Fairness. Critical section, mutual exclusion. Consumers/producers problem. Channels. The dinning philosopher problem and the Byzantine agreement problem. Statement of impossibility results.
Model checking of Markov Chains
7 dezembro 2015, 09:00 • Paulo Alexandre Carreira Mateus
Markov chains and Markov decision processes. Model-checking of reachability properties. Fix point characterisation.
Verificação de modelos probabilistica.
3 dezembro 2015, 15:00 • Paulo Alexandre Carreira Mateus
Exogenous Probabilistic Propositional Logic (EPPL): Syntax, semantics and complete Hilbert calculus. SAT algorithm and model-checking. LTL extension of EPPL. SAT algorithm for finite models. Markov chains. Infinite model generated by a Markov chain. Approximate model checking for Markov chains.
T11 - Manipulação de ROBDDS
30 novembro 2015, 09:00 • David João Barros Henriques
Regras de redução de OBBDS. Correcção e completude das regras. Manipulação eficiente de ROBDDs.