Date  Topics details 
Dec 30  Introduction, basic notion of synchronous and
asynchronous systems; globally synchronized
views of time. Notion of a system and its environment.
Delay models: delay insensitive,
quasidelay insensitive, speed independent and
timed systmes 
Jan 2  Small examples of delay insensitive, quasidelay
insensitive and timed systems. Petri Nets as a
mechanism of specifying behaviour at the interface
between a system and its environment. Petri Net
basics: definition, markings, rules for transition
firing, mathematical notation. Representing concurrency,
synchronization, choice/conflict, sequencing,
merge of events using Petri Nets. ksafeness and
1safeness of Petri Nets 
Jan 8  Talk by Prof. Jordi Cortadella. Trace set of a Petri Net.
More on equivalence of ksafe and 1safe Petri Nets 
Jan 9  Petri Nets: free choice, extended free choice, liveness.
1safe Petri Nets and state transition diagrams:
comparison of benefits of each formalism. Going from
Petri Nets to state transition diagrams and vice versa.
Introduction to a CSPbased process algebra:
syntax and semantics. Finite and infinite processes.
Sequential composition, nondeterministic choice,
guarded actions, tail recursion for defining
infinite processes

Jan 15  Institute holiday 
Jan 16  More of process algebra syntax and semantics: parallel
or concurrent composition. Expressive equivalence of
process algebra described and Petri Nets. Converting
Petri Nets to process algebraic descriptions and vice
versa. Example of a scalable queue described using
process algebraic constructs.

Jan 22  Handshakes as a mechanism of communication: two and
fourphase handshakes. Notion of channels, ports,
active and passive handshakes. Martin's CHP
description of processes; their handshaking expansion.
Effect of placing handshaking actions at different
points in a sequence of handshakes.
Example of a sequencer process with a passive L
port and two active R (R1, R2) ports:
its CHP description.

Jan 23  Expansion of CHP of description of sequencer
into 2phase handshakes. Production rules (PR):
definition, identifying PRs from a handshaking
expansion, naive implementation from PRs.
Implementation of sequencer and its environment
using wires (buffers) and a negation gate.
4phase handshaking expansion of sequencer CHP
description; obtaining PRs from this expansion.
Stability and noninterference of PRs.
Interference among PRs obtained from 4phase handshaking
expansion of the sequencer. Reshuffling of
handshaking actions, and how it helps remove
some of the interference between PRs.

Jan 29  Further reshuffling of 4phase handshaking events
of sequencer. Illustration of how reshuffling can
help yield simpler designs. Strongest precondition
of an event in a process description. Mutually
exclusive strongest preconditions. Deriving stable
guards (strongest guards) from strongest
preconditions.

Jan 30  Tutorial 1: Toggle and Merge elements.
Combining Toggle and Merge elements to obtain
a 2phase to 4phase (or vice versa) handshake
converter.

Feb 5  Combining strongest preconditions of same event (action)
occurring at different points in a process description.
Mutually exclusive strongest preconditions:
necessary and sufficient conditions for existence
of a stable PR set. Deriving strongest and weakest
guards of an event.

Feb 6  Simplifying strongest guards of PRs using don'tcare
sets from process description. Illustration
with simple sequencer having 4phase handshakes.
Strengthening weakest guards of PRs by inspection,
while ensuring that there are
no conflicting assignments to the same variable/port.
Symmetrization of guards enabling assignment of
conflicting values to same variable/port.
Illustration with simple sequencer.

Feb 12  Decomposition of a process into an interconnection
of linear processes using specialized elements like
Merge, Celement (synchronizer), Arbiter. Notion of
waking up and going to sleep in the context of
processes.

Feb 14  More on decomposition of processes. Dealing with
concurrency, synchronization, choice
when decomposing a process. Simple examples
illustrating how different process descriptions
can lead to the same interconnection of basic
elements.
