The notion of comparison between system runs is fundamental in formal verification. This concept is implicitly present in the verification of qualitative systems, and is more pronounced in the verification of quantitative systems. In this work, we identify a novel mode of comparison in quantitative systems: the online comparison of the aggregate values of two sequences of quantitative weights. This notion is embodied by {\em comparator automata} ({\em comparators}, in short), a new class of automata that read two infinite sequences of weights synchronously and relate their aggregate values. We show that {aggregate functions} that can be represented with B\"uchi automaton result in comparators that are finite-state and accept by the B\"uchi condition as well. Such {\em $\omega$-regular comparators} further lead to generic algorithms for a number of well-studied problems, including the quantitative inclusion and winning strategies in quantitative graph games with incomplete information, as well as related non-decision problems, such as obtaining a finite representation of all counterexamples in the quantitative inclusion problem. We study comparators for two aggregate functions: discounted-sum and limit-average. We prove that the discounted-sum comparator is $\omega$-regular iff the discount-factor is an integer. Not every aggregate function, however, has an $\omega$-regular comparator. Specifically, we show that the language of sequence-pairs for which limit-average aggregates exist is neither $\omega$-regular nor $\omega$-context-free. Given this result, we introduce the notion of {\em prefix-average} as a relaxation of limit-average aggregation, and show that it admits $\omega$-context-free comparators.

翻译：系统运行之间的比较概念是正式核查的基础。 这一概念隐含地存在于质量系统的核查中, 并且更明显地存在于数量系统的核查中。 在这项工作中, 我们确定定量系统中一种新型的比较模式: 对两个数量加权序列的合计值进行在线比较。 这个概念体现在一个全新的自动数据类别, 它读取两个无限的权重序列, 同步并反映其总值。 我们显示, 可以用B\ uchi 自动maton来表示的 {聚合功能} 能够代表总基值的比较国是固定状态, 并且被B\\ uchi 条件也接受。 例如 $\\ 美元定期比较国的比较国 。 这样的概念进一步导致一些经过充分研究的问题的通用算法, 包括量化包容和在数量图表游戏中以不完整的信息为主, 以及相关的非决定性问题, 比如在量化包容问题时获得所有反印的定值代表值 。 我们研究两个总基值函数的参照国不是固定的基值 国 。 然而, 市值 和市值的市值 表示, 我们的市值 的市值 的市值 表示一个市值 。