Coherent branching feature bisimulation

T. Belder, M.H. Beek, ter, E.P. Vink, de

Onderzoeksoutput: Boek/rapportRapportAcademic

72 Downloads (Pure)


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.
Originele taal-2Engels
Aantal pagina's17
StatusGepubliceerd - 2015

Publicatie series

Volume1504.03474 [cs.LO]

Vingerafdruk Duik in de onderzoeksthema's van 'Coherent branching feature bisimulation'. Samen vormen ze een unieke vingerafdruk.

  • Citeer dit

    Belder, T., Beek, ter, M. H., & Vink, de, E. P. (2015). Coherent branching feature bisimulation. (arXiv; Vol. 1504.03474 [cs.LO]). s.n.