Confluence in symbolic generator

[Meijuh]

The idea is to use statically derived confluence information (as provided by [lps]confcheck) during symbolic state space generation.

Several scenarios are possible:

1. ctau-groups are confluent and terminating (CR & WN)
2. assume ctau-groups are confluent only (not necessarily SN)
3. assume ctau-groups are weakly confluent

In case 1, every state is represented by its unique normal form. A symbolic algorithm is attached. In case 2, every state is represented by an element in its terminal (bottom) SCC. In case 3, every state is represented by its terminal (bottom) SCC. This boils down to computing all the BSCCS of a graph encoded as BDD. An algorithm based on pivoting individual states an be constructed, but might be suboptimal

Implementing 1 would be interesting, in order to see if confluence reduction is beneficial in a symbolic context.

Unsolved problem: how to push confluence information through the PINS interface?

Option 1:

• a separate array, indicating which groups are confluent
• easy to provide for mCRL and muCRL2
• careful: regrouping should only merge groups in the same category

Option 2:

• provide another, boolean, label on each transition (besides the action label)
• seems to be more flexible (same group can generate confluent and not confluent steps)
• it is less obvious how to enumerate all [non] confluent transitions

Attached: a symbolic algorithm for scenario 1.