Under- or overapproximate the solution of a PBES, by abstracting from variables.


Consider the following PBES:

nu X(n:Nat) = val(n > 1000000) || X(n+1)

Computing X(0) depends on the computation of equations for all X(i), for i <= 1000000. After pbesabstract, for variable n, the equation is reduced to:

nu X(n:Nat) = false || X(n+1)

Now, an application of pbesparelm can detect the redundancy of variable n, allowing one to rewrite the above equation to the equivalent PBES:

nu X = false || X

The latter is readily seen to have solution true. As a result, also the original equation systems have result true.