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）通过三个案例研究（包括交替比特协议和两阶段提交协议）对九个系统的适应度进行评估，展示了我们的方法。