An official website of the United States government
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. Weshowthat 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 ω-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 f inite 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 ω-regular iff the discount-factor is an integer. Not every aggregate function, however, has an ω-regular comparator. Specifically, we show that the language of sequence-pairs for which limit-average aggregates exist is neither ω-regular nor ω-context-free. Given this result, we introduce the notion of prefixaverage as a relaxation of limit-average aggregation, and show that it admits ω-context-free comparators i.e. comparator automata expressed by B¨uchi pushdown automata.
more »
« less
Safety and Co-safety Comparator Automata for Discounted-Sum Inclusion
Discounted-sum inclusion (DS-inclusion, in short) formalizes the goal of comparing quantitative dimensions of systems such as cost, resource consumption, and the like, when the mode of aggregation for the quantitative dimension is discounted-sum aggregation. Discounted-sum comparator automata, or DS-comparators in short, are Buechi automata that read two in nite sequences of weights synchronously and relate their discounted-sum. Recent empirical investigations have shown that while DS-comparators enable competitive algorithms for DS-inclusion, they still suffer from the scalability bottleneck of Bueuchi operations. Motivated by the connections between discounted-sum and Buechi automata, this paper undertakes an investigation of language-theoretic properties of DS-comparators in order to mitigate the challenges of Buechi DS-comparators to achieve improved scalability of DS-inclusion. Our investigation uncovers that DS-comparators possess safety and co-safety language-theoretic properties. As a result, they enable reductions based on subset construction-based methods as opposed to higher complexity Buechi complementation, yielding tighter worst-case complexity and improved empirical scalability for DS-inclusion.
more »
« less
- Award ID(s):
- 1704883
- PAR ID:
- 10162114
- Date Published:
- Journal Name:
- Computer-Aided Verification
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Bouajjani, A; Holík, L.; Wu, Z. (Ed.)This paper presents an optimization based framework to automate system repair against omega-regular properties. In the proposed formalization of optimal repair, the systems are represented as Kripke structures, the properties as omega-regular languages, and the repair space as repair machines—weighted omega-regular transducers equipped with Büchi conditions—that rewrite strings and associate a cost sequence to these rewritings. To translate the resulting cost-sequences to easily interpretable payoffs, we consider several aggregator functions to map cost sequences to numbers—including limit superior, supremum, discounted-sum, and average-sum—to define quantitative cost semantics. The problem of optimal repair, then, is to determine whether traces from a given system can be rewritten to satisfy an omega-regular property when the allowed cost is bounded by a given threshold. We also consider the dual challenge of impair verification that assumes that the rewritings are resolved adversarially under some given cost restriction, and asks to decide if all traces of the system satisfy the specification irrespective of the rewritings. With a negative result to the impair verification problem, we study the problem of designing a minimal mask of the Kripke structure such that the resulting traces satisfy the specifications despite the threshold-bounded impairment. We dub this problem as the mask synthesis problem. This paper presents automata-theoretic solutions to repair synthesis, impair verification, and mask synthesis problem for limit superior, supremum, discounted-sum, and average-sum cost semantics.more » « less
-
This paper describes a new abstract interpretation-based approach to verify temporal safety properties of recursive, higher-order programs. While prior works have provided theoretical impact and some automation, they have had limited scalability. We begin with a new automata-based abstract effect domain for summarizing context-sensitive dependent effects, capable of abstracting relations between the program environment and the automaton control state. Our analysis includes a new transformer for abstracting event prefixes to automatically computed context-sensitive effect summaries, and is instantiated in a type-and-effect system grounded in abstract interpretation. Since the analysis is parametric on the automaton, we next instantiate it to a broader class of history/register (or accumulator) automata, beyond finite state automata to express some context-free properties, input-dependency, event summation, resource usage, cost, equal event magnitude, etc. We implemented a prototype evDrift that computes dependent effect summaries (and validates assertions) for OCaml-like recursive higher-order programs. As a basis of comparison, we describe reductions to assertion checking for higher-order but effect-free programs, and demonstrate that our approach outperforms prior tools Drift, RCaml/Spacer, MoCHi, and ReTHFL. Overall, across a set of 23 benchmarks, Drift verified 12 benchmarks, RCaml/Spacer verified 6, MoCHi verified 11, ReTHFL verified 18, and evDrift verified 21; evDrift also achieved a 6.3x, 5.3x, 16.8x, and 6.4x speedup over Drift, RCaml/Spacer, MoCHi, and ReTHFL, respectively, on those benchmarks that both tools could solve.more » « less
-
Reactive synthesis from high-level specifications that combine hard constraints expressed in Linear Temporal Logic (LTL) with soft constraints expressed by discounted sum (DS) rewards has applications in planning and reinforcement learning. An existing approach combines techniques from LTL synthesis with optimization for the DS rewards but has failed to yield a sound algorithm. An alternative approach combining LTL synthesis with satisficing DS rewards (rewards that achieve a threshold) is sound and complete for integer discount factors, but, in practice, a fractional discount factor is desired. This work extends the existing satisficing approach, presenting the first sound algorithm for synthesis from LTL and DS rewards with fractional discount factors. The utility of our algorithm is demonstrated on robotic planning domains.more » « less
-
We propose a novel framework for modeling attack scenarios in cyber-physical control systems: we represent a cyber-physical system as a constrained switching system, where a single model embeds the dynamics of the physical process, the attack patterns, and the attack detection schemes. We show that this is compatible with established results in hybrid automata, namely, constrained switching systems. The proposed attack modeling approach admits a large class of non-deterministic attack policies and permits the characterization of system safety as an asymptotic property. By calculating the maximal safe set, the resulting new impact metrics intuitively quantify the degradation of safety and the impact of cyber attacks on the safety properties of the system under attack. We showcase our results via an illustrative example.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1007/978-3-030-25540-4_4
