一句话：提出比较器自动机，统一比较两条无限权重序列的聚合值，并用于定量验证算法。
定量验证常需比较两条系统运行或权重序列的聚合值。本文提出比较器自动机，同步读取两条无限权重序列并判定其聚合值关系。作者证明：若聚合函数可由 Büchi 自动机表示，则比较器为有限状态且按 Büchi 条件接受，即 ω-正则；由此可为定量包含、不完全信息定量图博弈的获胜策略及反例有限表示提供通用算法。对于 discounted-sum，比较器为 ω-正则当且仅当折扣因子为整数；对于 limit-average，其存在性语言既非 ω-正则也非 ω-上下文无关。作者进而提出 prefix-average 松弛，并给出 ω-上下文无关比较器（Büchi 下推自动机）。
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 comparator automata (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 $\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 prefix-average as a relaxation of limit-average aggregation, and show that it admits $\omega$-context-free comparators i.e. comparator automata expressed by B\"uchi pushdown automata.
@article{paperbot1677,
title = {Comparator automata in quantitative verification},
author = {Suguman Bansal and Swarat Chaudhuri and Moshe Y. Vardi},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 3},
year = {2022},
doi = {10.46298/lmcs-18(3:13)2022}
}