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

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

Translating OmegaRegular Specifications to Average Objectives for ModelFree Reinforcement LearningPiotr Faliszewski ; Viviana Mascardi (Ed.)Recent success in reinforcement learning (RL) has brought renewed attention to the design of reward functions by which agent behavior is reinforced or deterred. Manually designing reward functions is tedious and errorprone. An alternative approach is to specify a formal, unambiguous logic requirement, which is automatically translated into a reward function to be learned from. Omegaregular languages, of which Linear Temporal Logic (LTL) is a subset, are a natural choice for specifying such requirements due to their use in verification and synthesis. However, current techniques based on omegaregular languages learn in an episodic manner whereby the environment is periodically reset to an initial state during learning. In some settings, this assumption is challenging or impossible to satisfy. Instead, in the continuing setting the agent explores the environment without resets over a single lifetime. This is a more natural setting for reasoning about omegaregular specifications defined over infinite traces of agent behavior. Optimizing the average reward instead of the usual discounted reward is more natural in this case due to the infinitehorizon objective that poses challenges to the convergence of discounted RL solutions. We restrict our attention to the omegaregular languages which correspond to absolute liveness specifications. These specifications cannot be invalidated by any finite prefix of agent behavior, in accordance with the spirit of a continuing problem. We propose a translation from absolute liveness omegaregular languages to an average reward objective for RL. Our reduction can be done onthefly, without full knowledge of the environment, thereby enabling the use of modelfree RL algorithms. Additionally, we propose a reward structure that enables RL without episodic resetting in communicating MDPs, unlike previous approaches. We demonstrate empirically with various benchmarks that our proposed method of using average reward RL for continuing tasks defined by omegaregular specifications is more effective than competing approaches that leverage discounted RL.more » « less

In this paper, we present a toolbox for interval analysis in numpy, with an application to formal verification of neural network controlled systems. Using the notion of natural inclusion functions, we systematically construct interval bounds for a general class of mappings. The toolbox offers ef ficient computation of natural inclusion functions using compiled C code, as well as a familiar inter face in numpy with its canonical features, such as ndimensional arrays, matrix/vector operations, and vectorization. We then use this toolbox in for mal verification of dynamical systems with neural network controllers, through the composition of their inclusion functions.more » « less