Models that include a notion of time are ubiquitous in disciplines such as the natural sciences, engineering, philosophy, and linguistics, but in computing the abstractions provided by the traditional models are problematic and the discipline has spawned many novel models. This course offers a systematic, thorough presentation of the results of several decades of research on developing, analyzing, and applying time models to computing and engineering. It is based on the homonymous book authored by the teachers of the course: Furia, C.A., Mandrioli, D., Morzenti, A., Rossi, M.

The course aims at developing the ability to critically evaluate models to represent and analyze the time behavior of complex, heterogeneous systems and possibly to adapt existing ones to the specific needs of particular applications.

The topics covered by the course are the following ones:

General remarks on the models to represent time and on the languages to describe them and their properties.

"Dimensions" for their evaluation and comparison.

Traditional models revisited at the light of the above dimensions: dynamical systems, electronic devices, automata and their complexity.

Synchronous abstract machines: transition systems; timed, hybrid, stochastic automata.

Asynchronous abstract machines: Petri nets, timed Petri nets, Petri nets with inhibitor arcs; stochastic Petri nets.

Algebraic formalisms: communicating sequential processes; process algebras and their probabilistic version.

Logic-based formalisms: linear and branching time temporal logic; TRIO; interval-based temporal logic; probabilistic temporal logic.

Verification and the dual language approach: model checking; axiomatic verification of timed Petri nets.

During the lectures the teachers will propose a few exercises related to the presented topics.

At the end of the course, and, in any case within the end of May, each student will deliver at his/her own choice at least two among the proposed exercises which will be evaluated by the teachers.