Confluence detection for parameterised Boolean equation systems

Parameterised Boolean equation systems [1] are sequences of fixpoint
equations over predicate formulae. Such equation systems have application
in the context of model checking and equivalence checking. The de facto
technique to compute a (partial) solution to an equation system is by
instantiation to a Boolean equation system. Since the latter may be
exponentially larger than the original equation system, this can be a
time consuming transformation that we may wish to speed up.

A technique that has been applied successfully in the setting of algebraic
process verification is confluence reduction [2]. This reduces the transition
system underlying the processes by detecting and exploiting confluence at
a symbolic level and speeds up the generation of the transition system.
The main question we are interested in is whether similar techniques
can be employed in instantiating equation systems.

[1] Jan Friso Groote, Tim A. C. Willemse: Parameterised boolean equation
systems. Theor. Comput. Sci. 343(3): 332-369 (2005)

[2] Jan Friso Groote, M. P. A. Sellink: Confluence for Process
Verification. Theor. Comput. Sci. 170(1-2): 47-81 (1996)