Discountedsum inclusion (DSinclusion, 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 discountedsum aggregation. Discountedsum comparator automata, or DScomparators in short, are Buechi automata
that read two innite sequences of weights synchronously and relate their discountedsum. Recent empirical investigations have shown that while DScomparators enable competitive algorithms for DSinclusion, they still suffer from the scalability bottleneck of Bueuchi operations. Motivated by the connections between discountedsum and Buechi automata,
this paper undertakes an investigation of languagetheoretic properties of DScomparators in order to mitigate the challenges of Buechi DScomparators to achieve improved scalability of DSinclusion. Our investigation uncovers that DScomparators possess safety and cosafety languagetheoretic properties. As a result, they enable reductions based on subset constructionbased methods as opposed to higher complexity Buechi complementation, yielding tighter worstcase complexity and improved empirical scalability for DSinclusion.
more »
« less
Comparator automata in quantitative verification
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 finitestate and accept by the B¨uchi condition as well. Such ω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 f inite 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 ωregular iff the discountfactor is an integer. Not every aggregate function, however, has an ωregular comparator. Specifically, we show that the language of sequencepairs for which limitaverage aggregates exist is neither ωregular nor ωcontextfree. Given this result, we introduce the notion of prefixaverage as a relaxation of limitaverage aggregation, and show that it admits ωcontextfree comparators i.e. comparator automata expressed by B¨uchi pushdown automata.
more »
« less
 Award ID(s):
 1704883
 NSFPAR ID:
 10391910
 Date Published:
 Journal Name:
 Logical methods in computer science
 Volume:
 18
 Issue:
 3
 ISSN:
 18605974
 Page Range / eLocation ID:
 13:113:28
 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 omegaregular properties. In the proposed formalization of optimal repair, the systems are represented as Kripke structures, the properties as omegaregular languages, and the repair space as repair machines—weighted omegaregular transducers equipped with Büchi conditions—that rewrite strings and associate a cost sequence to these rewritings. To translate the resulting costsequences to easily interpretable payoffs, we consider several aggregator functions to map cost sequences to numbers—including limit superior, supremum, discountedsum, and averagesum—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 omegaregular 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 thresholdbounded impairment. We dub this problem as the mask synthesis problem. This paper presents automatatheoretic solutions to repair synthesis, impair verification, and mask synthesis problem for limit superior, supremum, discountedsum, and averagesum cost semantics.more » « less

Notions of transition invariants and closure certificates have seen recent use in the formal verification of controlled dy namical systems against ωregular properties. The existing approaches face limitations in two directions. First, they re quire a closedform mathematical expression representing the model of the system. Such an expression may be difficult to find, too complex to be of any use, or unavailable due to security or privacy constraints. Second, finding such invari ants typically rely on optimization techniques such as sumof squares (SOS) or satisfiability modulo theory (SMT) solvers. This restricts the classes of systems that need to be formally verified. To address these drawbacks, we introduce a notion of neural closure certificates. We present a datadriven algo rithm that trains a neural network to represent a closure cer tificate. Our approach is formally correct under some mild as sumptions, i.e., one is able to formally show that the unknown system satisfies the ωregular property of interest if a neural closure certificate can be computed. Finally, we demonstrate the efficacy of our approach with relevant case studies.more » « less

Automata theory provides us with fundamental notions such as languages, membership, emptiness and inclusion that in turn allow us to specify and verify properties of reactive systems in a useful manner. However, these notions all yield "yes"/"no" answers that sometimes fall short of being satisfactory answers when the models being analyzed are imperfect, and the observations made are prone to errors. To address this issue, a common engineering approach is not just to verify that a system satisfies a property, but whether it does so robustly. We present notions of robustness that place a metric on words, thus providing a natural notion of distance between words. Such a metric naturally leads to a topological neighborhood of words and languages, leading to quantitative and robust versions of the membership, emptiness and inclusion problems. More generally, we consider weighted transducers to model the cost of errors. Such a transducer models neighborhoods of words by providing the cost of rewriting a word into another. The main contribution of this work is to study robustness verification problems in the context of weighted transducers. We provide algorithms for solving the robust and quantitative versions of the membership and inclusion problems while providing useful motivating case studies including approximate pattern matching problems to detect clinically relevant events in a large type1 diabetes dataset.more » « less

A barrier certificate, defined over the states of a dynamical system, is a realvalued function whose zero level set characterizes an in ductively verifiable state invariant separating reachable states from unsafe ones. When combined with powerful decision procedures— such as sumofsquares programming (SOS) or satisfiabilitymodulo theory solvers (SMT)—barrier certificates enable an automated de ductive verification approach to safety. The barrier certificate ap proach has been extended to refute LTL and l regular specifications by separating consecutive transitions of corresponding l automata in the hope of denying all accepting runs. Unsurprisingly, such tactics are bound to be conservative as refutation of recurrence properties requires reasoning about the wellfoundedness of the transitive closure of the transition relation. This paper introduces the notion of closure certificates as a natural extension of barrier certificates from state invariants to transition invariants. We aug ment these definitions with SOS and SMT based characterization for automating the search of closure certificates and demonstrate their effectiveness over some case studies.more » « less