Lois Nijland: Adding sequential composition and termination to the linear time – branching time spectrum

Event Details

Van Glabbeek presented the linear time – branching time spectrum of behavioural semantics and gave sound, ground-complete axiomatisations for the process theory BCCSP. Groote and Chen et al. proved for the semantics in the spectrum whether there exist finite axiomatisations that are omega-complete. We add termination and sequential composition to the spectrum by studying the semantics for the process theories BSP and TSP. We provide a template for proving soundness and ground-completeness for BSP and apply this template to BSP modulo trace semantics. We prove that for BSP modulo ready simulation semantics with a finite number of actions of at least one a finite basis does not exist by giving an infinite family of equations which are sound but cannot be derived from a finite collection of axioms that are sound for BSP modulo ready simulation semantics. We show that we cannot use this family of equations to prove whether TSP modulo ready simulation semantics affords a finite basis. Finally, we prove that TSP modulo bisimulation is omega-complete when there is at least one action.