The correctness problem for reactive systems has been thoroughly explored and is well understood. Meanwhile, the efficiency problem for reactive systems has not received the same attention. Indeed, one correct system may be less fit than another correct system and determining this manually is challenging and often done ad hoc. We (1) propose a novel and general framework which automatically assigns comparable fitness scores to reactive systems using interpretable parameters that are decoupled from the system being evaluated, (2) state the computational problem of evaluating this fitness score and reduce this problem to a matrix analysis problem, (3) discuss symbolic and numerical methods for solving this matrix analysis problem, and (4) illustrate our approach by evaluating the fitness of nine systems across three case studies, including the Alternating Bit Protocol and Two Phase Commit.

翻译：反应式系统的正确性问题已被深入研究且理解透彻。然而，其效率问题尚未得到同等关注。事实上，一个正确的系统可能不如另一个正确的系统具有适应度，而人工判别这一差异颇具挑战性，且常以特设方式完成。我们：(1) 提出一种新颖且通用的框架，利用与待评估系统解耦的可解释参数自动为反应式系统分配可比较的适应度分数；(2) 阐述评估该适应度分数的计算问题，并将其归约为矩阵分析问题；(3) 讨论求解该矩阵分析问题的符号方法与数值方法；(4) 通过三个案例研究（包括交替比特协议和两阶段提交协议）对九个系统的适应度进行评估，以说明我们的方法。