= Introduction to Discrete-Systems Theory =

== Synopsys ==

''Discrete-state systems'' are the systems whose state evolves via a sequence of discrete, instantaneous state-changes. 
Examples of discrete-state systems are hardware systems, embedded software systems, mixed hardware-software systems, as well as general software systems. 
Examples of systems which are not discrete-state include many systems studied in physics and mechanics, whose state evolves in a continuous fashion in time, as well as physical systems with their digital control. 

The course provides an introduction to the modeling, specification, verification and analysis of discrete-state systems. The course will emphasize applications to hardware systems and embedded software systems, and will introduce concepts that can be used to reason on general software systems. 

== The Basics ==

 * '''Instructor:''' [http://www.soe.ucsc.edu/~luca Luca de Alfaro]]
 * '''Email:''' ''my_first_name''@soe.ucsc.edu
 * '''Location:''' 10:00-11:45, TTh, Porter Acad 246
 * '''Office Hours:''' Tuesdays, 1-2pm, or by appointment (email the instructor)

'''Textbook:''' We will use various material available on the web; all reading resources will be available at this web page. 

'''["Discrete-Systems Syllabus"]'''

== Reading Material ==

=== Lecture Notes ===
 * [attachment:lecture_notes.pdf My lecture notes]
 * [attachment:notation.pdf Notation]

=== Other readings ===
 * [http://mtc.epfl.ch/courses/ModelChecking-2007/Notes/3.pdf Notes on BDDs], from [http://mtc.epfl.ch/courses/ModelChecking-2007/ a class taught at EPFL by Tom Henzinger]. 
 * [http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/Papers.html Papers on MiniSat], the SAT-solver.
 * [http://www.soe.ucsc.edu/~luca/papers/07/concur07.html Three-valued abstraction paper], describing the refinement method described in class. 
 * [http://mtc.epfl.ch/~tah/Publications/temporal_safety_proofs_for_systems_code.html Temporal Safety Proofs for Systems Code], the paper on BLAST described in class. 
 * [http://www.c-program.com/kt/reflections-on-trusting.html Kernighan's Trojan Horse] (highly recommended reading).
== Homework ==
 * Homework 1, due Thursday October 4: Problem 2, page 8.  
 * Homework 2, due Thursday October 11: Problems 3 and 4, page 10. 
 * [:CMPE 278 2007 HW 3: Homework 3], on implementation of BDD operations, due Thursday October 25. 
 * [:CMPE 278 2007 HW 4: Homework 4], the traffic light example. 
 * [:CMPE 278 2007 HW 5: Homework 5], verification of the traffic light example.