Real-time and Probabilistic System Verification

News

  • September 7th, 2016: the course web site is now on-line
  • October 3rd, 2016: first lecture
  • November 2nd, 2016: lectures are suspended form 27th October 2016 until further notice due to the earthquakes of the last days.

General Info

Teacher:

Lessons schedule:

  • Mon 5.00 am - 7.00 pm @ Room D. M. Ritchie, 2nd floor, Palazzo di Informatica (ex Tribunale), Piazza Mazzini 1, Camerino new time table and new room will be communicated as soon as information about the restart of lectures will be available
  • Wed 11.00 am - 1.00 pm @ Room D. M. Ritchie, 2nd floor, Palazzo di Informatica (ex Tribunale), Piazza Mazzini 1, Camerino new time table and new room will be communicated as soon as information about the restart of lectures will be available

Lectures start on 3rd October 2016.

New schedule after earthquake (from Wed 7/12/2016 on):

  • Wed 9.00 am - 11.00 am @ Room AB2, 2nd floor, Polo Lodovici, via Madonna delle Carceri 9, Camerino.
  • Thu 9.00 am - 11.00 am @ Room AB1, 2nd floor, Polo Lodovici, via Madonna delle Carceri 9, Camerino.

Students Office hours:

  • Wed 3.00 pm - 5.00 pm - Luca Tesei's Room CS07 2nd Floor of Polo Tecnologico Palazzo Battibocca, via del Bastione 1, Camerino. Possible changes are advertised here
  • I will be available for online or face to face office hours by appointment, write to me at luca.tesei@unicam.it

Prerequisites

  • Having passed the course “Reactive Systems Verification” alias “Model Checking I”

Course Objectives

D1 – KNOWLEDGE AND UNDERSTANDING

At the end of the course, the student should be able to:

  1. Understand the concept of bisimilarity and the algorithms for calculating a bisimulation
  2. Understand the concept of action-based branching time logic
  3. Understand the issues related to time critical systems and the need of expanding non-deterministic formalisms with time
  4. Understand the concepts of clock variables, timed automata, timed paths, divergence and zenoness
  5. Illustrate the syntax and the semantics of Timed Computation Tree Logic (TCTL)
  6. Understand the concept of clock regions and zones and illustrate how they can be used to realize the model checking of TCTL
  7. Understand the concept of probabilistic and stochastic systems and their verification
  8. Illustrate the definition of Discrete Time Markov Chains (DTMC), Markov Decision Processes (MDP) and Continuous Time Markov Chains (CTMC)
  9. 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:

  1. Determine if two states of a transition system are bisimilar
  2. Use the Hennessy-Milner Logic with recursion for specifying untimed properties
  3. Use the formalism of Timed Automata to model real-time systems
  4. Use the tool UPPAAL to verify real-time systems
  5. Use the formalisms of DTMC, MDP and CTMC to model probabilistic or stochastic systems
  6. 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:

  1. 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:

  1. 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:

  1. Search the scientific literature for specific advances in formalisms and tools aimed at modelling and verifying timed, stochastic and probabilistic systems
  2. Autonomously understand and learn to use new features added to tools for modelling and verifying timed, stochastic and probabilistic systems

Course Contents

  • Bisimilarity and bisimulation, calculating the quotient set through partition refinement.
  • Theory of fixed points.
  • Hennessy-Milner Logic with Recursion.
  • Real-time systems and timed formalisms.
  • Timed Automata. Timed Computation Tree Logic (TCTL).
  • Clock Regions and Zones.
  • The UPPAAL Tool.
  • Probabilistic and Stochastic Systems.
  • Discrete Time Markov Chains (DTMC), Markov Decision Processes (MDP) and Continuous Time Markov Chains (CTMC).
  • Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL).
  • The tool PRISM.

Study material

Lectures

Reference books

  • Luca Aceto, Anna Ingolfsdottir, Kim Guldstrand Larsen and Jiri Srba, “Reactive Systems. Modelling, Specification and Verification”, Cambridge University Press, 2007. ISBN: 9780521875462 – Website
  • Christel Baier, Joost-Pieter Katoen, “Principles of Model Checking”, The MIT Press, ISBN: 9780262026499
  • Michael Huth, Mark Ryan, “Logic in Computer Science: Modelling and Reasoning about Systems”, Cambridge University Press. ISBN: 9780521543101.
  • Glynn Winskel, “Formal Semantics of Programming Languages”, The MIT Press, ISBN: 9780262731034.

Exams

Assignments

  • Assignment 1 - Self-study report on “Partition-based minimization algorithm for Finite State Automata recognizing regular languages”, deadline 14/10/2016 23.59. Send the pdf by email to luca.tesei@unicam.it
  • Assignment 2 - Text of the Assignment, deadline 10/02/2017 23.59.
  • Assignment 3 - Text of the Assignment, deadline 10/03/2017 23.59.

Exam Dates A.Y. 2016/2017

  • Winter session dates here
  • Summer session dates here
  • Autumn session dates here
  • Winter session dates here (2016)

Exam rules:

Exam Results

  • TBA