Computer Science Seminar
Speaker: S. Arun Kumar, GITAM University
Date: Friday, 24 January 2025
Time: 2:00 PM
Venue: Seminar Hall
Extending Process Algebra with an undefined action
S. Arun Kumar
GITAM University.
24-01-25

---

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.