Equivalence Testing in the Counting Semiring

[mschlund]

Find suitable algorithms to test the (in)equivalence of two elements of the counting-SR (depends on the representation, of course).

It would also be fine to have an incomplete test (since the theoretical complexity of testing equivalence of e.g. SL-sets is very high)

[mschlund]

Is of course possible in theory (see paper by Ginsburg and Spanier), but have yet to implement this... no idea if anywhere near practical

[pierreganty]

Could you be more specific? I suspect the following result might help you: Ganty, Iosif, Konečný. Underapproximation of Procedure Summaries for Integer Programs (TACAS 13) and whose implementation Flata is available on github.

[pierreganty]

Also, an updated version of the TACAS results are available here