arXiv subjects

Lenore Zuck

Publications and source records attributed to Lenore Zuck.

3 recordsLinked to original sources

arXiv2024

Decentralized Fair Division

Fair division is typically framed from a centralized perspective. However, in practice resource allocation often occurs via decentralized networks. We study a decentralized variant of fair division inspired by altruistic dynamics observed in behavioral economics and other practical settings. We develop an approach for decentralized fair division and compare it with a centralized approach with respect to fairness and social welfare guarantees. Our decentralized model can be seen as a relaxation of previous models of sequential exchange, in light of impossibility results concerning the inability of those models to achieve desirable outcomes. We find that the two models of resource allocation offer contrasting fairness and social welfare guarantees, and map out how these guarantees depend on valuations and other model parameters. We further show conditions under which a mix of the two approaches outperforms either approach in isolation. Despite the simplicity of our decentralized model, we show that under appropriate conditions it can ensure high-quality allocative decisions in an efficient fashion.

cs.GT↗

arXiv2023

A Case Study in Analytic Protocol Analysis in ACL2

When verifying computer systems we sometimes want to study their asymptotic behaviors, i.e., how they behave in the long run. In such cases, we need real analysis, the area of mathematics that deals with limits and the foundations of calculus. In a prior work, we used real analysis in ACL2s to study the asymptotic behavior of the RTO computation, commonly used in congestion control algorithms across the Internet. One key component in our RTO computation analysis was proving in ACL2s that for all alpha in [0, 1), the limit as n approaches infinity of alpha raised to n is zero. Whereas the most obvious proof strategy involves the logarithm, whose codomain includes irrationals, by default ACL2 only supports rationals, which forced us to take a non-standard approach. In this paper, we explore different approaches to proving the above result in ACL2(r) and ACL2s, from the perspective of a relatively new user to each. We also contextualize the theorem by showing how it allowed us to prove important asymptotic properties of the RTO computation. Finally, we discuss tradeoffs between the various proof strategies and directions for future research.

cs.LO↗

arXiv2020

Assured Autonomy: Path Toward Living With Autonomous Systems We Can Trust

The challenge of establishing assurance in autonomy is rapidly attracting increasing interest in the industry, government, and academia. Autonomy is a broad and expansive capability that enables systems to behave without direct control by a human operator. To that end, it is expected to be present in a wide variety of systems and applications. A vast range of industrial sectors, including (but by no means limited to) defense, mobility, health care, manufacturing, and civilian infrastructure, are embracing the opportunities in autonomy yet face the similar barriers toward establishing the necessary level of assurance sooner or later. Numerous government agencies are poised to tackle the challenges in assured autonomy. Given the already immense interest and investment in autonomy, a series of workshops on Assured Autonomy was convened to facilitate dialogs and increase awareness among the stakeholders in the academia, industry, and government. This series of three workshops aimed to help create a unified understanding of the goals for assured autonomy, the research trends and needs, and a strategy that will facilitate sustained progress in autonomy. The first workshop, held in October 2019, focused on current and anticipated challenges and problems in assuring autonomous systems within and across applications and sectors. The second workshop held in February 2020, focused on existing capabilities, current research, and research trends that could address the challenges and problems identified in workshop. The third event was dedicated to a discussion of a draft of the major findings from the previous two workshops and the recommendations.

cs.CY↗