| Title | : | Process Algebra: Forward from the rear view |
| Speaker | : | Prof. S Arun Kumar (GITAM University) |
| Details | : | Thu, 23 Jan, 2025 11:00 AM @ SSB 233 |
| Abstract: | : | Abstract: Extensional equivalences in process algebra (CCS, CSP, ACP, SCCS) have
sometimes led authors to conflate divergence with deadlock, divergence
with livelock and deadlock with livelock. We attempt a reformulation
that clearly distinguishes them all.
Following Scott we take divergence to mean undefinedness and define a
basic extended process algebra (BXPA) to include ``partially'' defined
processes and their behaviours. We define a behavioural preorder,
called lifted strong bisimilarity and show that it is a precongruence
on BXPA. Divergent processes are the least elements in the preorder
and lie below both deadlocks and livelocks which are mutually
incomparable.
We extend the notion of logical characterisations of behavioural
equivalences to that of behavioural preorders using a parameterised
Hennessy-Milner Logic (PHML) and prove the characterisation of the
pre-bisimilarity using techniques developed by Milner.
Bio: S. Arun-Kumar joined GITAM University in Visakhapatnam as Distinguished Professor and Dean of Computer Science and Engineering, after superannuating from IIT Delhi as Professor of Computer Science and Engineering, IIT Delhi. He has done his Bachelor's in Mechanical Enginnering from IIT Kanpur, Master's in Computer Science from IIT Bombay and Ph.D. in Computer Science from the Tata Institute of Fundamental Research in Bombay in 1989. He subsequently worked as a Research Fellow at the University of Sussex in England. He then joined IIT Delhi and remained there till his retirement. He spent a sabbatical year at the North Carolina State University. He is a recipient of the IBM Faculty award and has received teaching awards in IIT Delhi. His research work is in formal methods, particularly in the semantics and verification of concurrent systems. Though much of his work is theoretical, he is a contributor to the model-checking tool "Concurrency Workbench of the New Century”. |
