Coherent Branching Feature Bisimulation}
Tessa Belder, Maurice H. ter Beek and Erik P. de Vink

Progress in the behavioral analysis of software product lines at the family
level benefits from further development of the underlying semantical theory.
Here, we propose a behavioral equivalence for feature transition systems (FTS)
generalizing branching bisimulation for labeled transition systems (LTS). We
prove that branching feature bisimulation for an FTS of a family of products
coincides with branching bisimulation for the LTS projection of each the
individual products. For a restricted notion of coherent branching feature
bisimulation we furthermore present a minimization algorithm and show its
correctness. Although the minimization problem for coherent branching feature
bisimulation is shown to be intractable, application of the algorithm in the
setting of a small case study results in a significant speed-up of model
checking of behavioral properties.