Title M&S refactoring part 2: Consider performing exact label reduction in some cases where the labels have different cost
Priority feature Status chatting
Superseder Nosy List malte, silvan
Assigned To silvan Keywords
Optional summary

Created on 2018-04-19.18:08:53 by silvan, last changed by malte.

msg7063 (view) Author: malte Date: 2018-04-20.18:03:35
No, these kind of subset queries occur in many settings (for example duplicate
elimination in regression search, or pruning given dominance relationships), and
I'm not convinced by any of the algorithms I've seen. One easy thing to look at
would be labels that are identical in all abstractions, which is a special case
of subsumption. I don't think they would often arise, but they might arise more
frequently with greedy bisimulation.
msg7062 (view) Author: silvan Date: 2018-04-20.17:56:10
I didn't find anything in the paper that would work without having a label
dominance relation, except label subsumption as you mentioned, which of course
can be viewed as a label dominance relation.

Do you have any hint at how to compute such subsumption relationships? It seems
to be expensive indeed.
msg7061 (view) Author: malte Date: 2018-04-19.18:16:04
The source seems to be msg4485, so we may want to look at the paper mentioned
there. Without having looked back at the paper, one obvious case where labels l
and l' with different cost can be merged without loss of accuracy is when
cost(l) < cost(l') and every transition labeled with l' has a parallel
transition labeled with l (i.e., the subsumption case). We don't generally test
for subsumption, presumably for efficiency reasons, so I don't know how
frequently this happens.

One special case of this is where the labels are Theta-combinable and the
subsumption relationship holds for the transition system Theta. A special case
of the special case is where the labels are locally equivalent everywhere.
msg7060 (view) Author: silvan Date: 2018-04-19.18:11:17
When looking for some potential efficiency improvements, I implemented a
cost-abstracting label reduction variant that uses the same combinability
criterion as exact label reduction but allows reducing combinable labels of
different cost. The results are underwhelming:
msg7059 (view) Author: silvan Date: 2018-04-19.18:08:53
This is part of meta issue567, which has item G that reads "Consider performing
exact label reduction in some cases where the labels have different cost". I'm
not quite sure what these "some cases" could be; Malte, do you remember/know?
Date User Action Args
2018-04-20 18:03:35maltesetmessages: + msg7063
2018-04-20 17:56:10silvansetmessages: + msg7062
2018-04-19 18:16:04maltesetmessages: + msg7061
2018-04-19 18:11:17silvansetmessages: + msg7060
2018-04-19 18:08:53silvancreate