Abstract:Symbolic transition graphs with assignment is a general semantical model for value-passing processes. Strong bisimulation equivalences between such graphs can be reduced to the greatest solutions to simple predicate equation systems. The aim of this paper is to generalise this result to weak bisimulation equivalences. For this purpose, the notion of nesting predicate equation systems is introduced, and algorithms are presented to reduce weak bisimulation equivalences to the greatest solutions to nesting predicate equation systems of the form E2μE1.