On Finite Alphabets and Infinite Bases: From Ready Pairs to Possible Worlds

We prove that if a finite alphabet of actions contains at least two elements, then the equational theory for the process algebra BCCSP modulo any semantics no coarser than readiness equivalence and no finer than possible worlds equivalence does not have a finite basis. This semantic range includes ready trace equivalence.

• Type: Conference
• Year: 2004
• Where: FOSSACS
• Authors: Wan Fokkink, Sumit Nain
• Keywords: FOSSACS 2004, Possible Worlds Equivalence, Readiness Equivalence, Ready Trace Equivalence, Software Engineering