相干分支特征互模拟
Coherent branching feature bisimulation
摘要：
在软件产品线的行为分析在家庭水平的进展受益于进一步发展的基本语义理论。在这里，我们提出了一个行为等价的特征转换系统（FTS）广义分支互模拟标记的转换系统（LTS）。我们证明了分支功能互模拟的一个家庭的产品的FTS与分支互模拟的LTS投影的每个单独的产品。对于相干分支特征互模拟的一个限制性概念，我们进一步提出了一个极小化算法，并证明了它的正确性。虽然相干分支特征互模拟的最小化问题被证明是棘手的，在一个小的案例研究结果的设置中的算法的应用程序在一个显着的加速模型检验的行为属性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
