Erik Pardijs: Finite bases in the linear time-branching time spectrum with sequential composition and succesful termination.


Event Details


The process algebra TSP extends the process algebra BCCSP with sequential composition and successful termination. For BCCSP it is known, for all semantics in Van Glabbeek’s linear time-branching time spectrum of behavioural semantics, whether a finite basis exists. In this thesis, we study whether these semantics are finitely based over TSP. We discovered that none of the congruences between Ready Simulation and Completed Trace equivalence, some of which were finitely based over BCCSP, are finitely based, regardless of alphabet cardinality. We also show that 2-Nested Simulation and Possible Futures equivalence still do not have a finite, sound and ground-complete axiomatization. Furthermore, we provide a finite basis for Simulation equivalence with an infinite alphabet, Trace equivalence with a non-singleton alphabet and Language equivalence for all alphabet cardinalities.