Back to Search
Start Over
Comparator automata in quantitative verification
- Source :
- Lecture Notes in Computer Science ISBN: 9783319893655, FoSSaCS
- Publication Year :
- 2022
- Publisher :
- episciences.org, 2022.
-
Abstract
- 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.
- Subjects :
- FOS: Computer and information sciences
Discounting
Computer Science - Logic in Computer Science
Theoretical computer science
General Computer Science
Comparator
Formal Languages and Automata Theory (cs.FL)
Computer science
Aggregate (data warehouse)
Mode (statistics)
Computer Science - Formal Languages and Automata Theory
0102 computer and information sciences
02 engineering and technology
01 natural sciences
Theoretical Computer Science
Logic in Computer Science (cs.LO)
Automaton
010201 computation theory & mathematics
0202 electrical engineering, electronic engineering, information engineering
020201 artificial intelligence & image processing
Formal verification
Subjects
Details
- Language :
- English
- ISBN :
- 978-3-319-89365-5
- ISBNs :
- 9783319893655
- Database :
- OpenAIRE
- Journal :
- Lecture Notes in Computer Science ISBN: 9783319893655, FoSSaCS
- Accession number :
- edsair.doi.dedup.....3dcc27d6975ade28db57f8adef76ba14