Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher.
Some full text articles may not yet be available without a charge during the embargo (administrative interval).
What is a DOI Number?
Some links on this page may take you to nonfederal websites. Their policies may differ from this site.

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

Reactive synthesis from highlevel 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

LTLf synthesis is the automated construction of a reactive system from a highlevel description, expressed in LTLf, of its finitehorizon behavior. So far, the conversion of LTLf formulas to deterministic finitestate automata (DFAs) has been identified as the primary bottleneck to the scalabity of synthesis. Recent investigations have also shown that the size of the DFA state space plays a critical role in synthesis as well. Therefore, effective resolution of the bottleneck for synthesis requires the conversion to be time and memory performant, and prevent statespace explosion. Current conversion approaches, however, which are based either on explicitstate representation or symbolicstate representation, fail to address these necessities adequately at scale: Explicitstate approaches generate minimal DFA but are slow due to expensive DFA minimization. Symbolicstate representations can be succinct, but due to the lack of DFA minimization they generate such large state spaces that even their symbolic representations cannot compensate for the blowup. This work proposes a hybrid representation approach for the conversion. Our approach utilizes both explicit and symbolic representations of the statespace, and effectively leverages their complementary strengths. In doing so, we offer an LTLf to DFA conversion technique that addresses all three necessities, hence resolving the bottleneck. A comprehensive empirical evaluation on conversion and synthesis benchmarks supports the merits of our hybrid approach.more » « less

LTLf synthesis is the automated construction of a reactive system from a highlevel description, expressed in LTLf, of its finitehorizon behavior. So far, the conversion of LTLf formulas to deterministic finitestate automata (DFAs) has been identified as the primary bottleneck to the scalabity of synthesis. Recent investigations have also shown that the size of the DFA state space plays a critical role in synthesis as well.Therefore, effective resolution of the bottleneck for synthesis requires the conversion to be time and memory performant, and prevent statespace explosion. Current conversion approaches, however, which are based either on explicitstate representation or symbolicstate representation, fail to address these necessities adequately at scale: Explicitstate approaches generate minimal DFA but are slow due to expensive DFA minimization. Symbolicstate representations can be succinct, but due to the lack of DFA minimization they generate such large state spaces that even their symbolic representations cannot compensate for the blowup.This work proposes a hybrid representation approach for the conversion. Our approach utilizes both explicit and symbolic representations of the statespace, and effectively leverages their complementary strengths. In doing so, we offer an LTLf to DFA conversion technique that addresses all three necessities, hence resolving the bottleneck. A comprehensive empirical evaluation on conversion and synthesis benchmarks supports the merits of our hybrid approach.more » « less

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