I will discuss a process algebra with constants for the deadlocked and accepting processes, action prefixing, non-deterministic choice, sequencing, signals and conditions. As Jos Baeten already mentioned in his FSA colloquium talk of October 7, 2021, a process can be specified with a guarded recursive specification over this process algebra if, and only if, it is stateless(ly?) bisimilar to the process associated with a pushdown automaton. I’ll first briefly recap that correspondence result, and then proceed to present a sound and (ground-)complete axiomatisation of stateless bisimilarity in the context of the process algebra.

(The talk is based on ongoing joint work with Jos Baeten and Cesare Carissimo.)