episciences.org_5050_20230321085210083
20230321085210083
episciences.org
raphael.tournoy+crossrefapi@ccsd.cnrs.fr
episciences.org
Logical Methods in Computer Science
18605974
07
29
2022
Volume 18, Issue 3
Comparator automata in quantitative verification
Suguman
Bansal
Swarat
Chaudhuri
Moshe Y.
Vardi
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 finitestate and accept by the B\"uchi
condition as well. Such $\omega$regular comparators further lead to generic
algorithms for a number of wellstudied problems, including the quantitative
inclusion and winning strategies in quantitative graph games with incomplete
information, as well as related nondecision problems, such as obtaining a
finite representation of all counterexamples in the quantitative inclusion
problem.
We study comparators for two aggregate functions: discountedsum and
limitaverage. We prove that the discountedsum comparator is $\omega$regular
iff the discountfactor is an integer. Not every aggregate function, however,
has an $\omega$regular comparator. Specifically, we show that the language of
sequencepairs for which limitaverage aggregates exist is neither
$\omega$regular nor $\omega$contextfree. Given this result, we introduce the
notion of prefixaverage as a relaxation of limitaverage aggregation, and show
that it admits $\omega$contextfree comparators i.e. comparator automata
expressed by B\"uchi pushdown automata.
07
29
2022
5050
National Science Foundation
1704883
https://creativecommons.org/licenses/by/4.0
arXiv:1812.06569
10.48550/arXiv.1812.06569
https://arxiv.org/abs/1812.06569v3
https://arxiv.org/abs/1812.06569v2
https://arxiv.org/abs/1812.06569v1
10.46298/lmcs18(3:13)2022
https://lmcs.episciences.org/5050

https://lmcs.episciences.org/9865/pdf

https://lmcs.episciences.org/9865/pdf