D1 – KNOWLEDGE AND UNDERSTANDING
At the end of the course, the student should be able to:
Understand the concept of bisimilarity and the algorithms for calculating a bisimulation
Understand the concept of action-based branching time logic
Understand the issues related to time critical systems and the need of expanding non-deterministic formalisms with time
Understand the concepts of clock variables, timed automata, timed paths, divergence and zenoness
Illustrate the syntax and the semantics of Timed Computation Tree Logic (TCTL)
Understand the concept of clock regions and zones and illustrate how they can be used to realize the model checking of TCTL
Understand the concept of probabilistic and stochastic systems and their verification
Illustrate the definition of Discrete Time Markov Chains (DTMC), Markov Decision Processes (MDP) and Continuous Time Markov Chains (CTMC)
Illustrate the syntax and the semantics of Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL)
D2 – APPLYING KNOWLEDGE AND UNDERSTANDING
At the end of the course, the student should be able to:
Determine if two states of a transition system are bisimilar
Use the Hennessy-Milner Logic with recursion for specifying untimed properties
Use the formalism of Timed Automata to model real-time systems
Use the tool UPPAAL to verify real-time systems
Use the formalisms of DTMC, MDP and CTMC to model probabilistic or stochastic systems
Use the tool PRISM to verify probabilistic or stochastic systems
D3 – MAKING JUDGEMENTS
At the end of the course, the student should be able to:
Identify the best model suitable for describing a system using a given formalism
D4 - COMMUNICATION SKILLS
At the end of the course, the student should be able to:
Write a clear report on the modelling and analysis of a system under study using a formal style
D5 – LEARNING SKILLS
At the end of the course, the student should be able to:
Search the scientific literature for specific advances in formalisms and tools aimed at modelling and verifying timed, stochastic and probabilistic systems
Autonomously understand and learn to use new features added to tools for modelling and verifying timed, stochastic and probabilistic systems