TCS / Studies / T-79.5301 Reactive Systems
Helsinki University of Technology, 
     Department of Information and Computer Science

T-79.5301 Reactive Systems (4 cr) P

Spring 2008 (Periods III and IV)

Previous years: [Spring 2007] [Spring 2006]

Reactive systems can be found in many embedded systems such as microprocessors, telecommunication systems and data communication networks. Their central feature is non-terminating behavior and reaction to stimuli provided by the environment.

The modeling and verification of reactive systems has become a natural part of the system development cycle in the design of VLSI circuits. Similar techniques can also be applied, e.g., to the design and implementation of data communication protocols.

The course covers the basic theory of modeling reactive systems using automata, specifying requirements on the behavior of such models using temporal logic, and verifying these properties using model checking algorithms.

Course coordinator: Heikki Tauriainen.

Lectures and Seminars: Tuesdays 16-18 in room B353 (Computer Science building).

Tutorials: Tuesdays 18-19 (room B353).


  • B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, Ph. Schnoebelen, and P. McKenzie: Systems and Software Verification - Model-Checking Techniques and Tools. Springer, 1999. (Chapters 1-2, 6-11)
  • E. M. Clarke Jr., O. Grumberg, and D. A. Peled: Model Checking. The MIT Press, 1999. (Chapters 3-4, 9-11)
  • Z. Manna and A. Pnueli: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, 1992. (Chapters 3.3, 4.2)
  • Scientific articles.

To pass the course, you should:

  1. give three seminar talks (30-40 min / talk), and
  2. earn at least 50 % of points awarded from three home assignments (15 points / assignment).
Completing the above tasks will earn you a basic grade of 3. Earning 70 % (90 %) of the points from the home assignments will raise your final grade to 4 (5, respectively).

Schedule for Spring 2008

Lecture slides (with corrections to the versions distributed on paper)

  • Automata and synchronization [PS] [PDF]
  • Temporal logics [PS] [PDF]
  • Safety properties [PS] [PDF]
  • Fairness properties [PS] [PDF]
  • Syntactic classification of temporal formulas [PS] [PDF]
  • Automata-theoretic model checking [PS] [PDF]
  • Translating LTL to Büchi automata [PS] [PDF]
  • Model checking with fairness constraints; CTL* model checking [PS] [PDF]
  • Partial order reduction for LTL-X [PS] [PDF]
  • Partial order reduction: Complexity, heuristics and correctness [PS] [PDF]

Home assignments

Final results of the course (19 May, 2008)

Literature for seminar talks

Reserved topics are denoted by ***.

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 19 May 2008.