Last modified: Tue Apr 25 12:57:03 IST 2017
This special topics course will begin with the concept of non-determinism in finite-state automata and proceed to distinguish it from the non-determinism in concurrent systems. Generalising finite state automata to labelled transition systems (LTS), the rest of the course will use labelled transition systems as the basic framework in which to discuss various behavioural notions such as equivalences and preorders on concurrent systems.
Basic behavioural equivalence and preordering relations based on the concept of bisimulations will be defined for comparing concurrent, parallel and distributed (including mobile and timed) systems modelled using LTSs. The course then proceeds to give
characterizations of bisimulation relations.
Applications of these notions to shared-variable concurrency, distributed, parallel and mobile systems will then be considered using operational models based on LTSs.
The course is fairly mathematical (algebraic and logical) and hence students who have a strong inclination towards mathematical modelling of systems (including automata theoretic) will probably enjoy it.
Home-work 1 due Tue 24 Jan 2017.
Home-work 2 due Tue 14 Feb 2017.
Home-work 3 due Tue 07 Mar 2017.
Home-work 4 due Tue 31 Mar 2017.
Home-work 5 due Mon 08 May 2017.
Since it is expected that the registration would be small, evaluation will be through individual take-home exams mostly on applications and presentations by students.
R. Milner: Calculi for Synchrony and Asynchrony
S. Arun-Kumar: On Bisimilarities Induced by Orderings
S. Arun-Kumar and V. Natarajan: Conformance: A Precongruence Close to Bisimilarity
S. Arun-Kumar and M. Hennessy: An Efficiency Preorder for Processes
R. Milner[*]: Communication and Concurrency, Prentice-Hall
C A R Hoare[*]: Communicating Sequential Processes, Prentice-Hall
E W Dijkstra: A Discipline of Programming, Prentice-hall 1974
D Gries: The Science of Programming, Springer
E W Dijkstra: Guarded Commands, Nondeterminacy and Formal Derivation of Programs, Communications of the ACM 1975.
C A R Hoare: Communicating Sequential Processes, Communications of the ACM 1978.
N. Soundararajan: Correctness Proofs of CSP Programs, Theoretical Computer Science, vol. 24, 1983.
[*]: To get some flavour of the course. However these texts are too language-specific and do not adequately address the generality of LTSs and bisimulations. Most of the material in the course would be from papers (both classic and modern).