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.

We propose a new algorithm to simplify the controller development for distributed robotic systems subject to external observations, disturbances, and communication delays. Unlike prior approaches that propose specialized solutions to handling communication latency for specific robotic applications, our algorithm uses an arbitrary centralized controller as the specification and automatically generates distributed controllers with communication management and delay compensation. We formulate our goal as nonlinear optimal control— using a regret minimizing objective that measures how much the distributed agents behave differently from the delayfree centralized response—and solve for optimal actions w.r.t. local estimations of this objective using gradientbased optimization. We analyze our proposed algorithm’s behavior under a linear timeinvariant special case and prove that the closedloop dynamics satisfy a form of inputtostate stability w.r.t. unexpected disturbances and observations. Our experimental results on both simulated and realworld robotic tasks demonstrate the practical usefulness of our approach and show significant improvement over several baseline approaches.more » « less

The determinization of a nondeterministic Büchi automaton (NBA) is a fundamental construction of automata theory, with applications to probabilistic verification and reactive synthesis. The standard determinization constructions, such as the ones based on the SafraPiterman’s approach, work on the whole NBA. In this work we propose a divideandconquer determinization approach. To this end, we first classify the strongly connected components (SCCs) of the given NBA as inherently weak, deterministic accepting, and nondeterministic accepting. We then present how to determinize each type of SCC independently from the others; this results in an easier handling of the determinization algorithm that takes advantage of the structure of that SCC. Once all SCCs have been determinized, we show how to compose them so to obtain the final equivalent deterministic EmersonLei automaton, which can be converted into a deterministic Rabin automaton without blowup of states and transitions. We implement our algorithm in our tool COLA and empirically evaluate COLA with the stateoftheart tools Spot and Owl on a large set of benchmarks from the literature. The experimental results show that our prototype COLA outperforms Spot and Owl regarding the number of states and transitions.more » « less

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

The problems of verification and realizability are two central themes in the analysis of reactive systems. When multiagent systems are considered, these problems have natural analogues of existence (nonemptiness) of purestrategy Nash equilibria and verification of purestrategy Nash equilibria. Recently, this body of work has begun to include finitehorizon temporal goals. With finitehorizon temporal goals, there is a natural hierarchy of goal representation, ranging from deterministic finite automata (DFA), to nondeterministic finite automata (NFA), and to alternating finite automata (AFA), with a worstcase exponential gap between each successive representation. Previous works showed that the realizability problem with DFA goals was PSPACEcomplete, while the realizability problem with temporal logic goals is in 2EXPTIME. In this work, we study both the realizability and the verification problems with respect to various goal representations. We first show that the realizability problem with NFA goals is EXPTIMEcomplete and with AFA goals is 2EXPTIMEcomplete, thus establishing strict complexity gaps between realizability with respect to DFA, NFA, and AFA goals. We then contrast these complexity gaps with the complexity of the verification problem, where we show that verification with respect to DFAs, NFA, and AFA goals is PSPACEcomplete.

Do agents know each others’ strategies? In multiprocess software construction, each process has access to the processes already constructed; but in typical humanrobot interactions, a human may not announce its strategy to the robot (indeed, the human may not even know their own strategy). This question has often been overlooked when modeling and reasoning about multiagent systems. In this work, we study how it impacts strategic reasoning.To do so we consider Strategy Logic (SL), a wellestablished and highly expressive logic for strategic reasoning. Its usual semantics, which we call “whitebox semantics”, models systems in which agents “broadcast” their strategies. By adding imperfect information to the evaluation games for the usual semantics, we obtain a new semantics called “blackbox semantics”, in which agents keep their strategies private. We consider the modelchecking problem and show that the blackbox semantics has much lower complexity than whitebox semantics for an important fragment of Strategy Logic.

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

This paper presents a new approach to the automated design of mechanisms that incentivize selfinterested agents to maximize a global objective (such as revenue or social welfare) in equilibrium. Prior work on automated design has either been restricted to relatively simple mechanisms, or represented mechanisms as neural networks that are hard to interpret and cannot easily incorporate prior knowledge. In this paper, we propose program synthesis as a way around these issues. Concretely, we formalize the problem of designing mechanisms in the form of multiagent environments whose transition and reward functions are programs in a domainspecific language (DSL), in order to maximize an outcome such as revenue or social welfare under given assumptions on how agents act in these environments. We present an initial algorithm, based on a combination of stochastic search over programs and Bayesian optimization, for this problem. We empirically evaluate the algorithm in two domains with different characteristics. Our experiments suggest that the approach can synthesize programmatic mechanisms that are humaninterpretable and also perform well.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